From f5349978eae2915243ccfe0757c734f8535922ce Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 27 Nov 2024 13:17:06 -0600 Subject: [PATCH] Add support for the opaque and transparent modifiers --- src/ivcMcs.ml | 8 +- src/lustre/contractsToProps.ml | 2 +- src/lustre/lspInfo.ml | 4 +- src/lustre/lustreAbstractInterpretation.ml | 2 +- src/lustre/lustreArrayDependencies.ml | 2 +- src/lustre/lustreAst.ml | 14 ++- src/lustre/lustreAst.mli | 7 ++ src/lustre/lustreAstDependencies.ml | 12 +-- src/lustre/lustreAstHelpers.ml | 4 +- src/lustre/lustreAstInlineConstants.ml | 8 +- src/lustre/lustreAstNormalizer.ml | 8 +- src/lustre/lustreDeclarations.ml | 4 +- src/lustre/lustreDependencies.ml | 8 +- src/lustre/lustreDesugarAnyOps.ml | 14 +-- src/lustre/lustreDesugarFrameBlocks.ml | 6 +- src/lustre/lustreDesugarIfBlocks.ml | 8 +- src/lustre/lustreFlattenRefinementTypes.ml | 8 +- src/lustre/lustreGenRefTypeImpNodes.ml | 18 ++-- src/lustre/lustreInstantiatePolyNodes.ml | 34 +++---- src/lustre/lustreLexer.mll | 2 + src/lustre/lustreNode.ml | 8 ++ src/lustre/lustreNode.mli | 2 + src/lustre/lustreNodeGen.ml | 17 +++- src/lustre/lustreParser.messages | 6 +- src/lustre/lustreParser.mly | 24 +++-- src/lustre/lustreRemoveMultAssign.ml | 8 +- src/lustre/lustreSlicing.ml | 4 +- src/lustre/lustreSyntaxChecks.ml | 27 ++++-- src/lustre/lustreSyntaxChecks.mli | 2 + src/lustre/lustreTypeChecker.ml | 4 +- src/nativeInput.ml | 1 + src/opacity.ml | 26 ++++++ src/opacity.mli | 28 ++++++ src/strategy.ml | 92 +++++++++++-------- src/strategy.mli | 3 +- src/subSystem.ml | 13 ++- src/subSystem.mli | 6 +- .../lustreSyntaxChecks/opaque_no_contract.lus | 5 + .../transparent_no_body.lus | 3 + tests/ounit/lustre/testLustreFrontend.ml | 8 ++ 40 files changed, 307 insertions(+), 153 deletions(-) create mode 100644 src/opacity.ml create mode 100644 src/opacity.mli create mode 100644 tests/ounit/lustre/lustreSyntaxChecks/opaque_no_contract.lus create mode 100644 tests/ounit/lustre/lustreSyntaxChecks/transparent_no_body.lus diff --git a/src/ivcMcs.ml b/src/ivcMcs.ml index 274716244..ad1c0deb7 100644 --- a/src/ivcMcs.ml +++ b/src/ivcMcs.ml @@ -225,7 +225,7 @@ let rand_node name ts = |> List.map2 (fun t out -> dpos,HString.mk_hstring out,t,A.ClockTrue) ts in A.NodeDecl (dspan, - (name, true, [], [dpos,HString.mk_hstring "id",A.Int dpos,A.ClockTrue, false], + (name, true, Opaque, [], [dpos,HString.mk_hstring "id",A.Int dpos,A.ClockTrue, false], outs, [], [], None) ) @@ -413,7 +413,7 @@ let minimize_contract_node_eq ue lst cne = | A.AssumptionVars _ -> [cne] let minimize_node_decl ue loc_core - ((id, extern, tparams, inputs, outputs, locals, items, spec) as ndecl) = + ((id, extern, opac, tparams, inputs, outputs, locals, items, spec) as ndecl) = let id' = HString.string_of_hstring id in let id_typ_map = build_id_typ_map inputs outputs locals in @@ -428,7 +428,7 @@ let minimize_node_decl ue loc_core end in let locals = List.map (minimize_node_local_decl ue lst) locals in - (id, extern, tparams, inputs, outputs, locals, items, spec) + (id, extern, opac, tparams, inputs, outputs, locals, items, spec) in let scope = (Scope.mk_scope [id']) in @@ -471,7 +471,7 @@ let minimize_decl ue loc_core = function | decl -> decl let fill_input_types_hashtbl ast = - let aux_node_decl (id, _, _, inputs, _, _, _, _) = + let aux_node_decl (id, _, _, _, inputs, _, _, _, _) = let typ_of_input (_,_,t,_,_) = t in Hashtbl.replace nodes_input_types id (List.map typ_of_input inputs) ; in diff --git a/src/lustre/contractsToProps.ml b/src/lustre/contractsToProps.ml index 239ba1204..d1b68175d 100644 --- a/src/lustre/contractsToProps.ml +++ b/src/lustre/contractsToProps.ml @@ -188,7 +188,7 @@ let rec fmt_declarations fmt = function " pp_print_position spos |> failwith - | Ast.NodeDecl (_, (wan, _, two,tri,far,fiv,six,contract)) -> ( + | Ast.NodeDecl (_, (wan, _, _, two,tri,far,fiv,six,contract)) -> ( let contract_info = match contract with | None -> ([],[],[],[]) | Some (_, c) -> collect_contracts ([],[],[],[]) c diff --git a/src/lustre/lspInfo.ml b/src/lustre/lspInfo.ml index c4d7bfa39..95817986e 100644 --- a/src/lustre/lspInfo.ml +++ b/src/lustre/lspInfo.ml @@ -73,7 +73,7 @@ let lsp_const_decl_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } = elnum ecnum let lsp_node_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } - (id, imported, _, _, _, _, _, contract) = + (id, imported, _, _, _, _, _, _, contract) = let file, slnum, scnum = Lib.file_row_col_of_pos spos in let _, elnum, ecnum = Lib.file_row_col_of_pos epos in match contract with @@ -113,7 +113,7 @@ let lsp_node_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } elnum ecnum let lsp_function_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } - (id, imported, _, _, _, _, _, _) = + (id, imported, _, _, _, _, _, _, _) = let file, slnum, scnum = Lib.file_row_col_of_pos spos in let _, elnum, ecnum = Lib.file_row_col_of_pos epos in Format.fprintf ppf diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index ffc04ca82..7fb3a0721 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -234,7 +234,7 @@ and interpret_contract_node ty_ctx (id, ps, ins, outs, contract) = let ty_ctx = TC.add_io_node_ctx ty_ctx id ps ins outs in interpret_contract id empty_context ty_ctx contract -and interpret_node ty_ctx gids (id, _, ps, ins, outs, locals, items, contract) = +and interpret_node ty_ctx gids (id, _, _, ps, ins, outs, locals, items, contract) = (* Setup the typing context *) let ty_ctx = TC.add_io_node_ctx ty_ctx id ps ins outs in let ctx = IMap.empty in diff --git a/src/lustre/lustreArrayDependencies.ml b/src/lustre/lustreArrayDependencies.ml index 5f5291c89..d0ffe6b88 100644 --- a/src/lustre/lustreArrayDependencies.ml +++ b/src/lustre/lustreArrayDependencies.ml @@ -268,7 +268,7 @@ let rec check_inductive_array_dependencies ctx ns = function | [] -> Ok () and check_node_decl ctx ns decl = - let (id, _, params, inputs, outputs, locals, items, _) = decl in + let (id, _, _, params, inputs, outputs, locals, items, _) = decl in (* Setup the typing context *) let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in let* (graph, pos_map, count, idx_len) = process_items ctx ns items in diff --git a/src/lustre/lustreAst.ml b/src/lustre/lustreAst.ml index 4bf41421d..c12c45c9b 100644 --- a/src/lustre/lustreAst.ml +++ b/src/lustre/lustreAst.ml @@ -274,6 +274,10 @@ type contract_node_equation = (* A contract is some ghost consts / var, and assumes guarantees and modes. *) type contract = position * (contract_node_equation list) +type opacity = + | Default + | Opaque + | Transparent (* A node or function declaration @@ -281,6 +285,7 @@ Boolean flag indicates whether node / function is extern. *) type node_decl = ident * bool + * opacity * ident list * const_clocked_typed_decl list * clocked_typed_decl list @@ -1146,17 +1151,22 @@ let pp_print_contract_node_decl ppf (n,p,i,o,(_,e)) let pp_print_node_or_fun_decl is_fun ppf ( - _, (n, ext, p, i, o, l, e, r) + _, (n, ext, opac, p, i, o, l, e, r) ) = if e = [] then Format.fprintf ppf - "@[@[%s%s %a%t@ \ + "@[@[%s%s%s %a%t@ \ @[(%a)@]@;<1 -2>\ returns@ @[(%a)@];@]@.\ %a@?\ %a@?@]@?" (if is_fun then "function" else "node") (if ext then " imported" else "") + (match opac with + | Default -> "" + | Opaque -> "opaque " + | Transparent -> "transparent " + ) pp_print_ident n (function ppf -> pp_print_node_param_list ppf p) (pp_print_list pp_print_const_clocked_typed_ident ";@ ") i diff --git a/src/lustre/lustreAst.mli b/src/lustre/lustreAst.mli index 69384cbef..85f866069 100644 --- a/src/lustre/lustreAst.mli +++ b/src/lustre/lustreAst.mli @@ -285,10 +285,16 @@ type contract = position * (contract_node_equation list) (* contract_mode list * contract_call list *) (* ) list *) +type opacity = + | Default + | Opaque + | Transparent + (** Declaration of a node or function as a tuple of - its identifier, - a flag, true if the node / function is extern + - its opacity - its type parameters, - the list of its inputs, - the list of its outputs, @@ -298,6 +304,7 @@ type contract = position * (contract_node_equation list) type node_decl = ident * bool + * opacity * ident list * const_clocked_typed_decl list * clocked_typed_decl list diff --git a/src/lustre/lustreAstDependencies.ml b/src/lustre/lustreAstDependencies.ml index 87b9564c5..41a98454e 100644 --- a/src/lustre/lustreAstDependencies.ml +++ b/src/lustre/lustreAstDependencies.ml @@ -521,7 +521,7 @@ and extract_node_calls: LA.node_item list -> (LA.ident * Lib.position) list = fun l -> List.fold_left (fun acc i -> extract_node_calls_item i @ acc) [] l let mk_graph_node_decl: Lib.position -> LA.node_decl -> dependency_analysis_data - = fun pos (i, _, _, ips, ops, locals, nitems, contract_opt) -> + = fun pos (i, _, _, _, ips, ops, locals, nitems, contract_opt) -> let cg = connect_g_pos (match contract_opt with | None -> empty_dependency_analysis_data @@ -580,8 +580,8 @@ let rec mk_decl_map: LA.declaration option IMap.t -> LA.t -> ((LA.declaration o let* m' = check_and_add m pos const_prefix i (Some cnstd) in mk_decl_map m' decls - | (LA.NodeDecl (span, (i, _, _, _, _, _, _, _)) as ndecl) :: decls - | (LA.FuncDecl (span, (i, _, _, _, _, _, _, _)) as ndecl) :: decls -> + | (LA.NodeDecl (span, (i, _, _, _, _, _, _, _, _)) as ndecl) :: decls + | (LA.FuncDecl (span, (i, _, _, _, _, _, _, _, _)) as ndecl) :: decls -> let {LA.start_pos = pos} = span in let* m' = check_and_add m pos node_prefix i (Some ndecl) in mk_decl_map m' decls @@ -1152,7 +1152,7 @@ let summarize_ip_vars: LA.ident list -> SI.t -> int list = fun ips critial_ips - (** Helper function to generate a node summary *) let mk_node_summary: bool -> node_summary -> LA.node_decl -> node_summary - = fun connect_imported s (i, imported, _, ips, ops, _, items, _) -> + = fun connect_imported s (i, imported, _, _, ips, ops, _, items, _) -> if not imported then let op_vars = List.map (fun o -> LH.extract_op_ty o |> fst) ops in @@ -1345,7 +1345,7 @@ let check_no_input_output_local_duplicate ips ops locals = let check_node_equations: dependency_analysis_data -> LA.node_decl -> (LA.node_decl, [> error]) result - = fun ad ((i, imported, params, ips, ops, locals, items, contract_opt) as ndecl)-> + = fun ad ((i, imported, opac, params, ips, ops, locals, items, contract_opt) as ndecl)-> (if not imported then let* _ = check_no_input_output_local_duplicate ips ops locals in analyze_circ_node_equations ad.nsummary2 items >> @@ -1357,7 +1357,7 @@ let check_node_equations: dependency_analysis_data let* (_, _, _, _, c') = sort_and_check_contract_eqns ad (HString.concat (HString.mk_hstring "inline$") [contract_prefix;i], params, ips, ops, c) in - R.ok (i, imported, params, ips, ops, locals, items, Some c') + R.ok (i, imported, opac, params, ips, ops, locals, items, Some c') (** Check if node equations do not have circularity and also, if the node has a contract sort the contract equations. *) diff --git a/src/lustre/lustreAstHelpers.ml b/src/lustre/lustreAstHelpers.ml index caa893e88..f8a501185 100644 --- a/src/lustre/lustreAstHelpers.ml +++ b/src/lustre/lustreAstHelpers.ml @@ -1226,7 +1226,7 @@ let get_last_node_name: declaration list -> ident option let rec get_first_node_name: declaration list -> ident option = function | [] -> None - | NodeDecl (_, (n, _, _, _, _, _, _, _)) :: _ -> Some n + | NodeDecl (_, (n, _, _, _, _, _, _, _, _)) :: _ -> Some n | _ :: rest -> get_first_node_name rest in get_first_node_name (List.rev ds) @@ -1238,7 +1238,7 @@ let rec remove_node_in_declarations: fun n pres -> function | [] -> None - | (NodeDecl (_, (n', _, _, _, _, _, _, _)) as mn) :: rest -> + | (NodeDecl (_, (n', _, _, _, _, _, _, _, _)) as mn) :: rest -> if HString.compare n' n = 0 then Some (mn, pres @ rest) else remove_node_in_declarations n (pres @ [mn]) rest diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 22fec0ad3..b227fd04a 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -515,7 +515,7 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati let e' = simplify_expr ctx e in let ctx' = TC.add_ty (TC.add_const ctx i e' ty' Global) i ty' in (ctx', ConstDecl (span, TypedConst (pos', i, e', ty'))) - | (LA.NodeDecl (span, (i, imported, params, ips, ops, ldecls, items, contract))) -> + | (LA.NodeDecl (span, (i, imported, opac, params, ips, ops, ldecls, items, contract))) -> let ips' = inline_constants_of_const_clocked_type_decl ctx ips in let ops' = inline_constants_of_clocked_type_decl ctx ops in let contract' = match contract with @@ -524,8 +524,8 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati in let ctx', ldecls' = inline_constants_of_node_locals ctx ldecls in let items' = inline_constants_of_node_items ctx' items in - ctx, (LA.NodeDecl (span, (i, imported, params, ips', ops', ldecls', items', contract'))) - | (LA.FuncDecl (span, (i, imported, params, ips, ops, ldecls, items, contract))) -> + ctx, (LA.NodeDecl (span, (i, imported, opac, params, ips', ops', ldecls', items', contract'))) + | (LA.FuncDecl (span, (i, imported, opac, params, ips, ops, ldecls, items, contract))) -> let ips' = inline_constants_of_const_clocked_type_decl ctx ips in let ops' = inline_constants_of_clocked_type_decl ctx ops in let contract' = match contract with @@ -534,7 +534,7 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati in let ctx', ldecls' = inline_constants_of_node_locals ctx ldecls in let items' = inline_constants_of_node_items ctx' items in - ctx, (LA.FuncDecl (span, (i, imported, params, ips', ops', ldecls', items', contract'))) + ctx, (LA.FuncDecl (span, (i, imported, opac, params, ips', ops', ldecls', items', contract'))) | (LA.ContractNodeDecl (span, (i, params, ips, ops, (p, contract)))) -> ctx, (LA.ContractNodeDecl (span, (i, params, ips, ops, (p, inline_constants_of_contract ctx contract)))) | e -> (ctx, e) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index aa57e6a7d..74da8e22d 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -296,10 +296,10 @@ let pp_print_generated_identifiers ppf gids = let compute_node_input_constant_mask decls = let over_decl map = function - | A.NodeDecl (_, (id, _, _, inputs, _, _, _, _)) -> + | A.NodeDecl (_, (id, _, _, _, inputs, _, _, _, _)) -> let is_consts = List.map (fun (_, _, _, _, c) -> c) inputs in StringMap.add id is_consts map - | FuncDecl (_, (id, _, _, inputs, _, _, _, _)) -> + | FuncDecl (_, (id, _, _, _, inputs, _, _, _, _)) -> let is_consts = List.map (fun (_, _, _, _, c) -> c) inputs in StringMap.add id is_consts map | _ -> map @@ -1134,7 +1134,7 @@ and normalize_ghost_declaration info node_id map = function FreeConst (pos, id, ty), map, warnings and normalize_node info map - (node_id, is_extern, params, inputs, outputs, locals, items, contract) = + (node_id, is_extern, opac, params, inputs, outputs, locals, items, contract) = (* Setup the typing context *) let ctx = Chk.add_io_node_ctx info.context node_id params inputs outputs in let ctx = Ctx.add_ty ctx ctr_id (A.Int dpos) in @@ -1250,7 +1250,7 @@ and normalize_node info map gids4; gids5; gids7; gids6_8; gids9; gids10] in let old_gids, warnings6 = normalize_gid_equations info map node_id in let map = StringMap.add node_id (union old_gids new_gids) map in - (node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts), + (node_id, is_extern, opac, params, inputs, outputs, locals, List.flatten nitems, ncontracts), map, List.flatten warnings1 @ List.flatten warnings2 @ List.flatten warnings3 @ warnings4 @ warnings5 @ warnings6 diff --git a/src/lustre/lustreDeclarations.ml b/src/lustre/lustreDeclarations.ml index 02bd9b790..002f08a81 100644 --- a/src/lustre/lustreDeclarations.ml +++ b/src/lustre/lustreDeclarations.ml @@ -2105,7 +2105,7 @@ and declaration_to_context ctx = function (* Function declaration without parameters *) | A.FuncDecl ( - {A.start_pos = pos}, (i, ext, [], inputs, outputs, locals, items, contracts) + {A.start_pos = pos}, (i, ext, _, [], inputs, outputs, locals, items, contracts) ) -> ( (* Identifier of AST identifier *) @@ -2185,7 +2185,7 @@ and declaration_to_context ctx = function (* Node declaration without parameters *) | A.NodeDecl ( - {A.start_pos = pos}, (i, ext, [], inputs, outputs, locals, items, contracts) + {A.start_pos = pos}, (i, ext, _, [], inputs, outputs, locals, items, contracts) ) -> ( (* Identifier of AST identifier *) diff --git a/src/lustre/lustreDependencies.ml b/src/lustre/lustreDependencies.ml index dbeca600d..dd40831e3 100644 --- a/src/lustre/lustreDependencies.ml +++ b/src/lustre/lustreDependencies.ml @@ -125,9 +125,9 @@ let info_of_decl = function | A.ConstDecl ({A.start_pos=pos}, A.TypedConst(_, ident, _, _)) -> pos, ident |> HString.string_of_hstring |> I.mk_string_ident, Const -| A.NodeDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _)) -> +| A.NodeDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _, _)) -> pos, ident |> HString.string_of_hstring |> I.mk_string_ident, NodeOrFun -| A.FuncDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _)) -> +| A.FuncDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _, _)) -> pos, ident |> HString.string_of_hstring |> I.mk_string_ident, NodeOrFun | A.ContractNodeDecl ({A.start_pos=pos}, (ident, _, _, _, _)) -> @@ -146,8 +146,8 @@ let insert_decl decl (f_type, f_ident) decls = let has_ident = match f_type with | NodeOrFun -> ( function - | A.NodeDecl (_, (i, _, _, _, _, _, _, _)) -> i = ident - | A.FuncDecl (_, (i, _, _, _, _, _, _, _)) -> i = ident + | A.NodeDecl (_, (i, _, _, _, _, _, _, _, _)) -> i = ident + | A.FuncDecl (_, (i, _, _, _, _, _, _, _, _)) -> i = ident | _ -> false ) | Type -> ( diff --git a/src/lustre/lustreDesugarAnyOps.ml b/src/lustre/lustreDesugarAnyOps.ml index d800c806a..29f0ce5c5 100644 --- a/src/lustre/lustreDesugarAnyOps.ml +++ b/src/lustre/lustreDesugarAnyOps.ml @@ -97,11 +97,11 @@ fun ctx node_name fun_ids expr -> let generated_node = if has_pre_arrow_or_node_call then A.NodeDecl (span, - (name, true, ty_params, inputs, + (name, true, A.Opaque, ty_params, inputs, [pos, id, ty, A.ClockTrue], [], [], Some (pos, contract))) else A.FuncDecl (span, - (name, true, ty_params, inputs, + (name, true, A.Opaque, ty_params, inputs, [pos, id, ty, A.ClockTrue], [], [], Some (pos, contract))) in A.Call(pos, ty_vars, name, inputs_call), [generated_node] @@ -263,24 +263,24 @@ fun ctx node_name fun_ids ni -> let desugar_any_ops: Ctx.tc_context -> A.declaration list -> A.declaration list = fun ctx decls -> let fun_ids = List.filter_map - (fun decl -> match decl with | A.FuncDecl (_, (id, _, _, _, _, _, _, _)) -> Some id | _ -> None) + (fun decl -> match decl with | A.FuncDecl (_, (id, _, _, _, _, _, _, _, _)) -> Some id | _ -> None) decls in let decls = List.fold_left (fun decls decl -> match decl with - | A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) -> + | A.NodeDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) -> let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in let items, gen_nodes = List.map (desugar_node_item ctx id fun_ids) items |> List.split in let contract, gen_nodes2 = desugar_contract ctx id fun_ids contract in let gen_nodes = List.flatten gen_nodes in - decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))] - | A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) -> + decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract))] + | A.FuncDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) -> let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in let items, gen_nodes = List.map (desugar_node_item ctx id fun_ids) items |> List.split in let contract, gen_nodes2 = desugar_contract ctx id fun_ids contract in let gen_nodes = List.flatten gen_nodes in - decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))] + decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract))] | A.ContractNodeDecl (span, (id, params, inputs, outputs, contract)) -> let ctx = Chk.add_io_node_ctx ctx id params inputs outputs in let contract, gen_nodes = desugar_contract ctx id fun_ids (Some contract) in diff --git a/src/lustre/lustreDesugarFrameBlocks.ml b/src/lustre/lustreDesugarFrameBlocks.ml index 57b90743f..ea1ae4344 100644 --- a/src/lustre/lustreDesugarFrameBlocks.ml +++ b/src/lustre/lustreDesugarFrameBlocks.ml @@ -339,15 +339,15 @@ let desugar_node_item node_id ni = match ni with let desugar_frame_blocks sorted_node_contract_decls = HString.HStringHashtbl.clear pos_list_map ; let desugar_node_decl decl = (match decl with - | A.NodeDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis2, co))) -> + | A.NodeDecl (s, ((node_id, b, o, nps, cctds, ctds, nlds, nis2, co))) -> let* res = R.seq (List.map (desugar_node_item node_id) nis2) in let decls, nis, warnings = split3 res in let warnings = List.flatten warnings in - R.ok (A.NodeDecl (s, (node_id, b, nps, cctds, ctds, + R.ok (A.NodeDecl (s, (node_id, b, o, nps, cctds, ctds, (List.flatten decls) @ nlds, List.flatten nis, co)), warnings) (* Make sure there are no frame blocks in functions *) - | A.FuncDecl (_, ((_, _, _, _, _, _, nis, _))) -> ( + | A.FuncDecl (_, ((_, _, _, _, _, _, _, nis, _))) -> ( let contains_frame_block = List.find_opt (fun ni -> match ni with | A.FrameBlock _ -> true | _ -> false) nis in match contains_frame_block with | Some (FrameBlock (pos, _, _, _) as fb) -> mk_error pos (MisplacedFrameBlockError fb) diff --git a/src/lustre/lustreDesugarIfBlocks.ml b/src/lustre/lustreDesugarIfBlocks.ml index da2019897..8c9e4ee2e 100644 --- a/src/lustre/lustreDesugarIfBlocks.ml +++ b/src/lustre/lustreDesugarIfBlocks.ml @@ -341,18 +341,18 @@ let rec desugar_node_item node_id ctx ni = match ni with (** Desugars an individual node declaration (removing IfBlocks). *) let desugar_node_decl ctx decl = match decl with - | A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) -> + | A.FuncDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)) -> let ctx = Chk.add_full_node_ctx ctx node_id nps cctds ctds nlds in let* nis = R.seq (List.map (desugar_node_item node_id ctx) nis) in let new_decls, nis, gids = split_and_flatten3 nis in let gids = List.fold_left GI.union (GI.empty ()) gids in - R.ok (A.FuncDecl (s, (node_id, b, nps, cctds, ctds, new_decls @ nlds, nis, co)), GI.StringMap.singleton node_id gids) - | A.NodeDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) -> + R.ok (A.FuncDecl (s, (node_id, b, opac, nps, cctds, ctds, new_decls @ nlds, nis, co)), GI.StringMap.singleton node_id gids) + | A.NodeDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)) -> let ctx = Chk.add_full_node_ctx ctx node_id nps cctds ctds nlds in let* nis = R.seq (List.map (desugar_node_item node_id ctx) nis) in let new_decls, nis, gids = split_and_flatten3 nis in let gids = List.fold_left GI.union (GI.empty ()) gids in - R.ok (A.NodeDecl (s, (node_id, b, nps, cctds, ctds, new_decls @ nlds, nis, co)), GI.StringMap.singleton node_id gids) + R.ok (A.NodeDecl (s, (node_id, b, opac, nps, cctds, ctds, new_decls @ nlds, nis, co)), GI.StringMap.singleton node_id gids) | _ -> R.ok (decl, GI.StringMap.empty) diff --git a/src/lustre/lustreFlattenRefinementTypes.ml b/src/lustre/lustreFlattenRefinementTypes.ml index c6fa5b43f..c728c9e61 100644 --- a/src/lustre/lustreFlattenRefinementTypes.ml +++ b/src/lustre/lustreFlattenRefinementTypes.ml @@ -195,7 +195,7 @@ let flatten_ref_types ctx sorted_node_contract_decls = List.map (fun decl -> match decl with | A.TypeDecl (pos, AliasType (pos2, id, ps, ty)) -> A.TypeDecl (pos, AliasType (pos2, id, ps, flatten_ref_type ctx ty)) - | NodeDecl (pos, (id, imported, params, ips, ops, locals, items, contract)) -> + | NodeDecl (pos, (id, imported, opac, params, ips, ops, locals, items, contract)) -> let ctx = List.fold_left (fun acc p -> TypeCheckerContext.add_ty_syn acc p (A.AbstractType (Lib.dummy_pos, p)) @@ -211,8 +211,8 @@ let flatten_ref_types ctx sorted_node_contract_decls = let locals = List.map (flatten_ref_types_local_decl ctx) locals in let items = List.map (flatten_ref_types_item ctx) items in let contract = flatten_ref_types_contract_opt ctx contract in - NodeDecl (pos, (id, imported, params, ips, ops, locals, items, contract)) - | FuncDecl (pos, (id, imported, params, ips, ops, locals, items, contract)) -> + NodeDecl (pos, (id, imported, opac, params, ips, ops, locals, items, contract)) + | FuncDecl (pos, (id, imported, opac, params, ips, ops, locals, items, contract)) -> let ctx = List.fold_left (fun acc p -> TypeCheckerContext.add_ty_syn acc p (A.AbstractType (Lib.dummy_pos, p)) @@ -228,7 +228,7 @@ let flatten_ref_types ctx sorted_node_contract_decls = let locals = List.map (flatten_ref_types_local_decl ctx) locals in let items = List.map (flatten_ref_types_item ctx) items in let contract = flatten_ref_types_contract_opt ctx contract in - FuncDecl (pos, (id, imported, params, ips, ops, locals, items, contract)) + FuncDecl (pos, (id, imported, opac, params, ips, ops, locals, items, contract)) | NodeParamInst (pos, (id1, id2, tys)) -> let tys = List.map (flatten_ref_type ctx) tys in NodeParamInst (pos, (id1, id2, tys)) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 53660a17c..127a98a87 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -29,7 +29,7 @@ let unwrap = function | Error _ -> assert false let node_decl_to_contracts -= fun pos ctx (id, extern, params, inputs, outputs, locals, _, contract) -> += fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) -> let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in let contract' = List.filter_map (fun ci -> match ci with @@ -62,11 +62,11 @@ let node_decl_to_contracts (* We generate two imported nodes: One for the input node's contract (w/ type info), and another for the input node's inputs/environment *) if extern then - let environment = gen_node_id, extern, params, inputs2, outputs2, [], node_items, contract' in + let environment = gen_node_id, extern, A.Opaque, params, inputs2, outputs2, [], node_items, contract' in if Flags.Contracts.check_environment () then [environment] else [] else - let environment = gen_node_id, extern', params, inputs2, outputs2, [], node_items, contract' in - let contract = (gen_node_id2, extern', params, inputs, locals_as_outputs @ outputs, [], node_items, contract) in + let environment = gen_node_id, extern', A.Opaque, params, inputs2, outputs2, [], node_items, contract' in + let contract = (gen_node_id2, extern', A.Opaque, params, inputs, locals_as_outputs @ outputs, [], node_items, contract) in if Flags.Contracts.check_environment () then [environment; contract] else [contract] (* NOTE: Currently, we do not allow global constants to have refinement types. @@ -80,7 +80,7 @@ let type_to_contract: Lib.position -> HString.t -> A.lustre_type -> HString.t li let gen_node_id = HString.concat2 (HString.mk_hstring type_tag) id in (* To prevent slicing, we mark generated imported nodes as main nodes *) let node_items = [A.AnnotMain(pos, true)] in - Some (NodeDecl (span, (gen_node_id, true, ps, [], [(pos, id, ty, A.ClockTrue)], [], node_items, None))) + Some (NodeDecl (span, (gen_node_id, true, A.Opaque, ps, [], [(pos, id, ty, A.ClockTrue)], [], node_items, None))) let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> A.declaration list = fun ctx decls -> @@ -94,19 +94,19 @@ let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> A.declaration list | None -> acc) | A.TypeDecl (_, FreeType _) | A.ConstDecl (_, UntypedConst _) -> acc - | A.NodeDecl (span, ((p, e, ps, ips, ops, locs, _, c) as node_decl)) -> + | A.NodeDecl (span, ((p, e, opac, ps, ips, ops, locs, _, c) as node_decl)) -> (* Add main annotations to imported nodes *) let node_decl = - if e then p, e, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c + if e then p, e, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else node_decl in let decls = node_decl_to_contracts span.start_pos ctx node_decl in let decls = List.map (fun decl -> A.NodeDecl (span, decl)) decls in A.NodeDecl(span, node_decl) :: decls @ acc - | A.FuncDecl (span, ((p, e, ps, ips, ops, locs, _, c) as func_decl)) -> + | A.FuncDecl (span, ((p, e, opac, ps, ips, ops, locs, _, c) as func_decl)) -> (* Add main annotations to imported functions *) let func_decl = - if e then p, e, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c + if e then p, e, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else func_decl in let decls = node_decl_to_contracts span.start_pos ctx func_decl in diff --git a/src/lustre/lustreInstantiatePolyNodes.ml b/src/lustre/lustreInstantiatePolyNodes.ml index 73fddc07d..97e0317c7 100644 --- a/src/lustre/lustreInstantiatePolyNodes.ml +++ b/src/lustre/lustreInstantiatePolyNodes.ml @@ -117,14 +117,14 @@ let rec gen_poly_decl: Ctx.tc_context -> HString.t option -> (A.declaration * A. ctx, pnname, [], node_decls_map (* Creating new polymorphic instantiation *) | None -> - let span, is_function, is_contract, ext, ips, ops, locs, nis, c = + let span, is_function, is_contract, ext, opac, ips, ops, locs, nis, c = match GI.StringMap.find nname node_decls_map with - | (A.FuncDecl (span, (_, ext, _, ips, ops, locs, nis, c)), _) -> - span, true, false, ext, ips, ops, locs, nis, c - | (A.NodeDecl (span, (_, ext, __FUNCTION__, ips, ops, locs, nis, c)), _) -> - span, false, false, ext, ips, ops, locs, nis, c - | (A.ContractNodeDecl (span, (_, _, ips, ops, c)), _) -> - span, false, true, false, ips, ops, [], [], Some c + | (A.FuncDecl (span, (_, ext, opac, _, ips, ops, locs, nis, c)), _) -> + span, true, false, ext, opac, ips, ops, locs, nis, c + | (A.NodeDecl (span, (_, ext, opac, __FUNCTION__, ips, ops, locs, nis, c)), _) -> + span, false, false, ext, opac, ips, ops, locs, nis, c + | (A.ContractNodeDecl (span, (_, _, ips, ops, c)), _) -> + span, false, true, false, A.Default, ips, ops, [], [], Some c | _ -> assert false in let nis = List.filter (fun ni -> match ni with @@ -171,7 +171,7 @@ let rec gen_poly_decl: Ctx.tc_context -> HString.t option -> (A.declaration * A. let ctx = Ctx.add_ty_args_node ctx pnname ty_args in let node_ty = build_node_fun_ty span.start_pos ips ops in Ctx.add_ty_node ctx pnname node_ty, - A.FuncDecl (span, (pnname, ext, ps, ips, ops, locs, nis, c)) + A.FuncDecl (span, (pnname, ext, opac, ps, ips, ops, locs, nis, c)) else if is_contract then let c = Option.get c in let ctx = Ctx.add_ty_vars_contract ctx pnname ps in @@ -187,7 +187,7 @@ let rec gen_poly_decl: Ctx.tc_context -> HString.t option -> (A.declaration * A. let ctx = Ctx.add_ty_args_node ctx pnname ty_args in let node_ty = build_node_fun_ty span.start_pos ips ops in Ctx.add_ty_node ctx pnname node_ty, - NodeDecl (span, (pnname, ext, ps, ips, ops, locs, nis, c)) + NodeDecl (span, (pnname, ext, opac, ps, ips, ops, locs, nis, c)) in (* Recursively create new instantiations (this node could use the given polymorphic @@ -473,7 +473,7 @@ and gen_poly_decls_ci and gen_poly_decls_decls = fun ctx node_decls_map decls -> let ctx, decls, node_decls_map = List.fold_left (fun (ctx, acc_decls, acc_node_decls_map) decl -> match decl with - | A.FuncDecl (p, (nname, ext, ps, ips, ops, locs, nis, c)) -> + | A.FuncDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, c)) -> let ctx = Chk.add_ty_params_node_ctx ctx nname ps in let ctx, ips, decls, node_decls_map = List.fold_left (fun (ctx, acc_ips, acc_decls, acc_node_decls_map) ip -> let ctx, ip, decls, node_decls_map = gen_poly_decls_ip ctx (Some nname) acc_node_decls_map ip in @@ -493,17 +493,17 @@ and gen_poly_decls_decls ) (ctx, [], decls, node_decls_map) nis in ( match c with | None -> - let decl = A.FuncDecl (p, (nname, ext, ps, ips, ops, locs, nis, c)) in + let decl = A.FuncDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, c)) in ctx, decl :: decls, node_decls_map | Some (p3, c) -> let ctx, c, decls, node_decls_map = List.fold_left (fun (ctx, acc_cis, acc_decls, acc_node_decls_map) ip -> let ctx, ci, decls, node_decls_map = gen_poly_decls_ci ctx (Some nname) acc_node_decls_map ip in ctx, acc_cis @ [ci], decls @ acc_decls, node_decls_map ) (ctx, [], decls, node_decls_map) c in - let decl = A.FuncDecl (p, (nname, ext, ps, ips, ops, locs, nis, Some (p3, c))) in + let decl = A.FuncDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, Some (p3, c))) in ctx, decl :: decls, node_decls_map ) - | NodeDecl (p, (nname, ext, ps, ips, ops, locs, nis, c)) -> + | NodeDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, c)) -> let ctx = Chk.add_ty_params_node_ctx ctx nname ps in let ctx, ips, decls, node_decls_map = List.fold_left (fun (ctx, acc_ips, acc_decls, acc_node_decls_map) ip -> let ctx, ip, decls, node_decls_map = gen_poly_decls_ip ctx (Some nname) acc_node_decls_map ip in @@ -523,14 +523,14 @@ and gen_poly_decls_decls ) (ctx, [], decls, node_decls_map) nis in ( match c with | None -> - let decl = A.NodeDecl (p, (nname, ext, ps, ips, ops, locs, nis, c)) in + let decl = A.NodeDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, c)) in ctx, decl :: decls, node_decls_map | Some (p3, c) -> let ctx, c, decls, node_decls_map = List.fold_left (fun (ctx, acc_cis, acc_decls, acc_node_decls_map) ip -> let ctx, ci, decls, node_decls_map = gen_poly_decls_ci ctx (Some nname) acc_node_decls_map ip in ctx, acc_cis @ [ci], decls @ acc_decls, node_decls_map ) (ctx, [], decls, node_decls_map) c in - let decl = A.NodeDecl (p, (nname, ext, ps, ips, ops, locs, nis, Some (p3, c))) in + let decl = A.NodeDecl (p, (nname, ext, opac, ps, ips, ops, locs, nis, Some (p3, c))) in ctx, decl :: decls, node_decls_map ) | ContractNodeDecl (p, (cname, ps, ips, ops, (p3, c))) -> @@ -560,8 +560,8 @@ let instantiate_polymorphic_nodes: Ctx.tc_context -> A.declaration list -> Ctx.t (* Initialize node_decls_map (a map from a node name to its declaration and the list of its polymorphic instantiations created so far) *) let node_decls_map = List.fold_left (fun acc decl -> match decl with - | (A.NodeDecl (_, (id, _, _, _, _, _, _, _)) as decl) - | (FuncDecl (_, (id, _, _, _, _, _, _, _)) as decl) + | (A.NodeDecl (_, (id, _, _, _, _, _, _, _, _)) as decl) + | (FuncDecl (_, (id, _, _, _, _, _, _, _, _)) as decl) | (ContractNodeDecl (_, (id, _, _, _, _)) as decl) -> GI.StringMap.add id (decl, []) acc | TypeDecl _ | ConstDecl _ | NodeParamInst _ -> acc ) GI.StringMap.empty decls diff --git a/src/lustre/lustreLexer.mll b/src/lustre/lustreLexer.mll index 85653c6c6..d4be3a71c 100644 --- a/src/lustre/lustreLexer.mll +++ b/src/lustre/lustreLexer.mll @@ -247,6 +247,8 @@ let keyword_table = mk_hashtbl [ "param", PARAM ; (* Node / function declaration *) + "transparent", TRANSPARENT ; + "opaque", OPAQUE ; "imported", IMPORTED ; "node", NODE ; "function", FUNCTION ; diff --git a/src/lustre/lustreNode.ml b/src/lustre/lustreNode.ml index 5c6254492..0ce506bcc 100644 --- a/src/lustre/lustreNode.ml +++ b/src/lustre/lustreNode.ml @@ -137,6 +137,7 @@ type equation = equation_lhs * E.t (* A contract. *) type contract = C.t + (* A Lustre node *) type t = { @@ -146,6 +147,9 @@ type t = { (* Is the node extern? *) is_extern: bool; + (* Whether the node should be always abstracted by its contract, never, or sometimes *) + opacity: Opacity.t; + (* Node type arguments *) ty_args: LustreAst.lustre_type list; @@ -211,6 +215,7 @@ type t = { let empty_node name is_extern = { name ; is_extern ; + opacity = Translucent; ty_args = []; instance = StateVar.mk_state_var @@ -1139,6 +1144,8 @@ let rec subsystem_of_nodes' nodes accum = function (* Scope of the system from node name *) let scope = [I.string_of_ident false top] in + let opacity = node.opacity in + (* Does node have contracts? *) let has_contract = has_effective_contract node in @@ -1153,6 +1160,7 @@ let rec subsystem_of_nodes' nodes accum = function { SubSystem.scope; SubSystem.source = node; + SubSystem.opacity; SubSystem.has_contract; SubSystem.has_modes; SubSystem.has_impl; diff --git a/src/lustre/lustreNode.mli b/src/lustre/lustreNode.mli index 907e93384..d0ea0d0d0 100644 --- a/src/lustre/lustreNode.mli +++ b/src/lustre/lustreNode.mli @@ -156,6 +156,8 @@ type t = { is_extern : bool; (** Is the node extern? *) + opacity: Opacity.t; + (** Whether the node should be always abstracted by its contract, never, or sometimes *) ty_args: LustreAst.lustre_type list; (** Node type arguments (if the node was created during monomorphization) *) diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index af90d610a..fff3a48fc 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1426,11 +1426,17 @@ and compile_contract cstate gids ctx map contract_scope node_scope contract = in assumes @ assumes2, guarantees @ guarantees2 -and compile_node_decl gids_map is_function cstate ctx i ext params inputs outputs locals items contract = +and compile_node_decl gids_map is_function opac cstate ctx i ext params inputs outputs locals items contract = let gids = StringMap.find i gids_map in let name = mk_ident i in let node_scope = name |> I.to_scope in let is_extern = ext in + let opacity = + match opac with + | A.Opaque -> Opacity.Opaque + | A.Transparent -> Opacity.Transparent + | A.Default -> Opacity.Translucent + in let instance = StateVar.mk_state_var ~is_const:true @@ -2313,6 +2319,7 @@ and compile_node_decl gids_map is_function cstate ctx i ext params inputs output let (node:N.t) = { name; is_extern; + opacity; ty_args; instance; init_flag; @@ -2420,10 +2427,10 @@ and compile_declaration: compiler_state -> GI.t StringMap.t -> Ctx.tc_context -> | A.ConstDecl (_, const_decl) -> let empty_map = ref (empty_identifier_maps None) in compile_const_decl cstate ctx empty_map [] const_decl - | A.FuncDecl (_, (i, ext, params, inputs, outputs, locals, items, contract)) -> - compile_node_decl gids true cstate ctx i ext params inputs outputs locals items contract - | A.NodeDecl (_, (i, ext, params, inputs, outputs, locals, items, contract)) -> - compile_node_decl gids false cstate ctx i ext params inputs outputs locals items contract + | A.FuncDecl (_, (i, ext, opac, params, inputs, outputs, locals, items, contract)) -> + compile_node_decl gids true opac cstate ctx i ext params inputs outputs locals items contract + | A.NodeDecl (_, (i, ext, opac, params, inputs, outputs, locals, items, contract)) -> + compile_node_decl gids false opac cstate ctx i ext params inputs outputs locals items contract (* All contract node declarations are recorded and normalized in gids, this is necessary because each unique call to a contract node must be normalized independently *) diff --git a/src/lustre/lustreParser.messages b/src/lustre/lustreParser.messages index ea83019c5..6ade2a7d3 100644 --- a/src/lustre/lustreParser.messages +++ b/src/lustre/lustreParser.messages @@ -3079,4 +3079,8 @@ Syntax Error! main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ASSUME LPARAMBRACKET RPARAMBRACKET XOR - +Syntax Error! + +main: OPAQUE XOR + +Syntax Error! diff --git a/src/lustre/lustreParser.mly b/src/lustre/lustreParser.mly index c2ef230ab..1872a346a 100644 --- a/src/lustre/lustreParser.mly +++ b/src/lustre/lustreParser.mly @@ -89,6 +89,8 @@ let mk_span start_pos end_pos = %token PARAM (* Tokens for node declarations *) +%token OPAQUE +%token TRANSPARENT %token IMPORTED %token NODE %token LPARAMBRACKET @@ -237,6 +239,10 @@ one_expr: e = expr EOF { e } (* A Lustre program is a list of declarations *) main: p = list(decl) EOF { List.flatten p } +opacity_modifier: + | OPAQUE { A.Opaque } + | TRANSPARENT { A.Transparent } + | { A.Default } (* A declaration is a type, a constant, a node or a function declaration *) decl: @@ -249,23 +255,23 @@ decl: | d = type_decl { List.map (function e -> A.TypeDecl (mk_span $startpos $endpos, e)) d } - | NODE ; decl = node_decl ; def = node_def { + | opac = opacity_modifier ; NODE ; decl = node_decl ; def = node_def { let (n, p, i, o, r) = decl in let (l, e) = def in - [A.NodeDecl ( mk_span $startpos $endpos, (n, false, p, i, o, l, e, r) )] + [A.NodeDecl ( mk_span $startpos $endpos, (n, false, opac, p, i, o, l, e, r) )] } - | FUNCTION ; decl = node_decl ; def = node_def { + | opac = opacity_modifier ; FUNCTION ; decl = node_decl ; def = node_def { let (n, p, i, o, r) = decl in let (l, e) = def in - [A.FuncDecl (mk_span $startpos $endpos, (n, false, p, i, o, l, e, r))] + [A.FuncDecl (mk_span $startpos $endpos, (n, false, opac, p, i, o, l, e, r))] } - | NODE ; IMPORTED ; decl = node_decl { + | opac = opacity_modifier ; NODE ; IMPORTED ; decl = node_decl { let (n, p, i, o, r) = decl in - [A.NodeDecl ( mk_span $startpos $endpos, (n, true, p, i, o, [], [], r) )] + [A.NodeDecl ( mk_span $startpos $endpos, (n, true, opac, p, i, o, [], [], r) )] } - | FUNCTION ; IMPORTED ; decl = node_decl { + | opac = opacity_modifier ; FUNCTION ; IMPORTED ; decl = node_decl { let (n, p, i, o, r) = decl in - [A.FuncDecl (mk_span $startpos $endpos, (n, true, p, i, o, [], [], r))] + [A.FuncDecl (mk_span $startpos $endpos, (n, true, opac, p, i, o, [], [], r))] } | d = contract_decl { [A.ContractNodeDecl (mk_span $startpos $endpos, d)] } | d = node_param_inst { [A.NodeParamInst (mk_span $startpos $endpos, d)] } @@ -579,7 +585,7 @@ contract_spec: (* A node declaration as an instance of a parameterized node *) node_param_inst: - | NODE; + | opacity_modifier ; NODE; n = ident; EQUALS; s = ident; diff --git a/src/lustre/lustreRemoveMultAssign.ml b/src/lustre/lustreRemoveMultAssign.ml index 641353b31..aa9f72caf 100644 --- a/src/lustre/lustreRemoveMultAssign.ml +++ b/src/lustre/lustreRemoveMultAssign.ml @@ -157,18 +157,18 @@ let desugar_node_item ctx ni = match ni with (** Remove multiple assignment from if and frame blocks in a single declaration. *) let desugar_node_decl ctx decl = match decl with - | A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) -> + | A.FuncDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)) -> let ctx = Chk.add_full_node_ctx ctx node_id nps cctds ctds nlds in let res = List.map (desugar_node_item ctx) nis in let nis, gids = List.split res in let gids = List.fold_left GI.union (GI.empty ()) gids in - A.FuncDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)), GI.StringMap.singleton node_id gids - | A.NodeDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)) -> + A.FuncDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)), GI.StringMap.singleton node_id gids + | A.NodeDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)) -> let ctx = Chk.add_full_node_ctx ctx node_id nps cctds ctds nlds in let res = List.map (desugar_node_item ctx) nis in let nis, gids = List.split res in let gids = List.fold_left GI.union (GI.empty ()) gids in - A.NodeDecl (s, (node_id, b, nps, cctds, ctds, nlds, nis, co)), GI.StringMap.singleton node_id gids + A.NodeDecl (s, (node_id, b, opac, nps, cctds, ctds, nlds, nis, co)), GI.StringMap.singleton node_id gids | _ -> decl, GI.StringMap.empty (** Desugars a declaration list to remove multiple assignment from if blocks and frame diff --git a/src/lustre/lustreSlicing.ml b/src/lustre/lustreSlicing.ml index 41906ce19..ff33caa77 100644 --- a/src/lustre/lustreSlicing.ml +++ b/src/lustre/lustreSlicing.ml @@ -662,7 +662,8 @@ let slice_all_of_node ?(keep_contracts = true) ?(keep_asserts = true) { N.name; - N.is_extern; + N.is_extern; + N.opacity; N.ty_args; N.instance; N.init_flag; @@ -686,6 +687,7 @@ let slice_all_of_node properties, assertions, contracts and main annotation *) { N.name; N.is_extern; + N.opacity; N.ty_args; N.instance; N.init_flag; diff --git a/src/lustre/lustreSyntaxChecks.ml b/src/lustre/lustreSyntaxChecks.ml index 3c75e6689..e2021267f 100644 --- a/src/lustre/lustreSyntaxChecks.ml +++ b/src/lustre/lustreSyntaxChecks.ml @@ -67,6 +67,8 @@ type error_kind = Unknown of string | MisplacedVarInFrameBlock of LustreAst.ident | MisplacedAssertInFrameBlock | IllegalClockExprInActivate of LustreAst.expr + | OpaqueWithoutContract of LustreAst.ident + | TransparentWithoutBody of LustreAst.ident type error = [ | `LustreSyntaxChecksError of Lib.position * error_kind @@ -119,6 +121,8 @@ let error_message kind = match kind with | MisplacedVarInFrameBlock id -> "Variable '" ^ HString.string_of_hstring id ^ "' is defined in the frame block but not declared in the frame block header" | MisplacedAssertInFrameBlock -> "Assertion not allowed in frame block initialization" | IllegalClockExprInActivate e -> "Illegal clock expression '" ^ LA.string_of_expr e ^ "' in activate" + | OpaqueWithoutContract n -> "An opaque annotation found for a node/function without a contract: " ^ HString.string_of_hstring n + | TransparentWithoutBody n -> "A transparent annotation found for an imported node/function: " ^ HString.string_of_hstring n let syntax_error pos kind = Error (`LustreSyntaxChecksError (pos, kind)) @@ -286,9 +290,9 @@ let build_global_ctx (decls:LustreAst.t) = | ConstDecl (_, TypedConst (_, i, _, ty)) -> ctx_add_const acc i (Some ty) (* The types here can be constructed from the available information but this type information is not needed for syntax checks for now *) - | NodeDecl (_, (i, _, _, _, _, _, _, _)) -> + | NodeDecl (_, (i, _, _, _, _, _, _, _, _)) -> ctx_add_node acc i () - | FuncDecl (_, (i, _, _, _, _, _, _, _)) -> + | FuncDecl (_, (i, _, _, _, _, _, _, _, _)) -> ctx_add_func acc i () | _ -> acc in @@ -619,6 +623,11 @@ let rec expr_only_supported_in_merge observer expr = else syntax_error pos (UnsupportedOutsideMerge e) | RestartEvery (_, _, e1, e2) -> r_list observer e1 >> r observer e2 +let check_opacity pos node_id contract is_ext = function + | LA.Opaque when contract = None -> syntax_error pos (OpaqueWithoutContract node_id) + | Transparent when is_ext -> syntax_error pos (TransparentWithoutBody node_id) + | _ -> Ok () + let rec syntax_check (ast:LustreAst.t) = let ctx = build_global_ctx ast in let* warnings_decls = Res.seq (List.map (check_declaration ctx) ast) in @@ -701,11 +710,12 @@ and check_local_items: context -> LA.node_local_decl -> ([> warning] list, [> er | NodeVarDecl (_, (_, _, _, LA.ClockTrue)) -> Ok ([]) | NodeVarDecl (_, (pos, i, _, _)) -> syntax_error pos (UnsupportedClockedLocal i) -and check_node_decl ctx span (id, ext, params, inputs, outputs, locals, items, contract) = +and check_node_decl ctx span (id, ext, opac, params, inputs, outputs, locals, items, contract) = let decl = LA.NodeDecl - (span, (id, ext, params, inputs, outputs, locals, items, contract)) + (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) in - (locals_exactly_one_definition locals items) + check_opacity span.start_pos id contract ext opac + >> (locals_exactly_one_definition locals items) >> (outputs_at_most_one_definition outputs items) >> (Res.seq_ (List.map check_input_items inputs)) >> (Res.seq_ (List.map check_output_items outputs)) >> @@ -725,13 +735,13 @@ and check_node_decl ctx span (id, ext, params, inputs, outputs, locals, items, c items) in (Ok (warnings1 @ List.flatten warnings2 @ warnings3, decl)) -and check_func_decl ctx span (id, ext, params, inputs, outputs, locals, items, contract) = +and check_func_decl ctx span (id, ext, opac, params, inputs, outputs, locals, items, contract) = let ctx = (* Locals are not visible in contracts *) build_local_ctx ctx [] inputs outputs in let decl = LA.FuncDecl - (span, (id, ext, params, inputs, outputs, locals, items, contract)) + (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) in let composed_items_checks ctx e = (no_calls_to_node ctx e) @@ -744,7 +754,8 @@ and check_func_decl ctx span (id, ext, params, inputs, outputs, locals, items, c let* warnings2 = (no_temporal_operator "function contract" e) in Ok (warnings1 @ warnings2) in - (Res.seq_ (List.map no_reachability_modifiers items)) + check_opacity span.start_pos id contract ext opac + >> (Res.seq_ (List.map no_reachability_modifiers items)) >> (Res.seq_ (List.map check_input_items inputs)) >> (Res.seq_ (List.map check_output_items outputs)) >> let* warnings1 = (Res.seq (List.map (check_local_items ctx) locals)) in diff --git a/src/lustre/lustreSyntaxChecks.mli b/src/lustre/lustreSyntaxChecks.mli index 14d8ccba6..b100404a1 100644 --- a/src/lustre/lustreSyntaxChecks.mli +++ b/src/lustre/lustreSyntaxChecks.mli @@ -50,6 +50,8 @@ type error_kind = Unknown of string | MisplacedVarInFrameBlock of LustreAst.ident | MisplacedAssertInFrameBlock | IllegalClockExprInActivate of LustreAst.expr + | OpaqueWithoutContract of LustreAst.ident + | TransparentWithoutBody of LustreAst.ident type error = [ | `LustreSyntaxChecksError of Lib.position * error_kind diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index efc74dc8a..7eb8cf3b5 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -1398,7 +1398,7 @@ and check_type_const_decl: tc_context -> HString.t option -> LA.const_decl -> tc and check_type_node_decl: Lib.position -> tc_context -> LA.node_decl -> ([> warning] list, [> error]) result = fun pos ctx - (node_name, is_extern, params, input_vars, output_vars, ldecls, items, contract) + (node_name, is_extern, _, params, input_vars, output_vars, ldecls, items, contract) -> Debug.parse "TC declaration node: %a {" LA.pp_print_ident node_name; let arg_ids = LA.SI.of_list (List.map (fun a -> LH.extract_ip_ty a |> fst) input_vars) in @@ -1815,7 +1815,7 @@ and tc_ctx_of_ty_decl: tc_context -> LA.type_decl -> (tc_context, [> error]) res R.ok (add_ty_decl ctx' i) and tc_ctx_of_node_decl: Lib.position -> tc_context -> LA.node_decl -> (tc_context * [> warning] list, [> error]) result - = fun pos ctx (nname, _, ps, ip, op, _, _, _)-> + = fun pos ctx (nname, _, _, ps, ip, op, _, _, _)-> Debug.parse "Extracting type of node declaration: %a" LA.pp_print_ident nname diff --git a/src/nativeInput.ml b/src/nativeInput.ml index a44eeef84..39917ce27 100644 --- a/src/nativeInput.ml +++ b/src/nativeInput.ml @@ -430,6 +430,7 @@ let node_def_of_sexpr = function let rec mk_subsys_structure sys = { SubSystem.scope = TransSys.scope_of_trans_sys sys; source = sys; + opacity = Opacity.Transparent; has_contract = false; has_impl = true; has_modes = false; diff --git a/src/opacity.ml b/src/opacity.ml new file mode 100644 index 000000000..2fbaa54a9 --- /dev/null +++ b/src/opacity.ml @@ -0,0 +1,26 @@ +(* This file is part of the Kind 2 model checker. + + Copyright (c) 2024 by the Board of Trustees of the University of Iowa + + Licensed under the Apache License, Version 2.0 (the "License"); you + may not use this file except in compliance with the License. You + may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied. See the License for the specific language governing + permissions and limitations under the License. + +*) + +type t = + | Opaque + (* Always use the contract *) + | Translucent + (* Use the contract, and refine with the body if required *) + | Transparent + (* Always use the body *) + diff --git a/src/opacity.mli b/src/opacity.mli new file mode 100644 index 000000000..8714b1fab --- /dev/null +++ b/src/opacity.mli @@ -0,0 +1,28 @@ +(* This file is part of the Kind 2 model checker. + + Copyright (c) 2024 by the Board of Trustees of the University of Iowa + + Licensed under the Apache License, Version 2.0 (the "License"); you + may not use this file except in compliance with the License. You + may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied. See the License for the specific language governing + permissions and limitations under the License. + +*) + +(** @author Daniel Larraz *) + +type t = + | Opaque + (** Always use the contract *) + | Translucent + (** Use the contract, and refine with the body if required *) + | Transparent + (** Always use the body *) + diff --git a/src/strategy.ml b/src/strategy.ml index 2f0855363..03437d90c 100644 --- a/src/strategy.ml +++ b/src/strategy.ml @@ -17,11 +17,13 @@ *) module A = Analysis +module O = Opacity (** Information used by the strategy module. *) type info = { - can_refine: bool ; (** Is the system refineable? ([extern] for lustre nodes.) *) + opacity: Opacity.t ; (** Whether the node should be always abstracted by its contract, never, or sometimes *) has_contract: bool ; (** Does the system have a contract? *) + has_impl: bool ; (** Does the system have an implementation? *) has_modes: bool ; (** Does the system have modes? *) } @@ -48,30 +50,35 @@ let get_reachability_abstraction results subs_of_scope result = not abstracted systems to the input. The function looks at the subsystems previously appended to the input recursively. *) let rec loop refined abstraction = function - | ( (system, _) :: tail ) :: lower -> ( + | ( (system, { opacity } ) :: tail ) :: lower -> ( (* Is system currently abstracted? *) if Scope.Map.find system abstraction then (* Is system refineable? *) - try match A.results_find system results with - | ({ A.param } as result) :: _ -> - (* It is if everything was proved in the last analysis. *) - if A.result_is_all_inv_proved result then ( - let info = A.info_of_param param in - let sub = info.A.top in - (* System is now concrete. *) - let abstraction = Scope.Map.add sub false abstraction in - (* Updating with the abstraction used to prove [sub]. *) - let abstraction = - merge_abstractions abstraction info.A.abstraction_map - in - (tail :: lower) @ [ subs_of_scope system ] - |> loop true abstraction - ) - (* Otherwise keep going. *) - else tail :: lower |> loop refined abstraction - | [] -> failwith "unreachable" - with Not_found -> (* Case of imported nodes (they have no result) *) + if (opacity <> Opaque) then ( + try match A.results_find system results with + | ({ A.param } as result) :: _ -> + (* It is if everything was proved in the last analysis. *) + if A.result_is_all_inv_proved result then ( + let info = A.info_of_param param in + let sub = info.A.top in + (* System is now concrete. *) + let abstraction = Scope.Map.add sub false abstraction in + (* Updating with the abstraction used to prove [sub]. *) + let abstraction = + merge_abstractions abstraction info.A.abstraction_map + in + (tail :: lower) @ [ subs_of_scope system ] + |> loop true abstraction + ) + (* Otherwise keep going. *) + else tail :: lower |> loop refined abstraction + | [] -> failwith "unreachable" + with Not_found -> (* Case of imported nodes (they have no result) *) + tail :: lower |> loop refined abstraction + ) + else ( tail :: lower |> loop refined abstraction + ) else (* System is not abstracted, remembering its subsystems and looping. *) (tail :: lower) @ [ subs_of_scope system ] @@ -119,19 +126,24 @@ let get_refinement_abstraction results subs_of_scope result = looks at the subsystems previously appended to the input recursively. *) let rec loop = function - | ( (candidate, _) :: tail ) :: lower -> ( + | ( (candidate, { opacity }) :: tail ) :: lower -> ( (* Is candidate currently abstracted? *) if Scope.Map.find candidate abstraction then (* Is candidate refineable? *) - try match A.results_find candidate results with - | result :: _ -> - (* It is if everything was proved in the last analysis. *) - if A.result_is_all_inv_proved result then Some result - (* Otherwise keep going. *) - else tail :: lower |> loop - | [] -> failwith "unreachable" - with Not_found -> (* Case of imported nodes (they have no result) *) + if (opacity <> O.Opaque) then ( + try match A.results_find candidate results with + | result :: _ -> + (* It is if everything was proved in the last analysis. *) + if A.result_is_all_inv_proved result then Some result + (* Otherwise keep going. *) + else tail :: lower |> loop + | [] -> failwith "unreachable" + with Not_found -> (* Case of imported nodes (they have no result) *) + tail :: lower |> loop + ) + else ( tail :: lower |> loop + ) else (* Candidate is not abstracted, remembering its subsystems and looping. *) (tail :: lower) @ [ subs_of_scope candidate ] |> loop @@ -157,21 +169,23 @@ let get_refinement_abstraction results subs_of_scope result = Some (sub, abstraction) ) -let is_candidate_for_analysis { can_refine ; has_modes } = - (has_modes && Flags.Contracts.check_modes ()) || can_refine +let is_candidate_for_analysis { has_impl ; has_modes } = + (has_modes && Flags.Contracts.check_modes ()) || has_impl (* Returns an option of the parameter for the first analysis of a system. *) let first_param_of ass _results all_nodes scope = let rec loop abstraction = function - | (sys, { can_refine ; has_contract ; has_modes }) :: tail -> ( + | (sys, { opacity; has_impl ; has_contract ; has_modes }) :: tail -> ( (* Can/should we abstract this system? *) let is_abstract = if sys = scope then has_modes && (Flags.Contracts.check_modes ()) else - (not can_refine) || ( - has_contract && (Flags.Contracts.compositional ()) + (not has_impl) || (has_contract && + (opacity=O.Opaque || + (Flags.Contracts.compositional() && opacity<>O.Transparent) + ) ) in (* Format.printf "%a is abstract: %b@.@." Scope.pp_print_scope sys is_abstract ; *) @@ -263,7 +277,7 @@ let next_monolithic_analysis results main_syss = function " | all_syss -> ( - let check_sys ( top, { can_refine } ) = + let check_sys ( top, { has_impl } ) = try ( match A.results_find top results with | [] -> failwith "unreachable" @@ -271,7 +285,7 @@ let next_monolithic_analysis results main_syss = function A.param = A.ContractCheck info ; A.contract_valid ; } ] when Flags.Contracts.check_implem () -> - if can_refine then + if has_impl then (* Invariants generated during ContractCheck analysis are discarded. They were generated assuming the contract! *) let ass = A.assumptions_empty in @@ -329,13 +343,13 @@ let next_modular_analysis results subs_of_scope = function Returns the params of the next analysis for that system if any, calls [go_up] on the systems before that system otherwise. *) let rec go_down prefix = function - | (sys, { can_refine }) :: tail -> ( + | (sys, { has_impl }) :: tail -> ( try ( (* Format.printf "| %a@." Scope.pp_print_scope sys ; *) match A.results_find sys results with | [] -> assert false | _ when Flags.Contracts.check_implem () |> not || - not can_refine -> go_up prefix + not has_impl -> go_up prefix | [ { A.param = A.ContractCheck info ; A.contract_valid ; diff --git a/src/strategy.mli b/src/strategy.mli index 91ca7d3c2..ab3d9db75 100644 --- a/src/strategy.mli +++ b/src/strategy.mli @@ -27,8 +27,9 @@ module A = Analysis (** Information used by the strategy module. *) type info = { - can_refine: bool ; (** Is the system refineable? ([extern] for lustre nodes.) *) + opacity: Opacity.t ; (** Whether the node should be always abstracted by its contract, never, or sometimes *) has_contract: bool ; (** Does the system have a contract? *) + has_impl: bool ; (** Does the system have an implementation? *) has_modes: bool ; (** Does the system have modes? *) } diff --git a/src/subSystem.ml b/src/subSystem.ml index d908bda18..d5aac4034 100644 --- a/src/subSystem.ml +++ b/src/subSystem.ml @@ -23,13 +23,16 @@ type 'a t = { (* Original input. *) source : 'a ; - (* System can be abstracted to its contract. *) + (* Whether the system should be always abstracted by its contract, never, or sometimes. *) + opacity : Opacity.t ; + + (* System has a contract. *) has_contract : bool ; (* System has modes. *) has_modes : bool ; - (* System can be refined to its implementation. *) + (* System has an implementation. *) has_impl : bool ; (* Direct sub-systems. *) @@ -38,11 +41,13 @@ type 'a t = { (* Strategy info of a subsystem. *) let strategy_info_of { - has_contract ; has_modes ; has_impl + opacity; has_contract ; has_modes ; has_impl } = { - Strategy.can_refine = has_impl ; + Strategy.opacity ; Strategy.has_contract ; Strategy.has_modes ; + Strategy.has_impl; + } diff --git a/src/subSystem.mli b/src/subSystem.mli index 190d78bc0..0dbd64590 100644 --- a/src/subSystem.mli +++ b/src/subSystem.mli @@ -36,11 +36,13 @@ type 'a t = { source : 'a ; (** Original input *) - has_contract : bool ; (** System can be abstracted to its contract *) + opacity : Opacity.t ; (** Whether the system should be always abstracted by its contract, never, or sometimes *) + + has_contract : bool ; (** System has a contract *) has_modes : bool ; (** System has modes. *) - has_impl : bool ; (** System can be refined to its implementation *) + has_impl : bool ; (** System has an implementation *) subsystems : 'a t list ; (** Sub-systems *) } diff --git a/tests/ounit/lustre/lustreSyntaxChecks/opaque_no_contract.lus b/tests/ounit/lustre/lustreSyntaxChecks/opaque_no_contract.lus new file mode 100644 index 000000000..22190fd67 --- /dev/null +++ b/tests/ounit/lustre/lustreSyntaxChecks/opaque_no_contract.lus @@ -0,0 +1,5 @@ + +opaque node N(x:int) returns (y:int); +let + y = x + 1; +tel diff --git a/tests/ounit/lustre/lustreSyntaxChecks/transparent_no_body.lus b/tests/ounit/lustre/lustreSyntaxChecks/transparent_no_body.lus new file mode 100644 index 000000000..5de011cac --- /dev/null +++ b/tests/ounit/lustre/lustreSyntaxChecks/transparent_no_body.lus @@ -0,0 +1,3 @@ + +transparent +node imported N(x:int) returns (y:int); diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml index a62169684..e3aecdaf7 100644 --- a/tests/ounit/lustre/testLustreFrontend.ml +++ b/tests/ounit/lustre/testLustreFrontend.ml @@ -162,6 +162,14 @@ let _ = run_test_tt_main ("frontend LustreSyntaxChecks error tests" >::: [ match load_file "./lustreSyntaxChecks/pre_of_quantified_var.lus" with | Error (`LustreSyntaxChecksError (_, QuantifiedVariableInPre _)) -> true | _ -> false); + mk_test "test opaque node without a contract" (fun () -> + match load_file "./lustreSyntaxChecks/opaque_no_contract.lus" with + | Error (`LustreSyntaxChecksError (_, OpaqueWithoutContract _)) -> true + | _ -> false); + mk_test "test transparent node without a body" (fun () -> + match load_file "./lustreSyntaxChecks/transparent_no_body.lus" with + | Error (`LustreSyntaxChecksError (_, TransparentWithoutBody _)) -> true + | _ -> false); ]) (* *************************************************************************** *)