From b37575b48c3a97388a5daf94df1211ca82a406fc Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 20 Jan 2025 13:16:16 -0600 Subject: [PATCH 01/11] Account for contract imports in environment realizability checks --- src/lustre/lustreGenRefTypeImpNodes.ml | 80 ++++++++++++++++++++----- src/lustre/lustreGenRefTypeImpNodes.mli | 3 +- src/lustre/lustreInput.ml | 9 +-- src/lustre/lustreTypeChecker.mli | 6 ++ 4 files changed, 77 insertions(+), 21 deletions(-) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index f50f98889..4cda4a03f 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -28,6 +28,37 @@ let unwrap = function | Ok x -> x | Error _ -> assert false +let contract_node_decl_to_contracts += fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> + let contract' = List.filter_map (fun ci -> + match ci with + | A.GhostConst _ | GhostVars _ -> Some ci + | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr)) + | A.ContractCall (pos, name, ty_args, ips, ops) -> + let name = HString.concat2 (HString.mk_hstring ".inputs_") name in + Some (A.ContractCall (pos, name, ty_args, ips, ops)) + | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None + ) base_contract in + let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in + let inputs2, outputs2 = + List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, + List.map (fun (p, id, ty, cl, _) -> (p, id, ty, cl)) inputs + in + (* Since we are omitting assumptions from environment realizability checks, + we need to chase base types for environment inputs *) + let inputs2 = List.map (fun (p, id, ty, cl, b) -> + let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in + (p, id, ty, cl, b) + ) inputs2 in + (* We generate two imported nodes: One for the input node's contract (w/ type info), and another + for the input node's inputs/environment *) + let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in + if Flags.Contracts.check_environment () + then + let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in + [environment], ctx + else [], ctx + let node_decl_to_contracts = fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) -> let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in @@ -35,7 +66,10 @@ let node_decl_to_contracts match ci with | A.GhostConst _ | GhostVars _ -> Some ci | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr)) - | _ -> None + | A.ContractCall (pos, name, ty_args, ips, ops) -> + let name = HString.concat2 (HString.mk_hstring ".inputs_") name in + Some (A.ContractCall (pos, name, ty_args, ips, ops)) + | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None ) base_contract in let locals_as_outputs = List.map (fun local_decl -> match local_decl with | A.NodeConstDecl (pos, FreeConst (_, id, ty)) @@ -64,11 +98,20 @@ let node_decl_to_contracts for the input node's inputs/environment *) if extern then let environment = gen_node_id, extern, A.Opaque, params, inputs2, outputs2, [], node_items, contract' in - if Flags.Contracts.check_environment () then [environment] else [] + if Flags.Contracts.check_environment () then + let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in + [environment], ctx + else [], ctx else 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] + if Flags.Contracts.check_environment () then + let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in + let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in + [environment; contract], ctx + else + let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in + [contract], ctx (* NOTE: Currently, we do not allow global constants to have refinement types. If we decide to support this in the future, then we need to add necessary refinement type information @@ -83,36 +126,41 @@ let type_to_contract: Lib.position -> HString.t -> A.lustre_type -> HString.t li let node_items = [A.AnnotMain(pos, true)] in 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 +let gen_imp_nodes : Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context = fun ctx decls -> - List.fold_left (fun acc decl -> + let decls, ctx = List.fold_left (fun (acc_decls, acc_ctx) decl -> match decl with | A.ConstDecl (_, FreeConst _) - | A.ConstDecl (_, TypedConst _) -> acc + | A.ConstDecl (_, TypedConst _) -> acc_decls, acc_ctx | A.TypeDecl (_, AliasType (p, id, ps, ty)) -> (match type_to_contract p id ty ps with - | Some decl1 -> decl1 :: acc - | None -> acc) + | Some decl1 -> decl1 :: acc_decls, acc_ctx + | None -> acc_decls, acc_ctx) | A.TypeDecl (_, FreeType _) - | A.ConstDecl (_, UntypedConst _) -> acc + | A.ConstDecl (_, UntypedConst _) -> acc_decls, acc_ctx | 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, 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, acc_ctx = node_decl_to_contracts span.start_pos acc_ctx node_decl in let decls = List.map (fun decl -> A.NodeDecl (span, decl)) decls in - A.NodeDecl(span, node_decl) :: decls @ acc + A.NodeDecl(span, node_decl) :: decls @ acc_decls, acc_ctx | 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, 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 + let decls, acc_ctx = node_decl_to_contracts span.start_pos acc_ctx func_decl in let decls = List.map (fun decl -> A.FuncDecl (span, decl)) decls in - A.FuncDecl(span, func_decl) :: decls @ acc - | A.ContractNodeDecl _ - | A.NodeParamInst _ -> decl :: acc - ) [] decls |> List.rev \ No newline at end of file + A.FuncDecl(span, func_decl) :: decls @ acc_decls, acc_ctx + | A.ContractNodeDecl (span, contract_node_decl) -> + let decls, acc_ctx = contract_node_decl_to_contracts acc_ctx contract_node_decl in + let decls = List.map (fun decl -> A.ContractNodeDecl (span, decl)) decls in + A.ContractNodeDecl (span, contract_node_decl) :: decls @ acc_decls, acc_ctx + | A.NodeParamInst _ -> decl :: acc_decls, acc_ctx + ) ([], ctx) decls + in + List.rev decls, ctx \ No newline at end of file diff --git a/src/lustre/lustreGenRefTypeImpNodes.mli b/src/lustre/lustreGenRefTypeImpNodes.mli index 2b73979d8..1d072dd72 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.mli +++ b/src/lustre/lustreGenRefTypeImpNodes.mli @@ -19,10 +19,11 @@ module A = LustreAst +module Ctx = TypeCheckerContext val inputs_tag : string val contract_tag : string val type_tag : string val poly_gen_node_tag : string -val gen_imp_nodes : TypeCheckerContext.tc_context -> A.declaration list -> A.declaration list +val gen_imp_nodes : Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 290370788..65c53d92b 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -173,12 +173,13 @@ let type_check declarations = LspInfo.print_ast_info global_ctx declarations; (* Step 9. Generate imported nodes associated with refinement types if realizability checking is enabled *) - let sorted_node_contract_decls = + let sorted_node_contract_decls, global_ctx = if List.mem `CONTRACTCK (Flags.enabled ()) then - LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts @ - LGI.gen_imp_nodes global_ctx sorted_node_contract_decls - else sorted_node_contract_decls + let decls1, ctx1 = LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts in + let decls2, ctx2 = LGI.gen_imp_nodes global_ctx sorted_node_contract_decls in + decls1 @ decls2, TypeCheckerContext.union ctx1 ctx2 + else sorted_node_contract_decls, global_ctx in (* Step 10. Remove multiple assignment from if blocks and frame blocks *) diff --git a/src/lustre/lustreTypeChecker.mli b/src/lustre/lustreTypeChecker.mli index dbd0b715a..be9175862 100644 --- a/src/lustre/lustreTypeChecker.mli +++ b/src/lustre/lustreTypeChecker.mli @@ -190,6 +190,12 @@ val infer_type_expr: tc_context -> HString.t option -> LA.expr -> (tc_type * [> val eq_lustre_type : tc_context -> LA.lustre_type -> LA.lustre_type -> (bool, [> error]) result (** Check if two lustre types are equal *) +val tc_ctx_of_contract_node_decl: Lib.position -> tc_context + -> LA.contract_node_decl + -> (tc_context * [> warning] list, [> error]) result + +val tc_ctx_of_node_decl: Lib.position -> tc_context -> LA.node_decl -> (tc_context * [> warning] list, [> error]) result + (* Local Variables: compile-command: "make -k -C .." From 1395d343f392a0ceaa6d54dda38b19ccd4b55d6b Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 21 Jan 2025 12:06:14 -0600 Subject: [PATCH 02/11] Minor comments/whitespace updates before opening PR --- src/lustre/lustreGenRefTypeImpNodes.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 4cda4a03f..72dcce26b 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -50,11 +50,11 @@ let contract_node_decl_to_contracts let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in (p, id, ty, cl, b) ) inputs2 in - (* We generate two imported nodes: One for the input node's contract (w/ type info), and another - for the input node's inputs/environment *) + (* We generate a contract representing this contract's inputs/environment *) let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in if Flags.Contracts.check_environment () then + (* Update ctx with info about the generated contract *) let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in [environment], ctx else [], ctx @@ -94,11 +94,12 @@ let node_decl_to_contracts let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in (p, id, ty, cl, b) ) inputs2 in - (* We generate two imported nodes: One for the input node's contract (w/ type info), and another + (* We potentially 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, A.Opaque, params, inputs2, outputs2, [], node_items, contract' in if Flags.Contracts.check_environment () then + (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in [environment], ctx else [], ctx @@ -106,10 +107,12 @@ let node_decl_to_contracts 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 + (* Update ctx with info about the generated nodes *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in [environment; contract], ctx else + (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in [contract], ctx @@ -126,7 +129,7 @@ let type_to_contract: Lib.position -> HString.t -> A.lustre_type -> HString.t li let node_items = [A.AnnotMain(pos, true)] in 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 * Ctx.tc_context +let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context = fun ctx decls -> let decls, ctx = List.fold_left (fun (acc_decls, acc_ctx) decl -> match decl with From ae49d99e7bb547325ef82ab9506d4ba686204a0a Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Thu, 23 Jan 2025 10:06:11 -0600 Subject: [PATCH 03/11] In generated contract calls for env realizability checks, swap inputs and outputs --- src/lustre/generatedIdentifiers.ml | 3 + src/lustre/generatedIdentifiers.mli | 1 + src/lustre/lustreAstNormalizer.ml | 28 +++--- src/lustre/lustreDesugarFrameBlocks.ml | 8 +- src/lustre/lustreGenRefTypeImpNodes.ml | 128 ++++++++++++++++++------ src/lustre/lustreGenRefTypeImpNodes.mli | 3 +- src/lustre/lustreInput.ml | 15 +-- src/lustre/lustreNodeGen.ml | 16 ++- src/lustre/lustreRemoveMultAssign.ml | 6 +- src/lustre/lustreRemoveMultAssign.mli | 2 +- src/utils/lib.ml | 6 ++ src/utils/lib.mli | 3 + 12 files changed, 153 insertions(+), 66 deletions(-) diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index 91a0b7b74..e098904ee 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -47,6 +47,7 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; + gen_ghost_vars : HString.t list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) @@ -112,6 +113,7 @@ let union ids1 ids2 = { node_args = ids1.node_args @ ids2.node_args; oracles = ids1.oracles @ ids2.oracles; ib_oracles = ids1.ib_oracles @ ids2.ib_oracles; + gen_ghost_vars = ids1.gen_ghost_vars @ ids2.gen_ghost_vars; calls = ids1.calls @ ids2.calls; contract_calls = StringMap.merge union_keys ids1.contract_calls ids2.contract_calls; @@ -138,6 +140,7 @@ let empty () = { node_args = []; oracles = []; ib_oracles = []; + gen_ghost_vars = []; calls = []; contract_calls = StringMap.empty; subrange_constraints = []; diff --git a/src/lustre/generatedIdentifiers.mli b/src/lustre/generatedIdentifiers.mli index 4e950a497..d396f2c9d 100644 --- a/src/lustre/generatedIdentifiers.mli +++ b/src/lustre/generatedIdentifiers.mli @@ -47,6 +47,7 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; + gen_ghost_vars : HString.t list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 75ce699f0..25c55eb26 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -207,12 +207,6 @@ type info = { inlinable_funcs : LustreAst.node_decl StringMap.t; } -let split3 triples = - let xs = List.map (fun (x, _, _) -> x) triples in - let ys = List.map (fun (_, y, _) -> y) triples in - let zs = List.map (fun (_, _, z) -> z) triples in - xs, ys, zs - let pp_print_generated_identifiers ppf gids = let locals_list = StringMap.bindings gids.locals in let array_ctor_list = StringMap.bindings gids.array_constructors @@ -285,11 +279,13 @@ let pp_print_generated_identifiers ppf gids = A.pp_print_eq_lhs lhs A.pp_print_expr expr in - Format.fprintf ppf "%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n" + Format.fprintf ppf "%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n" (pp_print_list pp_print_oracle "\n") gids.oracles (pp_print_list pp_print_array_ctor "\n") array_ctor_list (pp_print_list pp_print_node_arg "\n") gids.node_args (pp_print_list pp_print_local "\n") locals_list + (pp_print_list pp_print_local "\n") gids.ib_oracles + (pp_print_list HString.pp_print_hstring "\n") gids.gen_ghost_vars (pp_print_list pp_print_call "\n") gids.calls (pp_print_list pp_print_subrange_constraint "\n") gids.subrange_constraints (pp_print_list pp_print_refinement_type_constraint "\n") gids.refinement_type_constraints @@ -1136,7 +1132,7 @@ and normalize_gid_equations info gids_map node_id = let nexpr, gids, warnings = normalize_expr info node_id gids_map expr in gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr) ) gids.equations in - let gids_list, warnings, eqs = split3 res in + let gids_list, warnings, eqs = Lib.split3 res in (* Take out old equations that were not normalized *) let gids = { gids with equations = [] } in let gids = List.fold_left (fun acc g -> union g acc) gids gids_list in @@ -1166,11 +1162,11 @@ and normalize_node_contract info node_id map cref inputs outputs (id, _, ivars, let ivars, gids1, warnings1 = List.map (fun (p, id, ty, cl, c) -> let ty, gids, warnings = normalize_ty info node_id map id ty in (p, id, ty, cl, c), gids, warnings - ) ivars |> split3 in + ) ivars |> Lib.split3 in let ovars, gids2, warnings2 = List.map (fun (p, id, ty, cl) -> let ty, gids, warnings = normalize_ty info node_id map id ty in (p, id, ty, cl), gids, warnings - ) ovars |> split3 in + ) ovars |> Lib.split3 in let contract_ref = cref in let ivars_names = List.map (fun (_, id, _, _, _) -> id) ivars in let ovars_names = List.map (fun (_, id, _, _) -> id) ovars in @@ -1260,11 +1256,11 @@ and normalize_node info map let inputs, gids1, warnings1 = List.map (fun (p, id, ty, cl, c) -> let ty, gids, warnings = normalize_ty info node_id map id ty in (p, id, ty, cl, c), gids, warnings - ) inputs |> split3 in + ) inputs |> Lib.split3 in let outputs, gids2, warnings2 = List.map (fun (p, id, ty, cl) -> let ty, gids, warnings = normalize_ty info node_id map id ty in (p, id, ty, cl), gids, warnings - ) outputs |> split3 in + ) outputs |> Lib.split3 in let locals, gids3, warnings3 = List.map (fun decl -> match decl with | A.NodeConstDecl (p1, FreeConst (p2, id, ty)) -> @@ -1278,7 +1274,7 @@ and normalize_node info map | A.NodeVarDecl (p1, (p2, id, ty, cl)) -> let ty, gids, warnings = normalize_ty info node_id map id ty in A.NodeVarDecl (p1, (p2, id, ty, cl)), gids, warnings - ) locals |> split3 in + ) locals |> Lib.split3 in (* Record subrange and refinement type constraints on inputs, outputs *) let gids4 = let vars = List.map (fun (p,id,ty,_,_) -> (p,id,ty)) inputs in @@ -1619,7 +1615,7 @@ and normalize_contract info node_id map ivars ovars (p, items) = | Some (ivar, ty) -> let size = extract_array_size ty in let expanded_expr = expand_node_calls_in_place info node_id ivar size expr in - let exprs, gids, warnings = split3 (List.init lhs_arity + let exprs, gids, warnings = Lib.split3 (List.init lhs_arity ( fun i -> let info = { info with local_group_projection = i } in @@ -1668,7 +1664,7 @@ and normalize_contract info node_id map ivars ovars (p, items) = warnings else (pos, i, ty), gids, [] ) - tis |> split3 + tis |> Lib.split3 ) in tis, List.fold_left union (empty ()) gids_list, List.flatten warnings ) in @@ -1740,7 +1736,7 @@ and normalize_equation info node_id map = function | Some (ivar, ty) -> let size = extract_array_size ty in let expanded_expr = expand_node_calls_in_place info node_id ivar size expr in - let exprs, gids, warnings = split3 (List.init lhs_arity + let exprs, gids, warnings = Lib.split3 (List.init lhs_arity (fun i -> let info = { info with local_group_projection = i } in normalize_expr info node_id map expanded_expr)) diff --git a/src/lustre/lustreDesugarFrameBlocks.ml b/src/lustre/lustreDesugarFrameBlocks.ml index ea1ae4344..c6340e506 100644 --- a/src/lustre/lustreDesugarFrameBlocks.ml +++ b/src/lustre/lustreDesugarFrameBlocks.ml @@ -72,12 +72,6 @@ let warn_unguarded_pres nis pos = | _ -> [] ) nis -let split3 triples = - let xs = List.map (fun (x, _, _) -> x) triples in - let ys = List.map (fun (_, y, _) -> y) triples in - let zs = List.map (fun (_, _, z) -> z) triples in - xs, ys, zs - (** Parses an expression and replaces any ITE oracles with the 'fill' expression (which is stuttering, ie, 'pre variable'). *) @@ -341,7 +335,7 @@ let desugar_frame_blocks sorted_node_contract_decls = let desugar_node_decl decl = (match decl with | 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 decls, nis, warnings = Lib.split3 res in let warnings = List.flatten warnings in R.ok (A.NodeDecl (s, (node_id, b, o, nps, cctds, ctds, (List.flatten decls) @ nlds, List.flatten nis, co)), warnings) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 72dcce26b..c9bb32d0d 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -18,6 +18,7 @@ module A = LustreAst module Chk = LustreTypeChecker module Ctx = TypeCheckerContext +module GI = GeneratedIdentifiers let inputs_tag = ".inputs_" let contract_tag = ".contract_" @@ -28,17 +29,52 @@ let unwrap = function | Ok x -> x | Error _ -> assert false +(* [i] is module state used to guarantee newly created identifiers are unique *) +let i = ref 0 + +let mk_fresh_ghost_var () = + i := !i + 1; + let prefix = HString.mk_hstring (string_of_int !i) in + let name = HString.concat2 prefix (HString.mk_hstring "_ghost") in + let gids = { (GI.empty ()) with + gen_ghost_vars = [name]; + } in + name, gids + let contract_node_decl_to_contracts = fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> - let contract' = List.filter_map (fun ci -> + let contract', gids = List.filter_map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some ci - | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr)) + | A.GhostConst _ | GhostVars _ -> Some ([ci], GI.empty ()) + | A.Assume (pos, name, b, expr) -> Some ([A.Guarantee (pos, name, b, expr)], GI.empty ()) | A.ContractCall (pos, name, ty_args, ips, ops) -> let name = HString.concat2 (HString.mk_hstring ".inputs_") name in - Some (A.ContractCall (pos, name, ty_args, ips, ops)) + (* Since we are flipping the inputs and outputs of the generated contract, + we also need to flip inputs and outputs of the call *) + let ips' = List.map (fun id -> A.Ident (pos, id)) ops in + let ops', gen_ghost_variables, gids = List.mapi (fun i expr -> match expr with + | A.Ident (_, id) -> id, [], GI.empty () + (* Input is not a simple identifier, so we have to generate a ghost variable + to store the output *) + | expr -> + let called_contract_ty = Ctx.lookup_contract_ty ctx name in + let ghost_var_ty = match Option.get called_contract_ty with + | TArr (_, _, GroupType (_, tys)) -> + List.nth tys i + | TArr(_, _, ty) when i = 1 -> ty + | _ -> assert false + in + let gen_ghost_var, gids = mk_fresh_ghost_var () in + gen_ghost_var, + [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], + gids + ) ips |> Lib.split3 in + Some ( + List.flatten gen_ghost_variables @ [A.ContractCall (pos, name, ty_args, ips', ops')], + List.fold_left GI.union ( GI.empty ()) gids + ) | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None - ) base_contract in + ) base_contract |> List.split in let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in let inputs2, outputs2 = List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, @@ -50,27 +86,52 @@ let contract_node_decl_to_contracts let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in (p, id, ty, cl, b) ) inputs2 in + let contract' = List.flatten contract' in (* We generate a contract representing this contract's inputs/environment *) let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in + let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in if Flags.Contracts.check_environment () then (* Update ctx with info about the generated contract *) let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in - [environment], ctx - else [], ctx + [environment], ctx, gids + else [], ctx, gids let node_decl_to_contracts = 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 -> + let contract', gids = List.filter_map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some ci - | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr)) + | A.GhostConst _ | GhostVars _ -> Some ([ci], GI.empty ()) + | A.Assume (pos, name, b, expr) -> Some ([A.Guarantee (pos, name, b, expr)], GI.empty ()) | A.ContractCall (pos, name, ty_args, ips, ops) -> let name = HString.concat2 (HString.mk_hstring ".inputs_") name in - Some (A.ContractCall (pos, name, ty_args, ips, ops)) + (* Since we are flipping the inputs and outputs of the generated contract, + we also need to flip inputs and outputs of the call *) + let ips' = List.map (fun id -> A.Ident (pos, id)) ops in + let ops', gen_ghost_variables, gids = List.mapi (fun i expr -> match expr with + | A.Ident (_, id) -> id, [], GI.empty () + (* Input is not a simple identifier, so we have to generate a ghost variable + to store the output *) + | expr -> + let called_contract_ty = Ctx.lookup_contract_ty ctx name in + let ghost_var_ty = match Option.get called_contract_ty with + | TArr (_, _, GroupType (_, tys)) -> + List.nth tys i + | TArr(_, _, ty) when i = 1 -> ty + | _ -> assert false + in + let gen_ghost_var, gids = mk_fresh_ghost_var () in + gen_ghost_var, + [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], + gids + ) ips |> Lib.split3 in + Some ( + List.flatten gen_ghost_variables @ [A.ContractCall (pos, name, ty_args, ips', ops')], + List.fold_left GI.union ( GI.empty ()) gids + ) | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None - ) base_contract in + ) base_contract |> List.split in let locals_as_outputs = List.map (fun local_decl -> match local_decl with | A.NodeConstDecl (pos, FreeConst (_, id, ty)) | A.NodeConstDecl (pos, TypedConst (_, id, _, ty)) -> Some (pos, id, ty, A.ClockTrue) @@ -78,6 +139,7 @@ let node_decl_to_contracts Some (pos, id, ty, cl) | _ -> None ) locals |> List.filter_map Fun.id in + let contract' = List.flatten contract' in let contract' = if contract' = [] then None else Some (pos, contract') in let extern' = true in (* To prevent slicing, we mark generated imported nodes as main nodes *) @@ -94,6 +156,7 @@ let node_decl_to_contracts let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in (p, id, ty, cl, b) ) inputs2 in + let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in (* We potentially 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 @@ -101,8 +164,8 @@ let node_decl_to_contracts if Flags.Contracts.check_environment () then (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in - [environment], ctx - else [], ctx + [environment], ctx, gids + else [], ctx, gids else 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 @@ -110,11 +173,11 @@ let node_decl_to_contracts (* Update ctx with info about the generated nodes *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in - [environment; contract], ctx + [environment; contract], ctx, gids else (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in - [contract], ctx + [contract], ctx, gids (* NOTE: Currently, we do not allow global constants to have refinement types. If we decide to support this in the future, then we need to add necessary refinement type information @@ -129,41 +192,44 @@ let type_to_contract: Lib.position -> HString.t -> A.lustre_type -> HString.t li let node_items = [A.AnnotMain(pos, true)] in 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 * Ctx.tc_context +let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context * GI.t HString.HStringMap.t = fun ctx decls -> - let decls, ctx = List.fold_left (fun (acc_decls, acc_ctx) decl -> + let decls, ctx, gids = List.fold_left (fun (acc_decls, acc_ctx, acc_gids) decl -> match decl with | A.ConstDecl (_, FreeConst _) - | A.ConstDecl (_, TypedConst _) -> acc_decls, acc_ctx + | A.ConstDecl (_, TypedConst _) -> acc_decls, acc_ctx, acc_gids | A.TypeDecl (_, AliasType (p, id, ps, ty)) -> (match type_to_contract p id ty ps with - | Some decl1 -> decl1 :: acc_decls, acc_ctx - | None -> acc_decls, acc_ctx) + | Some decl1 -> decl1 :: acc_decls, acc_ctx, acc_gids + | None -> acc_decls, acc_ctx, acc_gids) | A.TypeDecl (_, FreeType _) - | A.ConstDecl (_, UntypedConst _) -> acc_decls, acc_ctx + | A.ConstDecl (_, UntypedConst _) -> acc_decls, acc_ctx, acc_gids | 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, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else node_decl in - let decls, acc_ctx = node_decl_to_contracts span.start_pos acc_ctx node_decl in + let decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx node_decl in let decls = List.map (fun decl -> A.NodeDecl (span, decl)) decls in - A.NodeDecl(span, node_decl) :: decls @ acc_decls, acc_ctx + A.NodeDecl(span, node_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids | 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, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else func_decl in - let decls, acc_ctx = node_decl_to_contracts span.start_pos acc_ctx func_decl in + let decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx func_decl in let decls = List.map (fun decl -> A.FuncDecl (span, decl)) decls in - A.FuncDecl(span, func_decl) :: decls @ acc_decls, acc_ctx + A.FuncDecl(span, func_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids | A.ContractNodeDecl (span, contract_node_decl) -> - let decls, acc_ctx = contract_node_decl_to_contracts acc_ctx contract_node_decl in + let decls, acc_ctx, gids = contract_node_decl_to_contracts acc_ctx contract_node_decl in let decls = List.map (fun decl -> A.ContractNodeDecl (span, decl)) decls in - A.ContractNodeDecl (span, contract_node_decl) :: decls @ acc_decls, acc_ctx - | A.NodeParamInst _ -> decl :: acc_decls, acc_ctx - ) ([], ctx) decls + A.ContractNodeDecl (span, contract_node_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids + | A.NodeParamInst _ -> decl :: acc_decls, acc_ctx, acc_gids + ) ([], ctx, GI.StringMap.empty) decls in - List.rev decls, ctx \ No newline at end of file + List.rev decls, ctx, gids \ No newline at end of file diff --git a/src/lustre/lustreGenRefTypeImpNodes.mli b/src/lustre/lustreGenRefTypeImpNodes.mli index 1d072dd72..4eeb7a3da 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.mli +++ b/src/lustre/lustreGenRefTypeImpNodes.mli @@ -20,10 +20,11 @@ module A = LustreAst module Ctx = TypeCheckerContext +module GI = GeneratedIdentifiers val inputs_tag : string val contract_tag : string val type_tag : string val poly_gen_node_tag : string -val gen_imp_nodes : Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context +val gen_imp_nodes : Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context * GI.t HString.HStringMap.t diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 65c53d92b..424c157ad 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -49,6 +49,7 @@ module LFR = LustreFlattenRefinementTypes module LGI = LustreGenRefTypeImpNodes module LIP = LustreInstantiatePolyNodes module LUF = LustreUserFunctions +module GI = GeneratedIdentifiers type error = [ | `LustreArrayDependencies of Lib.position * LustreArrayDependencies.error_kind @@ -173,17 +174,19 @@ let type_check declarations = LspInfo.print_ast_info global_ctx declarations; (* Step 9. Generate imported nodes associated with refinement types if realizability checking is enabled *) - let sorted_node_contract_decls, global_ctx = + let sorted_node_contract_decls, global_ctx, gids = if List.mem `CONTRACTCK (Flags.enabled ()) then - let decls1, ctx1 = LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts in - let decls2, ctx2 = LGI.gen_imp_nodes global_ctx sorted_node_contract_decls in - decls1 @ decls2, TypeCheckerContext.union ctx1 ctx2 - else sorted_node_contract_decls, global_ctx + let decls1, ctx1, gids1 = LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts in + let decls2, ctx2, gids2 = LGI.gen_imp_nodes global_ctx sorted_node_contract_decls in + decls1 @ decls2, + TypeCheckerContext.union ctx1 ctx2, + GI.StringMap.merge GI.union_keys2 gids1 gids2 + else sorted_node_contract_decls, global_ctx, GI.StringMap.empty in (* Step 10. Remove multiple assignment from if blocks and frame blocks *) - let sorted_node_contract_decls, gids = RMA.remove_mult_assign global_ctx sorted_node_contract_decls in + let sorted_node_contract_decls, gids = RMA.remove_mult_assign global_ctx gids sorted_node_contract_decls in (* Step 11. Desugar imperative if block to ITEs *) let* (sorted_node_contract_decls, gids) = (LDI.desugar_if_blocks global_ctx sorted_node_contract_decls gids) in diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index c676887f6..eb59466a6 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1297,11 +1297,25 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con (id |> HString.mk_hstring |> mk_ident, [prefix; ref]) | _ -> assert false in + let extract_orig_name name = + let name = HString.string_of_hstring name in + let parts = String.split_on_char '_' name in + match parts with + | _ :: _ :: tail -> + let id = String.concat "_" tail in + id |> HString.mk_hstring + | _ -> assert false + in let over_vars (gvar_accum, eq_accum) = fun (pos, (A.GhostVarDec (_, tis)), expr) -> let extract_local ((_, id, ty)) = ( let expr_ident = mk_ident id in let (ident, contract_namespace) = extract_namespace id in let index_types = compile_ast_type cstate ctx map ty in + let source = + if List.mem (extract_orig_name id) gids.GI.gen_ghost_vars + then N.Generated + else N.Ghost + in let over_indices = fun index index_type accum -> ( let possible_state_var = ( mk_state_var @@ -1312,7 +1326,7 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con ident index index_type - (Some N.Ghost) + (Some source) ) in match possible_state_var with diff --git a/src/lustre/lustreRemoveMultAssign.ml b/src/lustre/lustreRemoveMultAssign.ml index aa9f72caf..7d931b994 100644 --- a/src/lustre/lustreRemoveMultAssign.ml +++ b/src/lustre/lustreRemoveMultAssign.ml @@ -173,7 +173,7 @@ let desugar_node_decl ctx decl = match decl with (** Desugars a declaration list to remove multiple assignment from if blocks and frame blocks. *) -let remove_mult_assign ctx sorted_node_contract_decls = - let decls, gids = List.map (desugar_node_decl ctx) sorted_node_contract_decls |> List.split in - let gids = List.fold_left (GI.StringMap.merge GI.union_keys2) GI.StringMap.empty gids in +let remove_mult_assign ctx gids sorted_node_contract_decls = + let decls, gids2 = List.map (desugar_node_decl ctx) sorted_node_contract_decls |> List.split in + let gids = List.fold_left (GI.StringMap.merge GI.union_keys2) gids gids2 in decls, gids diff --git a/src/lustre/lustreRemoveMultAssign.mli b/src/lustre/lustreRemoveMultAssign.mli index 81e1ad927..83d970056 100644 --- a/src/lustre/lustreRemoveMultAssign.mli +++ b/src/lustre/lustreRemoveMultAssign.mli @@ -43,4 +43,4 @@ (** Desugars a declaration list to remove multiple assignment from if blocks and frame blocks. *) -val remove_mult_assign : TypeCheckerContext.tc_context -> LustreAst.declaration list -> LustreAst.declaration list * GeneratedIdentifiers.t GeneratedIdentifiers.StringMap.t +val remove_mult_assign : TypeCheckerContext.tc_context -> GeneratedIdentifiers.t HString.HStringMap.t -> LustreAst.declaration list -> LustreAst.declaration list * GeneratedIdentifiers.t GeneratedIdentifiers.StringMap.t diff --git a/src/utils/lib.ml b/src/utils/lib.ml index e973c6cbc..28c81922e 100644 --- a/src/utils/lib.ml +++ b/src/utils/lib.ml @@ -1349,6 +1349,12 @@ let split_dot s = let n = (index s '.') in sub s 0 n, sub s (n+1) (length s - n - 1) +let split3 triples = + let xs = List.map (fun (x, _, _) -> x) triples in + let ys = List.map (fun (_, y, _) -> y) triples in + let zs = List.map (fun (_, _, z) -> z) triples in + xs, ys, zs + (* Extract scope from a concatenated name *) let extract_scope_name name = diff --git a/src/utils/lib.mli b/src/utils/lib.mli index 532967d1b..32f206d8e 100644 --- a/src/utils/lib.mli +++ b/src/utils/lib.mli @@ -147,6 +147,9 @@ val list_suffix : 'a list -> int -> 'a list the second will contain all indices from [n,len) *) val list_split : int -> 'a list -> ('a list * 'a list) +(** [split3 l] takes a list of triples and produces a triple of lists *) +val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list + (** [chain_list \[e1; e2; ...\]] is [\[\[e1; e2\]; \[e2; e3\]; ... \]] *) val chain_list : 'a list -> 'a list list From 0f5fd548fa695f6b2e45ee2b51c14668b7beca2d Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Thu, 23 Jan 2025 10:54:53 -0600 Subject: [PATCH 04/11] WIP: Move gen ghost local info to gids --- src/lustre/generatedIdentifiers.ml | 2 +- src/lustre/generatedIdentifiers.mli | 2 +- src/lustre/lustreAstNormalizer.ml | 3 ++- src/lustre/lustreGenRefTypeImpNodes.ml | 11 ++++++----- src/lustre/lustreNodeGen.ml | 13 +++++++++++-- 5 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index e098904ee..9f9938af6 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -47,7 +47,7 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; - gen_ghost_vars : HString.t list; + gen_ghost_vars : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) diff --git a/src/lustre/generatedIdentifiers.mli b/src/lustre/generatedIdentifiers.mli index d396f2c9d..0effe48bb 100644 --- a/src/lustre/generatedIdentifiers.mli +++ b/src/lustre/generatedIdentifiers.mli @@ -47,7 +47,7 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; - gen_ghost_vars : HString.t list; + gen_ghost_vars : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 25c55eb26..889b57ad3 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -285,7 +285,7 @@ let pp_print_generated_identifiers ppf gids = (pp_print_list pp_print_node_arg "\n") gids.node_args (pp_print_list pp_print_local "\n") locals_list (pp_print_list pp_print_local "\n") gids.ib_oracles - (pp_print_list HString.pp_print_hstring "\n") gids.gen_ghost_vars + (pp_print_list pp_print_oracle "\n") gids.gen_ghost_vars (pp_print_list pp_print_call "\n") gids.calls (pp_print_list pp_print_subrange_constraint "\n") gids.subrange_constraints (pp_print_list pp_print_refinement_type_constraint "\n") gids.refinement_type_constraints @@ -1123,6 +1123,7 @@ let rec normalize ctx ai_ctx inlinable_funcs (decls:LustreAst.t) gids = Res.ok (ast, map, warnings) +(*!! TODO: Extend this for gen_ghost_vars(?) *) and normalize_gid_equations info gids_map node_id = match StringMap.find_opt node_id gids_map with | None -> empty(), [] diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index c9bb32d0d..29ac36016 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -32,12 +32,12 @@ let unwrap = function (* [i] is module state used to guarantee newly created identifiers are unique *) let i = ref 0 -let mk_fresh_ghost_var () = +let mk_fresh_ghost_var ty rhs = i := !i + 1; let prefix = HString.mk_hstring (string_of_int !i) in let name = HString.concat2 prefix (HString.mk_hstring "_ghost") in let gids = { (GI.empty ()) with - gen_ghost_vars = [name]; + gen_ghost_vars = [name, ty, rhs]; } in name, gids @@ -64,7 +64,7 @@ let contract_node_decl_to_contracts | TArr(_, _, ty) when i = 1 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var () in + let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in gen_ghost_var, [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], gids @@ -121,9 +121,10 @@ let node_decl_to_contracts | TArr(_, _, ty) when i = 1 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var () in + let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in gen_ghost_var, - [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], + (* [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], *) + [], gids ) ips |> Lib.split3 in Some ( diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index eb59466a6..74172702f 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1306,13 +1306,22 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con id |> HString.mk_hstring | _ -> assert false in + let gen_gvars = gids.GI.gen_ghost_vars in + let gen_gvars = List.map (fun (id, ty, expr) -> + let pos = AH.pos_of_expr expr in + pos, A.GhostVarDec (pos, [(pos, id, ty)]), expr + ) gen_gvars in let over_vars (gvar_accum, eq_accum) = fun (pos, (A.GhostVarDec (_, tis)), expr) -> let extract_local ((_, id, ty)) = ( let expr_ident = mk_ident id in let (ident, contract_namespace) = extract_namespace id in let index_types = compile_ast_type cstate ctx map ty in + let gen_ghost_vars = List.map (fun (a, _, _) -> a) gids.GI.gen_ghost_vars in + HString.pp_print_hstring Format.std_formatter id; + print_endline "got here"; let source = - if List.mem (extract_orig_name id) gids.GI.gen_ghost_vars + (* if List.mem (extract_orig_name id) gen_ghost_vars *) + if List.mem id gen_ghost_vars then N.Generated else N.Ghost in @@ -1341,7 +1350,7 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con let eq_lhs = A.StructDef (pos, struct_items) in let eq_rhs = expr in (List.map extract_local tis) @ gvar_accum, (pos, eq_lhs, eq_rhs) :: eq_accum - in List.fold_left over_vars ([], []) gvars + in List.fold_left over_vars ([], []) (gvars @ gen_gvars) (* ****************************************************************** *) (* Contract Modes *) (* ****************************************************************** *) From 49cd13dcbae3e825b5d61a841a5e5070edf26b78 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 28 Jan 2025 12:05:52 -0600 Subject: [PATCH 05/11] Finish pulling generated ghost variables out of Lustre AST --- src/lustre/generatedIdentifiers.ml | 6 ++- src/lustre/lustreAstNormalizer.ml | 65 ++++++++++++++++++++------ src/lustre/lustreGenRefTypeImpNodes.ml | 60 ++++++++++++------------ src/lustre/lustreNodeGen.ml | 19 +------- 4 files changed, 88 insertions(+), 62 deletions(-) diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index 9f9938af6..cb89ddfaa 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -113,7 +113,11 @@ let union ids1 ids2 = { node_args = ids1.node_args @ ids2.node_args; oracles = ids1.oracles @ ids2.oracles; ib_oracles = ids1.ib_oracles @ ids2.ib_oracles; - gen_ghost_vars = ids1.gen_ghost_vars @ ids2.gen_ghost_vars; + (* Prevent duplicates *) + gen_ghost_vars = List.fold_left (fun acc element -> + if (List.mem element acc) then acc + else element :: acc + ) ids1.gen_ghost_vars ids2.gen_ghost_vars; calls = ids1.calls @ ids2.calls; contract_calls = StringMap.merge union_keys ids1.contract_calls ids2.contract_calls; diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 889b57ad3..7c1cbb53f 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -1123,17 +1123,15 @@ let rec normalize ctx ai_ctx inlinable_funcs (decls:LustreAst.t) gids = Res.ok (ast, map, warnings) -(*!! TODO: Extend this for gen_ghost_vars(?) *) and normalize_gid_equations info gids_map node_id = match StringMap.find_opt node_id gids_map with | None -> empty(), [] | Some gids -> ( (* Normalize all equations in gids *) - let res = List.map (fun (_, _, lhs, expr) -> + let gids_list, warnings, eqs = List.map (fun (_, _, lhs, expr) -> let nexpr, gids, warnings = normalize_expr info node_id gids_map expr in gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr) - ) gids.equations in - let gids_list, warnings, eqs = Lib.split3 res in + ) gids.equations |> Lib.split3 in (* Take out old equations that were not normalized *) let gids = { gids with equations = [] } in let gids = List.fold_left (fun acc g -> union g acc) gids gids_list in @@ -1229,7 +1227,19 @@ and normalize_node_contract info node_id map cref inputs outputs (id, _, ivars, let vars = List.map (fun (p,id,ty,_) -> (p,id,ty)) ovars in add_ref_type_constraints info Output vars in - let nbody, gids7, warnings3 = normalize_contract info node_id map ivars ovars body in + let gen_gvars = match (StringMap.find_opt node_id map) with + | Some gids -> gids.gen_ghost_vars + (* FIXME: This should not happen; every node should have gids. + But, this is not currently the case, as monomorphization currently + (incorrectly) does not generate gids. This will be fixed in a future PR. *) + | None -> [] + in + let gen_gvars = List.map (fun (id, ty, expr) -> + let pos = AH.pos_of_expr expr in + let c_lhs = A.GhostVarDec (pos, [pos, id, ty]) in + A.GhostVars (pos, c_lhs, expr) + ) gen_gvars in + let nbody, gids7, warnings3 = normalize_contract info node_id map ivars ovars gen_gvars body in let gids = List.fold_left union (empty ()) [union_list gids1; union_list gids2; gids3; gids4; gids5; gids6; gids7] in nbody, gids, List.flatten (warnings1 @ warnings2) @ warnings3, StringMap.empty @@ -1297,8 +1307,20 @@ and normalize_node info map in let contract_ref = new_contract_reference () in let info = { info with context = ctx; contract_ref } in + let gen_gvars = match (StringMap.find_opt node_id map) with + | Some gids -> gids.gen_ghost_vars + (* FIXME: This should not happen; every node should have gids. + But, this is not currently the case, as monomorphization currently + (incorrectly) does not generate gids. This will be fixed in a future PR. *) + | None -> [] + in + let gen_gvars = List.map (fun (id, ty, expr) -> + let pos = AH.pos_of_expr expr in + let c_lhs = A.GhostVarDec (pos, [pos, id, ty]) in + A.GhostVars (pos, c_lhs, expr) + ) gen_gvars in let ncontracts, gids, warnings = - normalize_contract info node_id map inputs outputs contract in + normalize_contract info node_id map inputs outputs gen_gvars contract in (Some ncontracts), gids, warnings | None -> None, empty (), [] in @@ -1497,8 +1519,7 @@ and rename_ghost_variables info contract = let tail, info = rename_ghost_variables info t in (StringMap.singleton id new_id) :: tail, info (* Recurse through each declaration one at a time *) - | GhostVars (pos1, A.GhostVarDec(pos2, (_, id, _)::tis), e) :: t -> - let ty = Ctx.lookup_ty info.context id |> get in + | GhostVars (pos1, A.GhostVarDec(pos2, (_, id, ty)::tis), e) :: t -> let ty = Chk.expand_type_syn_reftype_history info.context ty |> unwrap in let new_id = HString.concat sep [info.contract_ref;id] in let info = { info with context = Ctx.add_ty info.context new_id ty } in @@ -1506,10 +1527,11 @@ and rename_ghost_variables info contract = (StringMap.singleton id new_id) :: tail, info | _ :: t -> rename_ghost_variables info t -and normalize_contract info node_id map ivars ovars (p, items) = +and normalize_contract info node_id map ivars ovars gen_ghost_vars (p, items) = let gids = ref (empty ()) in let warnings = ref [] in let result = ref [] in + let items = items @ gen_ghost_vars in let ghost_interp, info = rename_ghost_variables info items in let ghost_interp = List.fold_left (StringMap.merge union_keys) StringMap.empty ghost_interp @@ -1577,7 +1599,7 @@ and normalize_contract info node_id map ivars ovars (p, items) = in let called_node = StringMap.find name info.contract_calls_info in let (_, normalized_call), gids2, warnings2, interp = - normalize_node_contract info node_id map cref ninputs noutputs called_node + normalize_node_contract info name map cref ninputs noutputs called_node in let gids = union gids1 gids2 in let warnings = warnings1 @ warnings2 in @@ -1671,13 +1693,30 @@ and normalize_contract info node_id map ivars ovars (p, items) = ) in (* Get new identifiers for LHS *) - let tis = List.map (fun (p, id, ty) -> + let tis' = List.map (fun (p, id, ty) -> (p, StringMap.find id info.interpretation, ty) ) tis in - GhostVars (pos, GhostVarDec(pos2, tis), nexpr), - union (union gids1 gids2) gids3, + (* Update generated ghost var names in gids *) + let gids = union (union gids1 gids2) gids3 in + let curr_node_gids = match StringMap.find_opt node_id map with + | Some gids -> gids + (* FIXME: This should not happen; every node should have gids. + But, this is not currently the case, as monomorphization currently + (incorrectly) does not generate gids. This will be fixed in a future PR. *) + | None -> empty () + in + let updated_gen_ghost_vars = + List.map (fun (id, ty, expr) -> + StringMap.find id info.interpretation, ty, expr + ) curr_node_gids.gen_ghost_vars in + let gids = { gids with + gen_ghost_vars = updated_gen_ghost_vars + } in + + GhostVars (pos, GhostVarDec(pos2, tis'), nexpr), + gids, warnings @ warnings2, StringMap.empty diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 29ac36016..3aaeadfe7 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -48,7 +48,7 @@ let contract_node_decl_to_contracts | A.GhostConst _ | GhostVars _ -> Some ([ci], GI.empty ()) | A.Assume (pos, name, b, expr) -> Some ([A.Guarantee (pos, name, b, expr)], GI.empty ()) | A.ContractCall (pos, name, ty_args, ips, ops) -> - let name = HString.concat2 (HString.mk_hstring ".inputs_") name in + let name = HString.concat2 (HString.mk_hstring inputs_tag) name in (* Since we are flipping the inputs and outputs of the generated contract, we also need to flip inputs and outputs of the call *) let ips' = List.map (fun id -> A.Ident (pos, id)) ops in @@ -102,35 +102,36 @@ let node_decl_to_contracts let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in let contract', gids = List.filter_map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some ([ci], GI.empty ()) - | A.Assume (pos, name, b, expr) -> Some ([A.Guarantee (pos, name, b, expr)], GI.empty ()) + | A.GhostConst _ | GhostVars _ -> Some (ci, GI.empty ()) + | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr), GI.empty ()) | A.ContractCall (pos, name, ty_args, ips, ops) -> - let name = HString.concat2 (HString.mk_hstring ".inputs_") name in - (* Since we are flipping the inputs and outputs of the generated contract, - we also need to flip inputs and outputs of the call *) - let ips' = List.map (fun id -> A.Ident (pos, id)) ops in - let ops', gen_ghost_variables, gids = List.mapi (fun i expr -> match expr with - | A.Ident (_, id) -> id, [], GI.empty () - (* Input is not a simple identifier, so we have to generate a ghost variable - to store the output *) - | expr -> - let called_contract_ty = Ctx.lookup_contract_ty ctx name in - let ghost_var_ty = match Option.get called_contract_ty with - | TArr (_, _, GroupType (_, tys)) -> - List.nth tys i - | TArr(_, _, ty) when i = 1 -> ty - | _ -> assert false - in - let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in - gen_ghost_var, - (* [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], *) - [], - gids - ) ips |> Lib.split3 in - Some ( - List.flatten gen_ghost_variables @ [A.ContractCall (pos, name, ty_args, ips', ops')], - List.fold_left GI.union ( GI.empty ()) gids - ) + if Flags.Contracts.check_environment () then ( + let name = HString.concat2 (HString.mk_hstring inputs_tag) name in + (* Since we are flipping the inputs and outputs of the generated contract, + we also need to flip inputs and outputs of the call *) + let ips' = List.map (fun id -> A.Ident (pos, id)) ops in + let ops', gids = List.mapi (fun i expr -> match expr with + | A.Ident (_, id) -> id, GI.empty () + (* Input is not a simple identifier, so we have to generate a ghost variable + to store the output *) + | expr -> + let called_contract_ty = Ctx.lookup_contract_ty ctx name in + (* Option.get should not fail because we know the check_environment flag is enabled *) + let ghost_var_ty = match Option.get called_contract_ty with + | TArr (_, _, GroupType (_, tys)) -> + List.nth tys i + | TArr(_, _, ty) when i = 1 -> ty + | _ -> assert false + in + let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in + gen_ghost_var, + gids + ) ips |> List.split in + Some ( + A.ContractCall (pos, name, ty_args, ips', ops'), + List.fold_left GI.union ( GI.empty ()) gids + )) + else None | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None ) base_contract |> List.split in let locals_as_outputs = List.map (fun local_decl -> match local_decl with @@ -140,7 +141,6 @@ let node_decl_to_contracts Some (pos, id, ty, cl) | _ -> None ) locals |> List.filter_map Fun.id in - let contract' = List.flatten contract' in let contract' = if contract' = [] then None else Some (pos, contract') in let extern' = true in (* To prevent slicing, we mark generated imported nodes as main nodes *) diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index 74172702f..cb2f64238 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1297,30 +1297,13 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con (id |> HString.mk_hstring |> mk_ident, [prefix; ref]) | _ -> assert false in - let extract_orig_name name = - let name = HString.string_of_hstring name in - let parts = String.split_on_char '_' name in - match parts with - | _ :: _ :: tail -> - let id = String.concat "_" tail in - id |> HString.mk_hstring - | _ -> assert false - in - let gen_gvars = gids.GI.gen_ghost_vars in - let gen_gvars = List.map (fun (id, ty, expr) -> - let pos = AH.pos_of_expr expr in - pos, A.GhostVarDec (pos, [(pos, id, ty)]), expr - ) gen_gvars in let over_vars (gvar_accum, eq_accum) = fun (pos, (A.GhostVarDec (_, tis)), expr) -> let extract_local ((_, id, ty)) = ( let expr_ident = mk_ident id in let (ident, contract_namespace) = extract_namespace id in let index_types = compile_ast_type cstate ctx map ty in let gen_ghost_vars = List.map (fun (a, _, _) -> a) gids.GI.gen_ghost_vars in - HString.pp_print_hstring Format.std_formatter id; - print_endline "got here"; let source = - (* if List.mem (extract_orig_name id) gen_ghost_vars *) if List.mem id gen_ghost_vars then N.Generated else N.Ghost @@ -1350,7 +1333,7 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con let eq_lhs = A.StructDef (pos, struct_items) in let eq_rhs = expr in (List.map extract_local tis) @ gvar_accum, (pos, eq_lhs, eq_rhs) :: eq_accum - in List.fold_left over_vars ([], []) (gvars @ gen_gvars) + in List.fold_left over_vars ([], []) gvars (* ****************************************************************** *) (* Contract Modes *) (* ****************************************************************** *) From bcc93e7e7086ab03383cc376708c086ce235e412 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 28 Jan 2025 14:26:10 -0600 Subject: [PATCH 06/11] Fix bugs in generation of ghost variables --- src/lustre/lustreGenRefTypeImpNodes.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 3aaeadfe7..aaf279ebd 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -45,15 +45,15 @@ let contract_node_decl_to_contracts = fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> let contract', gids = List.filter_map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some ([ci], GI.empty ()) - | A.Assume (pos, name, b, expr) -> Some ([A.Guarantee (pos, name, b, expr)], GI.empty ()) + | A.GhostConst _ | GhostVars _ -> Some (ci, GI.empty ()) + | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr), GI.empty ()) | A.ContractCall (pos, name, ty_args, ips, ops) -> let name = HString.concat2 (HString.mk_hstring inputs_tag) name in (* Since we are flipping the inputs and outputs of the generated contract, we also need to flip inputs and outputs of the call *) let ips' = List.map (fun id -> A.Ident (pos, id)) ops in - let ops', gen_ghost_variables, gids = List.mapi (fun i expr -> match expr with - | A.Ident (_, id) -> id, [], GI.empty () + let ops', gids = List.mapi (fun i expr -> match expr with + | A.Ident (_, id) -> id, GI.empty () (* Input is not a simple identifier, so we have to generate a ghost variable to store the output *) | expr -> @@ -61,16 +61,15 @@ let contract_node_decl_to_contracts let ghost_var_ty = match Option.get called_contract_ty with | TArr (_, _, GroupType (_, tys)) -> List.nth tys i - | TArr(_, _, ty) when i = 1 -> ty + | TArr(_, _, ty) when i = 0 -> ty | _ -> assert false in let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in gen_ghost_var, - [A.GhostVars (pos, (GhostVarDec (pos, [(pos, gen_ghost_var, ghost_var_ty)])), expr)], gids - ) ips |> Lib.split3 in + ) ips |> List.split in Some ( - List.flatten gen_ghost_variables @ [A.ContractCall (pos, name, ty_args, ips', ops')], + A.ContractCall (pos, name, ty_args, ips', ops'), List.fold_left GI.union ( GI.empty ()) gids ) | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None @@ -86,7 +85,6 @@ let contract_node_decl_to_contracts let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in (p, id, ty, cl, b) ) inputs2 in - let contract' = List.flatten contract' in (* We generate a contract representing this contract's inputs/environment *) let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in From f2d79a23365ab46b696d9c15d831852d8c044da6 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 29 Jan 2025 13:34:13 -0600 Subject: [PATCH 07/11] Move generated ghost variables to generated locals field of gids --- src/lustre/generatedIdentifiers.ml | 7 --- src/lustre/generatedIdentifiers.mli | 1 - src/lustre/lustreAstNormalizer.ml | 65 +++++--------------------- src/lustre/lustreGenRefTypeImpNodes.ml | 9 ++-- src/lustre/lustreNodeGen.ml | 8 +--- 5 files changed, 17 insertions(+), 73 deletions(-) diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index cb89ddfaa..91a0b7b74 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -47,7 +47,6 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; - gen_ghost_vars : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) @@ -113,11 +112,6 @@ let union ids1 ids2 = { node_args = ids1.node_args @ ids2.node_args; oracles = ids1.oracles @ ids2.oracles; ib_oracles = ids1.ib_oracles @ ids2.ib_oracles; - (* Prevent duplicates *) - gen_ghost_vars = List.fold_left (fun acc element -> - if (List.mem element acc) then acc - else element :: acc - ) ids1.gen_ghost_vars ids2.gen_ghost_vars; calls = ids1.calls @ ids2.calls; contract_calls = StringMap.merge union_keys ids1.contract_calls ids2.contract_calls; @@ -144,7 +138,6 @@ let empty () = { node_args = []; oracles = []; ib_oracles = []; - gen_ghost_vars = []; calls = []; contract_calls = StringMap.empty; subrange_constraints = []; diff --git a/src/lustre/generatedIdentifiers.mli b/src/lustre/generatedIdentifiers.mli index 0effe48bb..4e950a497 100644 --- a/src/lustre/generatedIdentifiers.mli +++ b/src/lustre/generatedIdentifiers.mli @@ -47,7 +47,6 @@ type t = { StringMap.t; oracles : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; ib_oracles : (HString.t * LustreAst.lustre_type) list; - gen_ghost_vars : (HString.t * LustreAst.lustre_type * LustreAst.expr) list; calls : (Lib.position (* node call position *) * HString.t (* abstracted output *) * LustreAst.expr (* condition expression *) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 7c1cbb53f..688663fd7 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -279,13 +279,12 @@ let pp_print_generated_identifiers ppf gids = A.pp_print_eq_lhs lhs A.pp_print_expr expr in - Format.fprintf ppf "%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n" + Format.fprintf ppf "%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n%a\n" (pp_print_list pp_print_oracle "\n") gids.oracles (pp_print_list pp_print_array_ctor "\n") array_ctor_list (pp_print_list pp_print_node_arg "\n") gids.node_args (pp_print_list pp_print_local "\n") locals_list (pp_print_list pp_print_local "\n") gids.ib_oracles - (pp_print_list pp_print_oracle "\n") gids.gen_ghost_vars (pp_print_list pp_print_call "\n") gids.calls (pp_print_list pp_print_subrange_constraint "\n") gids.subrange_constraints (pp_print_list pp_print_refinement_type_constraint "\n") gids.refinement_type_constraints @@ -1227,19 +1226,7 @@ and normalize_node_contract info node_id map cref inputs outputs (id, _, ivars, let vars = List.map (fun (p,id,ty,_) -> (p,id,ty)) ovars in add_ref_type_constraints info Output vars in - let gen_gvars = match (StringMap.find_opt node_id map) with - | Some gids -> gids.gen_ghost_vars - (* FIXME: This should not happen; every node should have gids. - But, this is not currently the case, as monomorphization currently - (incorrectly) does not generate gids. This will be fixed in a future PR. *) - | None -> [] - in - let gen_gvars = List.map (fun (id, ty, expr) -> - let pos = AH.pos_of_expr expr in - let c_lhs = A.GhostVarDec (pos, [pos, id, ty]) in - A.GhostVars (pos, c_lhs, expr) - ) gen_gvars in - let nbody, gids7, warnings3 = normalize_contract info node_id map ivars ovars gen_gvars body in + let nbody, gids7, _, warnings3 = normalize_contract info node_id map ivars ovars body in let gids = List.fold_left union (empty ()) [union_list gids1; union_list gids2; gids3; gids4; gids5; gids6; gids7] in nbody, gids, List.flatten (warnings1 @ warnings2) @ warnings3, StringMap.empty @@ -1301,28 +1288,16 @@ and normalize_node info map in (* We have to handle contracts before locals Otherwise the typing contexts collide *) - let ncontracts, gids6, warnings4 = match contract with + let ncontracts, gids6, interpretation, warnings4 = match contract with | Some contract -> let ctx = Chk.tc_ctx_of_contract info.context Ghost node_id contract |> unwrap |> fst in let contract_ref = new_contract_reference () in let info = { info with context = ctx; contract_ref } in - let gen_gvars = match (StringMap.find_opt node_id map) with - | Some gids -> gids.gen_ghost_vars - (* FIXME: This should not happen; every node should have gids. - But, this is not currently the case, as monomorphization currently - (incorrectly) does not generate gids. This will be fixed in a future PR. *) - | None -> [] - in - let gen_gvars = List.map (fun (id, ty, expr) -> - let pos = AH.pos_of_expr expr in - let c_lhs = A.GhostVarDec (pos, [pos, id, ty]) in - A.GhostVars (pos, c_lhs, expr) - ) gen_gvars in - let ncontracts, gids, warnings = - normalize_contract info node_id map inputs outputs gen_gvars contract in - (Some ncontracts), gids, warnings - | None -> None, empty (), [] + let ncontracts, gids, interpretation, warnings = + normalize_contract info node_id map inputs outputs contract in + (Some ncontracts), gids, interpretation, warnings + | None -> None, empty (), StringMap.empty, [] in let ctx = Chk.add_local_node_ctx ctx locals in let info = { info with context = ctx } in @@ -1384,7 +1359,7 @@ and normalize_node info map in let new_gids = union_list [union_list gids1; union_list gids2; union_list gids3; gids4; gids5; gids7; gids6_8; gids9; gids10] in - let old_gids, warnings6 = normalize_gid_equations info map node_id in + let old_gids, warnings6 = normalize_gid_equations { info with interpretation = interpretation; } map node_id in let map = StringMap.add node_id (union old_gids new_gids) map in (node_id, is_extern, opac, params, inputs, outputs, locals, List.flatten nitems, ncontracts), map, @@ -1527,11 +1502,10 @@ and rename_ghost_variables info contract = (StringMap.singleton id new_id) :: tail, info | _ :: t -> rename_ghost_variables info t -and normalize_contract info node_id map ivars ovars gen_ghost_vars (p, items) = +and normalize_contract info node_id map ivars ovars (p, items) = let gids = ref (empty ()) in let warnings = ref [] in let result = ref [] in - let items = items @ gen_ghost_vars in let ghost_interp, info = rename_ghost_variables info items in let ghost_interp = List.fold_left (StringMap.merge union_keys) StringMap.empty ghost_interp @@ -1698,25 +1672,8 @@ and normalize_contract info node_id map ivars ovars gen_ghost_vars (p, items) = ) tis in - (* Update generated ghost var names in gids *) - let gids = union (union gids1 gids2) gids3 in - let curr_node_gids = match StringMap.find_opt node_id map with - | Some gids -> gids - (* FIXME: This should not happen; every node should have gids. - But, this is not currently the case, as monomorphization currently - (incorrectly) does not generate gids. This will be fixed in a future PR. *) - | None -> empty () - in - let updated_gen_ghost_vars = - List.map (fun (id, ty, expr) -> - StringMap.find id info.interpretation, ty, expr - ) curr_node_gids.gen_ghost_vars in - let gids = { gids with - gen_ghost_vars = updated_gen_ghost_vars - } in - GhostVars (pos, GhostVarDec(pos2, tis'), nexpr), - gids, + union (union gids1 gids2) gids3, warnings @ warnings2, StringMap.empty @@ -1728,7 +1685,7 @@ and normalize_contract info node_id map ivars ovars gen_ghost_vars (p, items) = gids := union !gids gids'; warnings := !warnings @ warnings'; done; - (p, !result), !gids, !warnings + (p, !result), !gids, !interpretation, !warnings and normalize_equation info node_id map = function diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index aaf279ebd..55dc2623a 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -32,12 +32,13 @@ let unwrap = function (* [i] is module state used to guarantee newly created identifiers are unique *) let i = ref 0 -let mk_fresh_ghost_var ty rhs = +let mk_fresh_ghost_var pos cname ty rhs = i := !i + 1; let prefix = HString.mk_hstring (string_of_int !i) in let name = HString.concat2 prefix (HString.mk_hstring "_ghost") in let gids = { (GI.empty ()) with - gen_ghost_vars = [name, ty, rhs]; + locals = GI.StringMap.singleton name ty; + equations = [([], [pos, cname], A.StructDef(pos, [SingleIdent (pos, name)]), rhs)]; } in name, gids @@ -64,7 +65,7 @@ let contract_node_decl_to_contracts | TArr(_, _, ty) when i = 0 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in + let gen_ghost_var, gids = mk_fresh_ghost_var pos id ghost_var_ty expr in gen_ghost_var, gids ) ips |> List.split in @@ -121,7 +122,7 @@ let node_decl_to_contracts | TArr(_, _, ty) when i = 1 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var ghost_var_ty expr in + let gen_ghost_var, gids = mk_fresh_ghost_var pos id ghost_var_ty expr in gen_ghost_var, gids ) ips |> List.split in diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index cb2f64238..c676887f6 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1302,12 +1302,6 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con let expr_ident = mk_ident id in let (ident, contract_namespace) = extract_namespace id in let index_types = compile_ast_type cstate ctx map ty in - let gen_ghost_vars = List.map (fun (a, _, _) -> a) gids.GI.gen_ghost_vars in - let source = - if List.mem id gen_ghost_vars - then N.Generated - else N.Ghost - in let over_indices = fun index index_type accum -> ( let possible_state_var = ( mk_state_var @@ -1318,7 +1312,7 @@ and compile_contract_variables cstate gids ctx map contract_scope node_scope con ident index index_type - (Some source) + (Some N.Ghost) ) in match possible_state_var with From b93b52a2b468dbf82e002bff6bf0b50d34c89a26 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 31 Jan 2025 16:38:13 -0600 Subject: [PATCH 08/11] Fix normalize_gid_equations to ensure the correct variable renaming (or lack of renaming) occurs --- src/lustre/generatedIdentifiers.ml | 3 +- src/lustre/generatedIdentifiers.mli | 3 +- src/lustre/lustreAstNormalizer.ml | 47 +++++++++++++++++++------- src/lustre/lustreGenRefTypeImpNodes.ml | 2 +- src/lustre/lustreNodeGen.ml | 2 +- src/lustre/lustreRemoveMultAssign.ml | 2 +- 6 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index 91a0b7b74..497f197d7 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -73,7 +73,8 @@ type t = { (LustreAst.typed_ident list (* quantified variables *) * (Lib.position * HString.t) list (* contract scope *) * LustreAst.eq_lhs - * LustreAst.expr) + * LustreAst.expr + * source option) (* Record the source of the equation if generated before normalization step *) list; nonvacuity_props: StringSet.t; array_literal_vars: StringSet.t; diff --git a/src/lustre/generatedIdentifiers.mli b/src/lustre/generatedIdentifiers.mli index 4e950a497..6594f0ede 100644 --- a/src/lustre/generatedIdentifiers.mli +++ b/src/lustre/generatedIdentifiers.mli @@ -73,7 +73,8 @@ type t = { (LustreAst.typed_ident list (* quantified variables *) * (Lib.position * HString.t) list (* contract scope *) * LustreAst.eq_lhs - * LustreAst.expr) + * LustreAst.expr + * source option) (* Record the source of the equation if generated before normalization step *) list; nonvacuity_props: StringSet.t; array_literal_vars: StringSet.t; (* Variables equal to an array literal *) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 688663fd7..5bbcdb345 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -275,7 +275,7 @@ let pp_print_generated_identifiers ppf gids = (pp_print_list (pp_print_pair Lib.pp_print_position HString.pp_print_hstring ":") "::") scope (pp_print_list A.pp_print_contract_item ";") decl in - let pp_print_equation ppf (_, _, lhs, expr) = Format.fprintf ppf "%a = %a" + let pp_print_equation ppf (_, _, lhs, expr, _) = Format.fprintf ppf "%a = %a" A.pp_print_eq_lhs lhs A.pp_print_expr expr in @@ -393,7 +393,7 @@ let mk_fresh_array_ctor info pos ind_vars expr_type expr size_expr = let (eq_lhs, nexpr) = generalize_to_array_expr name ind_vars expr nexpr in let gids = { (empty ()) with array_constructors = StringMap.singleton name (expr_type, expr, size_expr); - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr, None)]; } in nexpr, gids let mk_fresh_node_arg_local info pos is_const expr_type expr = @@ -408,7 +408,7 @@ let mk_fresh_node_arg_local info pos is_const expr_type expr = let (eq_lhs, nexpr) = generalize_to_array_expr name ind_vars expr nexpr in let gids = { (empty ()) with node_args = [(name, is_const, expr_type, expr)]; - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr, None)]; } in NodeArgCache.add node_arg_cache expr nexpr; nexpr, gids @@ -592,7 +592,7 @@ let mk_fresh_subrange_constraint source info pos node_id constrained_name expr_t let (eq_lhs, _) = generalize_to_array_expr name StringMap.empty range_expr nexpr in let gids = { (empty ()) with subrange_constraints = [(source, info.contract_scope, is_original, pos, name, output_expr)]; - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, range_expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, range_expr, None)]; } in gids) range_exprs @@ -681,7 +681,7 @@ let mk_fresh_local force info pos ind_vars expr_type expr = let (eq_lhs, nexpr) = generalize_to_array_expr name ind_vars expr nexpr in let gids = { (empty ()) with locals = StringMap.singleton name expr_type; - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr, None)]; } in LocalCache.add local_cache expr nexpr; nexpr, gids @@ -716,7 +716,7 @@ let mk_fresh_frozen_local node_id info pos ind_vars expr_type = let gids2 = { (empty ()) with locals = StringMap.singleton name expr_type; asserts; - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr, None)]; } in nexpr, name, union (union gids1 gids2) gids3 @@ -731,7 +731,7 @@ let mk_fresh_refinement_type_constraint source info pos id expr_type = let (eq_lhs, _) = generalize_to_array_expr name StringMap.empty ref_type_expr nexpr in let gids = { (empty ()) with refinement_type_constraints = [(source, pos, name, output_expr)]; - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, ref_type_expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, ref_type_expr, None)]; } in gids) ref_type_exprs @@ -777,7 +777,7 @@ let add_step_counter info = in { (empty ()) with locals = StringMap.singleton ctr_id (A.Int dpos); - equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } + equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr, None)]; } (** Add local step 'counter' and an equation setting counter = 0 -> pre counter + 1 *) let get_type_of_id info node_id id = @@ -841,7 +841,7 @@ let add_history_var_and_equation info id h_id = in A.TernaryOp (dpos, A.Ite, cond, A.Ident(dpos, id), prev_hist) in - [(info.quantified_variables, info.contract_scope, eq_lhs, eq_rhs)] + [(info.quantified_variables, info.contract_scope, eq_lhs, eq_rhs, None)] in { (empty ()) with locals; equations } @@ -1122,18 +1122,39 @@ let rec normalize ctx ai_ctx inlinable_funcs (decls:LustreAst.t) gids = Res.ok (ast, map, warnings) -and normalize_gid_equations info gids_map node_id = +(* In this function, we normalize generated identifiers that were created earlier in the pipeline. + It is a bit hacky with respect to how scoping is handled. More concretely, + because these equations were not generated within the normalizer, + and because our identifiers are not inherently scoped, + we need to recover some scoping information (namely, whether or not the generated equations + are contract or node body equations). + Future changes should be done carefully. +*) + and normalize_gid_equations info gids_map node_id = match StringMap.find_opt node_id gids_map with | None -> empty(), [] | Some gids -> ( (* Normalize all equations in gids *) - let gids_list, warnings, eqs = List.map (fun (_, _, lhs, expr) -> - let nexpr, gids, warnings = normalize_expr info node_id gids_map expr in - gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr) + let gids_list, warnings, eqs = List.map (fun (tis, sc, lhs, expr, source) -> + match source with + (* Generated equations created during the normalization step don't need to be normalized *) + | None -> + empty (), [], (tis, sc, lhs, expr, source) + (* Generated equations created before the normalization step; we need to use the right + info.interpretation and info.contract_scope *) + | Some Ghost -> + let nexpr, gids, warnings = normalize_expr info node_id gids_map expr in + gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr, None) + | Some _ -> + let info = { info with interpretation = StringMap.empty; contract_scope = [] } in + let nexpr, gids, warnings = normalize_expr info node_id gids_map expr in + gids, warnings, (info.quantified_variables, info.contract_scope, lhs, nexpr, None) ) gids.equations |> Lib.split3 in + (* Take out old equations that were not normalized *) let gids = { gids with equations = [] } in let gids = List.fold_left (fun acc g -> union g acc) gids gids_list in + (* Keep equations generated during normalization *) let eqs2 = gids.equations in let gids = { gids with equations = eqs @ eqs2; } in diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 55dc2623a..09636ef94 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -38,7 +38,7 @@ let mk_fresh_ghost_var pos cname ty rhs = let name = HString.concat2 prefix (HString.mk_hstring "_ghost") in let gids = { (GI.empty ()) with locals = GI.StringMap.singleton name ty; - equations = [([], [pos, cname], A.StructDef(pos, [SingleIdent (pos, name)]), rhs)]; + equations = [([], [pos, cname], A.StructDef(pos, [SingleIdent (pos, name)]), rhs, Some GI.Ghost)]; } in name, gids diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index c676887f6..6d0acda16 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -1999,7 +1999,7 @@ and compile_node_decl gids_map is_function opac cstate ctx i ext params inputs o (* Generated Equations *) (* ****************************************************************** *) in let gequations = - let over_equations = fun eqns (qvars, contract_scope, lhs, ast_expr) -> + let over_equations = fun eqns (qvars, contract_scope, lhs, ast_expr, _) -> map := { !map with contract_scope }; let eq_lhs, indexes = match lhs with | A.StructDef (_, []) -> X.empty, 0 diff --git a/src/lustre/lustreRemoveMultAssign.ml b/src/lustre/lustreRemoveMultAssign.ml index 7d931b994..6fd9a3925 100644 --- a/src/lustre/lustreRemoveMultAssign.ml +++ b/src/lustre/lustreRemoveMultAssign.ml @@ -100,7 +100,7 @@ let create_new_eqs ctx lhs expr = let arrayids_new = get_array_ids sis in let expr = LAH.replace_idents arrayids_original arrayids_new expr in let gids2 = { (GI.empty ()) with - equations = [([], [], A.StructDef(pos, sis), expr)]; + equations = [([], [], A.StructDef(pos, sis), expr, Some GI.Output)]; } in let eqs = List.map (fun x -> A.Body x) eqs in ( From 5d6f7dc3e274dc20bf18bb8e9e17afc3fdc21c46 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 31 Jan 2025 17:15:46 -0600 Subject: [PATCH 09/11] Disallow mode references in contract assumptions when environment realizability checking is enabled --- src/lustre/lustreErrors.ml | 3 + src/lustre/lustreErrors.mli | 1 + src/lustre/lustreGenRefTypeImpNodes.ml | 129 +++++++++++++++++------- src/lustre/lustreGenRefTypeImpNodes.mli | 11 +- src/lustre/lustreInput.ml | 17 ++-- src/lustre/lustreInput.mli | 1 + 6 files changed, 116 insertions(+), 46 deletions(-) diff --git a/src/lustre/lustreErrors.ml b/src/lustre/lustreErrors.ml index fde75c49c..a43d80b3c 100644 --- a/src/lustre/lustreErrors.ml +++ b/src/lustre/lustreErrors.ml @@ -29,6 +29,7 @@ type error = [ | `LustreUnguardedPreError of Lib.position * LustreAst.expr | `LustreParserError of Lib.position * string | `LustreDesugarIfBlocksError of Lib.position * LustreDesugarIfBlocks.error_kind + | `LustreGenRefTypeImpNodesError of Lib.position * LustreGenRefTypeImpNodes.error_kind | `LustreDesugarFrameBlocksError of Lib.position * LustreDesugarFrameBlocks.error_kind ] @@ -43,6 +44,7 @@ let error_position error = match error with | `LustreUnguardedPreError (pos, _) -> pos | `LustreParserError (pos, _) -> pos | `LustreDesugarIfBlocksError (pos, _) -> pos + | `LustreGenRefTypeImpNodesError (pos, _) -> pos | `LustreDesugarFrameBlocksError (pos, _) -> pos let error_message error = match error with @@ -56,4 +58,5 @@ let error_message error = match error with | `LustreUnguardedPreError (_, e) -> (Format.asprintf "@[Unguarded pre in expression@ %a@]" LA.pp_print_expr e) | `LustreParserError (_, e) -> e | `LustreDesugarIfBlocksError (_, kind) -> LustreDesugarIfBlocks.error_message kind + | `LustreGenRefTypeImpNodesError (_, kind) -> LustreGenRefTypeImpNodes.error_message kind | `LustreDesugarFrameBlocksError (_, kind) -> LustreDesugarFrameBlocks.error_message kind \ No newline at end of file diff --git a/src/lustre/lustreErrors.mli b/src/lustre/lustreErrors.mli index 690d5304d..cb7b2a8a6 100644 --- a/src/lustre/lustreErrors.mli +++ b/src/lustre/lustreErrors.mli @@ -30,6 +30,7 @@ type error = [ | `LustreUnguardedPreError of Lib.position * LustreAst.expr | `LustreParserError of Lib.position * string | `LustreDesugarIfBlocksError of Lib.position * LustreDesugarIfBlocks.error_kind + | `LustreGenRefTypeImpNodesError of Lib.position * LustreGenRefTypeImpNodes.error_kind | `LustreDesugarFrameBlocksError of Lib.position * LustreDesugarFrameBlocks.error_kind ] diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 09636ef94..90d355b26 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -19,6 +19,21 @@ module A = LustreAst module Chk = LustreTypeChecker module Ctx = TypeCheckerContext module GI = GeneratedIdentifiers +module R = Res + +let (let*) = R.(>>=) + +type error_kind = + | EnvRealizabilityCheckModeRefAssumption + +let error_message error = match error with + | EnvRealizabilityCheckModeRefAssumption -> "Environment realizability checks do not currently support assumptions containing mode references. To disable environment realizability checking, pass --check_realizability false" + +type error = [ + | `LustreGenRefTypeImpNodesError of Lib.position * error_kind +] + +let mk_error pos kind = Error (`LustreGenRefTypeImpNodesError (pos, kind)) let inputs_tag = ".inputs_" let contract_tag = ".contract_" @@ -41,13 +56,41 @@ let mk_fresh_ghost_var pos cname ty rhs = equations = [([], [pos, cname], A.StructDef(pos, [SingleIdent (pos, name)]), rhs, Some GI.Ghost)]; } in name, gids + +let rec expr_contains_mode_ref expr = + let r = expr_contains_mode_ref in + match expr with + | A.ModeRef (_, _) -> true + | Ident (_, _) + | Const (_, _) -> false + | RecordProject (_, e, _) | TupleProject (_, e, _) | UnaryOp (_, _, e) + | ConvOp (_, _, e) | Quantifier (_, _, _, e) | When (_, e, _) + | Pre (_, e) + -> r e + | BinaryOp (_, _, e1, e2) | CompOp (_, _, e1, e2) | StructUpdate (_, e1, _, e2) + | ArrayConstr (_, e1, e2) | ArrayIndex (_, e1, e2) + | Arrow (_, e1, e2) + -> r e1 || r e2 + | TernaryOp (_, _, e1, e2, e3) + -> r e1 || r e2 || r e3 + | GroupExpr (_, _, expr_list) + -> List.fold_left (fun acc x -> acc || r x) false expr_list + | RecordExpr (_, _, _, expr_list) | Merge (_, _, expr_list) + -> List.fold_left (fun acc (_, e) -> acc || r e) false expr_list + | Activate (_, _, e1, e2, expr_list) -> + r e1 || r e2 + || List.fold_left (fun acc x -> acc || r x) false expr_list + | Call (_, _, _, _) | Condact (_, _, _, _, _, _) | RestartEvery (_, _, _, _) | AnyOp (_, _, _, _) + -> false let contract_node_decl_to_contracts = fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> - let contract', gids = List.filter_map (fun ci -> + let* res = R.seq (List.map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some (ci, GI.empty ()) - | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr), GI.empty ()) + | A.GhostConst _ | GhostVars _ -> R.ok (Some (ci, GI.empty ())) + | A.Assume (pos, name, b, expr) -> + if expr_contains_mode_ref expr then mk_error pos EnvRealizabilityCheckModeRefAssumption else + R.ok (Some (A.Guarantee (pos, name, b, expr), GI.empty ())) | A.ContractCall (pos, name, ty_args, ips, ops) -> let name = HString.concat2 (HString.mk_hstring inputs_tag) name in (* Since we are flipping the inputs and outputs of the generated contract, @@ -69,12 +112,13 @@ let contract_node_decl_to_contracts gen_ghost_var, gids ) ips |> List.split in - Some ( + R.ok (Some ( A.ContractCall (pos, name, ty_args, ips', ops'), List.fold_left GI.union ( GI.empty ()) gids - ) - | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None - ) base_contract |> List.split in + )) + | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> R.ok None + ) base_contract) in + let contract', gids = List.filter_map (fun x -> x) res |> List.split in let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in let inputs2, outputs2 = List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, @@ -93,16 +137,18 @@ let contract_node_decl_to_contracts then (* Update ctx with info about the generated contract *) let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in - [environment], ctx, gids - else [], ctx, gids + R.ok ([environment], ctx, gids) + else R.ok ([], ctx, gids) let node_decl_to_contracts = fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) -> let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in - let contract', gids = List.filter_map (fun ci -> + let* res = R.seq (List.map (fun ci -> match ci with - | A.GhostConst _ | GhostVars _ -> Some (ci, GI.empty ()) - | A.Assume (pos, name, b, expr) -> Some (A.Guarantee (pos, name, b, expr), GI.empty ()) + | A.GhostConst _ | GhostVars _ -> R.ok (Some (ci, GI.empty ())) + | A.Assume (pos, name, b, expr) -> + if expr_contains_mode_ref expr then mk_error pos EnvRealizabilityCheckModeRefAssumption else + R.ok (Some (A.Guarantee (pos, name, b, expr), GI.empty ())) | A.ContractCall (pos, name, ty_args, ips, ops) -> if Flags.Contracts.check_environment () then ( let name = HString.concat2 (HString.mk_hstring inputs_tag) name in @@ -126,13 +172,14 @@ let node_decl_to_contracts gen_ghost_var, gids ) ips |> List.split in - Some ( + R.ok (Some ( A.ContractCall (pos, name, ty_args, ips', ops'), List.fold_left GI.union ( GI.empty ()) gids - )) - else None - | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> None - ) base_contract |> List.split in + ))) + else R.ok None + | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> R.ok None + ) base_contract) in + let contract', gids = List.filter_map (fun x -> x) res |> List.split in let locals_as_outputs = List.map (fun local_decl -> match local_decl with | A.NodeConstDecl (pos, FreeConst (_, id, ty)) | A.NodeConstDecl (pos, TypedConst (_, id, _, ty)) -> Some (pos, id, ty, A.ClockTrue) @@ -164,8 +211,8 @@ let node_decl_to_contracts if Flags.Contracts.check_environment () then (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in - [environment], ctx, gids - else [], ctx, gids + R.ok ([environment], ctx, gids) + else R.ok([], ctx, gids) else 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 @@ -173,11 +220,11 @@ let node_decl_to_contracts (* Update ctx with info about the generated nodes *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx environment |> unwrap in let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in - [environment; contract], ctx, gids + R.ok ([environment; contract], ctx, gids) else (* Update ctx with info about the generated node *) let ctx, _ = LustreTypeChecker.tc_ctx_of_node_decl pos ctx contract |> unwrap in - [contract], ctx, gids + R.ok ([contract], ctx, gids) (* NOTE: Currently, we do not allow global constants to have refinement types. If we decide to support this in the future, then we need to add necessary refinement type information @@ -192,44 +239,50 @@ let type_to_contract: Lib.position -> HString.t -> A.lustre_type -> HString.t li let node_items = [A.AnnotMain(pos, true)] in 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 * Ctx.tc_context * GI.t HString.HStringMap.t +let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> (A.declaration list * Ctx.tc_context * GI.t HString.HStringMap.t, [> error]) result = fun ctx decls -> - let decls, ctx, gids = List.fold_left (fun (acc_decls, acc_ctx, acc_gids) decl -> + let* decls, ctx, gids = R.seq_chain (fun (acc_decls, acc_ctx, acc_gids) decl -> match decl with | A.ConstDecl (_, FreeConst _) - | A.ConstDecl (_, TypedConst _) -> acc_decls, acc_ctx, acc_gids + | A.ConstDecl (_, TypedConst _) -> R.ok (acc_decls, acc_ctx, acc_gids) | A.TypeDecl (_, AliasType (p, id, ps, ty)) -> (match type_to_contract p id ty ps with - | Some decl1 -> decl1 :: acc_decls, acc_ctx, acc_gids - | None -> acc_decls, acc_ctx, acc_gids) + | Some decl1 -> R.ok (decl1 :: acc_decls, acc_ctx, acc_gids) + | None -> R.ok (acc_decls, acc_ctx, acc_gids)) | A.TypeDecl (_, FreeType _) - | A.ConstDecl (_, UntypedConst _) -> acc_decls, acc_ctx, acc_gids + | A.ConstDecl (_, UntypedConst _) -> R.ok (acc_decls, acc_ctx, acc_gids) | 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, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else node_decl in - let decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx node_decl in + let* decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx node_decl in let decls = List.map (fun decl -> A.NodeDecl (span, decl)) decls in - A.NodeDecl(span, node_decl) :: decls @ acc_decls, acc_ctx, - GI.StringMap.merge GI.union_keys2 gids acc_gids + R.ok ( + A.NodeDecl(span, node_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids + ) | 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, opac, ps, ips, ops, locs, [A.AnnotMain (span.start_pos, true)], c else func_decl in - let decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx func_decl in + let* decls, acc_ctx, gids = node_decl_to_contracts span.start_pos acc_ctx func_decl in let decls = List.map (fun decl -> A.FuncDecl (span, decl)) decls in - A.FuncDecl(span, func_decl) :: decls @ acc_decls, acc_ctx, - GI.StringMap.merge GI.union_keys2 gids acc_gids + R.ok ( + A.FuncDecl(span, func_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids + ) | A.ContractNodeDecl (span, contract_node_decl) -> - let decls, acc_ctx, gids = contract_node_decl_to_contracts acc_ctx contract_node_decl in + let* decls, acc_ctx, gids = contract_node_decl_to_contracts acc_ctx contract_node_decl in let decls = List.map (fun decl -> A.ContractNodeDecl (span, decl)) decls in - A.ContractNodeDecl (span, contract_node_decl) :: decls @ acc_decls, acc_ctx, - GI.StringMap.merge GI.union_keys2 gids acc_gids - | A.NodeParamInst _ -> decl :: acc_decls, acc_ctx, acc_gids + R.ok ( + A.ContractNodeDecl (span, contract_node_decl) :: decls @ acc_decls, acc_ctx, + GI.StringMap.merge GI.union_keys2 gids acc_gids + ) + | A.NodeParamInst _ -> R.ok (decl :: acc_decls, acc_ctx, acc_gids) ) ([], ctx, GI.StringMap.empty) decls in - List.rev decls, ctx, gids \ No newline at end of file + R.ok (List.rev decls, ctx, gids) \ No newline at end of file diff --git a/src/lustre/lustreGenRefTypeImpNodes.mli b/src/lustre/lustreGenRefTypeImpNodes.mli index 4eeb7a3da..1ffeca3be 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.mli +++ b/src/lustre/lustreGenRefTypeImpNodes.mli @@ -27,4 +27,13 @@ val contract_tag : string val type_tag : string val poly_gen_node_tag : string -val gen_imp_nodes : Ctx.tc_context -> A.declaration list -> A.declaration list * Ctx.tc_context * GI.t HString.HStringMap.t +type error_kind = + | EnvRealizabilityCheckModeRefAssumption + +val error_message : error_kind -> string + +type error = [ + | `LustreGenRefTypeImpNodesError of Lib.position * error_kind +] + +val gen_imp_nodes : Ctx.tc_context -> A.declaration list -> (A.declaration list * Ctx.tc_context * GI.t HString.HStringMap.t, [> error]) result \ No newline at end of file diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 424c157ad..19f7435e8 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -62,6 +62,7 @@ type error = [ | `LustreUnguardedPreError of Lib.position * LustreAst.expr | `LustreParserError of Lib.position * string | `LustreDesugarIfBlocksError of Lib.position * LustreDesugarIfBlocks.error_kind + | `LustreGenRefTypeImpNodesError of Lib.position * LustreGenRefTypeImpNodes.error_kind | `LustreDesugarFrameBlocksError of Lib.position * LustreDesugarFrameBlocks.error_kind ] @@ -174,15 +175,17 @@ let type_check declarations = LspInfo.print_ast_info global_ctx declarations; (* Step 9. Generate imported nodes associated with refinement types if realizability checking is enabled *) - let sorted_node_contract_decls, global_ctx, gids = + let* sorted_node_contract_decls, global_ctx, gids = if List.mem `CONTRACTCK (Flags.enabled ()) then - let decls1, ctx1, gids1 = LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts in - let decls2, ctx2, gids2 = LGI.gen_imp_nodes global_ctx sorted_node_contract_decls in - decls1 @ decls2, - TypeCheckerContext.union ctx1 ctx2, - GI.StringMap.merge GI.union_keys2 gids1 gids2 - else sorted_node_contract_decls, global_ctx, GI.StringMap.empty + let* decls1, ctx1, gids1 = LGI.gen_imp_nodes global_ctx const_inlined_type_and_consts in + let* decls2, ctx2, gids2 = LGI.gen_imp_nodes global_ctx sorted_node_contract_decls in + Res.ok ( + decls1 @ decls2, + TypeCheckerContext.union ctx1 ctx2, + GI.StringMap.merge GI.union_keys2 gids1 gids2 + ) + else Res.ok (sorted_node_contract_decls, global_ctx, GI.StringMap.empty) in (* Step 10. Remove multiple assignment from if blocks and frame blocks *) diff --git a/src/lustre/lustreInput.mli b/src/lustre/lustreInput.mli index 47c6c92c0..f1d6ad2a0 100644 --- a/src/lustre/lustreInput.mli +++ b/src/lustre/lustreInput.mli @@ -119,6 +119,7 @@ type error = [ | `LustreUnguardedPreError of Lib.position * LustreAst.expr | `LustreParserError of Lib.position * string | `LustreDesugarIfBlocksError of Lib.position * LustreDesugarIfBlocks.error_kind + | `LustreGenRefTypeImpNodesError of Lib.position * LustreGenRefTypeImpNodes.error_kind | `LustreDesugarFrameBlocksError of Lib.position * LustreDesugarFrameBlocks.error_kind ] From 97b12bb62a6f376f84c4f0c5dca18ad4428dd35b Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 31 Jan 2025 17:26:32 -0600 Subject: [PATCH 10/11] Minor update to make the last change clearer --- src/lustre/lustreGenRefTypeImpNodes.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index 90d355b26..dd49df15e 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -47,13 +47,15 @@ let unwrap = function (* [i] is module state used to guarantee newly created identifiers are unique *) let i = ref 0 -let mk_fresh_ghost_var pos cname ty rhs = +let mk_fresh_ghost_var pos ty rhs = i := !i + 1; let prefix = HString.mk_hstring (string_of_int !i) in let name = HString.concat2 prefix (HString.mk_hstring "_ghost") in let gids = { (GI.empty ()) with locals = GI.StringMap.singleton name ty; - equations = [([], [pos, cname], A.StructDef(pos, [SingleIdent (pos, name)]), rhs, Some GI.Ghost)]; + (* No contract scope is given because we are currently disallowing mode references in contract + assumptions during environment realizability checks. *) + equations = [([], [], A.StructDef(pos, [SingleIdent (pos, name)]), rhs, Some GI.Ghost)]; } in name, gids @@ -108,7 +110,7 @@ let contract_node_decl_to_contracts | TArr(_, _, ty) when i = 0 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var pos id ghost_var_ty expr in + let gen_ghost_var, gids = mk_fresh_ghost_var pos ghost_var_ty expr in gen_ghost_var, gids ) ips |> List.split in @@ -168,7 +170,7 @@ let node_decl_to_contracts | TArr(_, _, ty) when i = 1 -> ty | _ -> assert false in - let gen_ghost_var, gids = mk_fresh_ghost_var pos id ghost_var_ty expr in + let gen_ghost_var, gids = mk_fresh_ghost_var pos ghost_var_ty expr in gen_ghost_var, gids ) ips |> List.split in From 996283c47cd06f9ce99ec680205218010b8b29a1 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 31 Jan 2025 17:44:25 -0600 Subject: [PATCH 11/11] Factor out reused code --- src/lustre/lustreGenRefTypeImpNodes.ml | 114 +++++++++---------------- 1 file changed, 40 insertions(+), 74 deletions(-) diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index dd49df15e..24dd9e1f3 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -84,75 +84,16 @@ let rec expr_contains_mode_ref expr = || List.fold_left (fun acc x -> acc || r x) false expr_list | Call (_, _, _, _) | Condact (_, _, _, _, _, _) | RestartEvery (_, _, _, _) | AnyOp (_, _, _, _) -> false - -let contract_node_decl_to_contracts -= fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> - let* res = R.seq (List.map (fun ci -> - match ci with - | A.GhostConst _ | GhostVars _ -> R.ok (Some (ci, GI.empty ())) - | A.Assume (pos, name, b, expr) -> - if expr_contains_mode_ref expr then mk_error pos EnvRealizabilityCheckModeRefAssumption else - R.ok (Some (A.Guarantee (pos, name, b, expr), GI.empty ())) - | A.ContractCall (pos, name, ty_args, ips, ops) -> - let name = HString.concat2 (HString.mk_hstring inputs_tag) name in - (* Since we are flipping the inputs and outputs of the generated contract, - we also need to flip inputs and outputs of the call *) - let ips' = List.map (fun id -> A.Ident (pos, id)) ops in - let ops', gids = List.mapi (fun i expr -> match expr with - | A.Ident (_, id) -> id, GI.empty () - (* Input is not a simple identifier, so we have to generate a ghost variable - to store the output *) - | expr -> - let called_contract_ty = Ctx.lookup_contract_ty ctx name in - let ghost_var_ty = match Option.get called_contract_ty with - | TArr (_, _, GroupType (_, tys)) -> - List.nth tys i - | TArr(_, _, ty) when i = 0 -> ty - | _ -> assert false - in - let gen_ghost_var, gids = mk_fresh_ghost_var pos ghost_var_ty expr in - gen_ghost_var, - gids - ) ips |> List.split in - R.ok (Some ( - A.ContractCall (pos, name, ty_args, ips', ops'), - List.fold_left GI.union ( GI.empty ()) gids - )) - | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> R.ok None - ) base_contract) in - let contract', gids = List.filter_map (fun x -> x) res |> List.split in - let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in - let inputs2, outputs2 = - List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, - List.map (fun (p, id, ty, cl, _) -> (p, id, ty, cl)) inputs - in - (* Since we are omitting assumptions from environment realizability checks, - we need to chase base types for environment inputs *) - let inputs2 = List.map (fun (p, id, ty, cl, b) -> - let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in - (p, id, ty, cl, b) - ) inputs2 in - (* We generate a contract representing this contract's inputs/environment *) - let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in - let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in - if Flags.Contracts.check_environment () - then - (* Update ctx with info about the generated contract *) - let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in - R.ok ([environment], ctx, gids) - else R.ok ([], ctx, gids) -let node_decl_to_contracts -= fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) -> - let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in +let mk_generated_env_contract_eqs ctx base_contract = let* res = R.seq (List.map (fun ci -> match ci with | A.GhostConst _ | GhostVars _ -> R.ok (Some (ci, GI.empty ())) - | A.Assume (pos, name, b, expr) -> + | A.Assume (pos, name, b, expr) -> if expr_contains_mode_ref expr then mk_error pos EnvRealizabilityCheckModeRefAssumption else R.ok (Some (A.Guarantee (pos, name, b, expr), GI.empty ())) - | A.ContractCall (pos, name, ty_args, ips, ops) -> - if Flags.Contracts.check_environment () then ( + | A.ContractCall (pos, name, ty_args, ips, ops) -> + if Flags.Contracts.check_environment () then ( let name = HString.concat2 (HString.mk_hstring inputs_tag) name in (* Since we are flipping the inputs and outputs of the generated contract, we also need to flip inputs and outputs of the call *) @@ -167,7 +108,7 @@ let node_decl_to_contracts let ghost_var_ty = match Option.get called_contract_ty with | TArr (_, _, GroupType (_, tys)) -> List.nth tys i - | TArr(_, _, ty) when i = 1 -> ty + | TArr(_, _, ty) when i = 0 -> ty | _ -> assert false in let gen_ghost_var, gids = mk_fresh_ghost_var pos ghost_var_ty expr in @@ -182,6 +123,40 @@ let node_decl_to_contracts | A.Guarantee _ | A.AssumptionVars _ | A.Mode _ -> R.ok None ) base_contract) in let contract', gids = List.filter_map (fun x -> x) res |> List.split in + R.ok (contract', gids) + +let mk_swapped_inputs_and_outputs ctx inputs outputs = + let inputs2, outputs2 = + List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, + List.map (fun (p, id, ty, cl, _) -> (p, id, ty, cl)) inputs + in + (* Since we are omitting assumptions from environment realizability checks, + we need to chase base types for environment inputs *) + let inputs2 = List.map (fun (p, id, ty, cl, b) -> + let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in + (p, id, ty, cl, b) + ) inputs2 in + inputs2, outputs2 + +let contract_node_decl_to_contracts += fun ctx (id, params, inputs, outputs, (pos, base_contract)) -> + let* contract', gids = mk_generated_env_contract_eqs ctx base_contract in + let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in + let inputs2, outputs2 = mk_swapped_inputs_and_outputs ctx inputs outputs in + (* We generate a contract representing this contract's inputs/environment *) + let environment = gen_node_id, params, inputs2, outputs2, (pos, contract') in + let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in + if Flags.Contracts.check_environment () + then + (* Update ctx with info about the generated contract *) + let ctx, _ = LustreTypeChecker.tc_ctx_of_contract_node_decl pos ctx environment |> unwrap in + R.ok ([environment], ctx, gids) + else R.ok ([], ctx, gids) + +let node_decl_to_contracts += fun pos ctx (id, extern, _, params, inputs, outputs, locals, _, contract) -> + let base_contract = match contract with | None -> [] | Some (_, contract) -> contract in + let* contract', gids = mk_generated_env_contract_eqs ctx base_contract in let locals_as_outputs = List.map (fun local_decl -> match local_decl with | A.NodeConstDecl (pos, FreeConst (_, id, ty)) | A.NodeConstDecl (pos, TypedConst (_, id, _, ty)) -> Some (pos, id, ty, A.ClockTrue) @@ -195,16 +170,7 @@ let node_decl_to_contracts let node_items = [A.AnnotMain(pos, true)] in let gen_node_id = HString.concat2 (HString.mk_hstring inputs_tag) id in let gen_node_id2 = HString.concat2 (HString.mk_hstring contract_tag) id in - let inputs2, outputs2 = - List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, - List.map (fun (p, id, ty, cl, _) -> (p, id, ty, cl)) inputs - in - (* Since we are omitting assumptions from environment realizability checks, - we need to chase base types for environment inputs *) - let inputs2 = List.map (fun (p, id, ty, cl, b) -> - let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in - (p, id, ty, cl, b) - ) inputs2 in + let inputs2, outputs2 = mk_swapped_inputs_and_outputs ctx inputs outputs in let gids = List.fold_left GI.union (GI.empty ()) gids |> GI.StringMap.singleton gen_node_id in (* We potentially generate two imported nodes: One for the input node's contract (w/ type info), and another for the input node's inputs/environment *)