From 0682c271d65bc0341b16f8c86971cb5819a140a7 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Fri, 23 Aug 2024 14:48:29 -0500 Subject: [PATCH] Create param subrange constraints for arrays --- src/lustre/lustreAstNormalizer.ml | 14 ++++--- src/lustre/lustreAstNormalizer.mli | 6 +++ src/lustre/lustreNodeGen.ml | 39 +++++++++---------- src/lustre/typeCheckerContext.ml | 5 +++ src/transSys.ml | 2 +- .../success/free_const_subrange.lus | 14 +++++++ 6 files changed, 53 insertions(+), 27 deletions(-) create mode 100644 tests/regression/success/free_const_subrange.lus diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 201d54092..5e9146626 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -416,7 +416,7 @@ let mk_range_expr ctx node_id expr_type expr = [disj, true] ) | A.IntRange (_, l, u) -> - let original_ty, _ = Chk.infer_type_expr ctx (Some node_id) expr |> unwrap in + let original_ty, _ = Chk.infer_type_expr ctx node_id expr |> unwrap in let original_ty = Chk.expand_type_syn_reftype_history ctx original_ty |> unwrap in let user_prop, is_original = match original_ty with | A.IntRange (_, l', u') -> @@ -632,7 +632,7 @@ let add_subrange_constraints info node_id kind vars = |> List.fold_left (fun acc (p, id) -> let ty = get_type_of_id info node_id id in let ty = AIC.inline_constants_of_lustre_type info.context ty in - union acc (mk_fresh_subrange_constraint kind info p node_id id ty)) + union acc (mk_fresh_subrange_constraint kind info p (Some node_id) id ty)) (empty ()) let add_ref_type_constraints info kind vars = @@ -1128,7 +1128,7 @@ and normalize_node info map | A.NodeConstDecl (p, TypedConst (_, id, _, _)) -> let ty = get_type_of_id info node_id id in let ty = AIC.inline_constants_of_lustre_type info.context ty in - let gids = union acc (mk_fresh_subrange_constraint Local info p node_id id ty) + let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty) in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty) | A.NodeConstDecl (_, UntypedConst _)-> assert false) (empty ()) @@ -1469,7 +1469,7 @@ and normalize_contract info node_id map ivars ovars (p, items) = if Ctx.type_contains_subrange info.context ty || Ctx.type_contains_ref info.context ty then (pos, i, ty), union gids ( - union (mk_fresh_subrange_constraint Ghost info pos node_id new_id ty) + union (mk_fresh_subrange_constraint Ghost info pos (Some node_id) new_id ty) (mk_fresh_refinement_type_constraint Ghost info pos (A.Ident (pos, new_id)) ty)), warnings else (pos, i, ty), gids, [] @@ -1679,8 +1679,10 @@ and normalize_expr ?guard info node_id map = List.fold_left (fun acc (_, id, ty) -> let expr = A.Ident(dpos, id) in - let range_exprs = List.map fst (mk_range_expr info.context node_id ty expr) @ - List.map snd (mk_ref_type_expr info.context expr Local ty) in + let range_exprs = + List.map fst (mk_range_expr info.context (Some node_id) ty expr) @ + List.map snd (mk_ref_type_expr info.context expr Local ty) + in range_exprs :: acc ) [] diff --git a/src/lustre/lustreAstNormalizer.mli b/src/lustre/lustreAstNormalizer.mli index 324a0ff5f..4d91a04c7 100644 --- a/src/lustre/lustreAstNormalizer.mli +++ b/src/lustre/lustreAstNormalizer.mli @@ -82,6 +82,12 @@ val warning_message : warning_kind -> string val mk_fresh_dummy_index : 'a -> HString.t +val mk_range_expr : TypeCheckerContext.tc_context -> + HString.t option -> + LustreAst.lustre_type -> + LustreAst.expr -> + (LustreAst.expr * bool) list + val normalize : TypeCheckerContext.tc_context -> LustreAbstractInterpretation.context -> LustreAst.t -> diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index 6be5955d6..93492e661 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -25,6 +25,7 @@ open LustreReporting module A = LustreAst module AH = LustreAstHelpers +module AN = LustreAstNormalizer module GI = GeneratedIdentifiers module G = LustreGlobals module N = LustreNode @@ -2335,24 +2336,12 @@ and compile_node_decl gids_map is_function cstate ctx i ext params inputs output nodes = node :: cstate.nodes; } -and add_type_constraints global_constraints v ty = - match Type.node_of_type ty with - | Type.IntRange (Some n1, Some n2) -> - E.mk_and - (E.mk_lte (E.mk_int n1) (E.mk_var v)) - (E.mk_lte (E.mk_var v) (E.mk_int n2)) - :: global_constraints - | IntRange (Some n1, None) -> - (E.mk_lte (E.mk_int n1) (E.mk_var v)) :: global_constraints - | IntRange (None, Some n2) -> - (E.mk_lte (E.mk_var v) (E.mk_int n2)) :: global_constraints - | _ -> global_constraints and compile_const_decl ?(ghost = false) cstate ctx map scope = function - | A.FreeConst (_, i, ty) -> + | A.FreeConst (p, i, ty) -> let ident = mk_ident i in let cty = compile_ast_type cstate ctx map ty in - let over_index = fun i ty (vt, global_constraints) -> + let over_index = fun i ty vt -> let possible_state_var = mk_state_var ?is_input:(Some false) ?is_const:(Some true) @@ -2366,17 +2355,27 @@ and compile_const_decl ?(ghost = false) cstate ctx map scope = function in match possible_state_var with | Some state_var -> - let v = Var.mk_const_state_var state_var in - X.add i v vt, add_type_constraints global_constraints state_var ty - | None -> vt, global_constraints - in - let vt, global_constraints = - X.fold over_index cty (X.empty, cstate.global_constraints) + X.add i (Var.mk_const_state_var state_var) vt + | None -> vt in + let vt = X.fold over_index cty X.empty in let var_bounds = SVT.fold (fun k v a -> (k, v) :: a) !map.bounds [] in List.iter (fun (k, v) -> SVT.add cstate.state_var_bounds k v) var_bounds; if ghost then cstate else ( + let global_constraints = + let ty = Ctx.expand_type_syn ctx ty in + if Ctx.type_contains_subrange ctx ty then ( + let range_exprs = + AN.mk_range_expr ctx None ty (A.Ident (p, i)) |> List.map fst + in + List.map (fun expr -> + let c_expr = compile_ast_expr cstate ctx [] map expr in + X.max_binding c_expr |> snd + ) range_exprs @ cstate.global_constraints + ) + else cstate.global_constraints + in { cstate with free_constants = (!map.node_name, i, vt) :: cstate.free_constants; global_constraints diff --git a/src/lustre/typeCheckerContext.ml b/src/lustre/typeCheckerContext.ml index ec255c680..d4b98feec 100644 --- a/src/lustre/typeCheckerContext.ml +++ b/src/lustre/typeCheckerContext.ml @@ -676,6 +676,11 @@ let rec type_contains_subrange ctx = function (match lookup_ty ctx id with | Some ty -> type_contains_subrange ctx ty | _ -> assert false) + | UserType (_, ty_args, id) -> ( + match lookup_ty_syn ctx id ty_args with + | Some ty -> type_contains_subrange ctx ty + | None -> assert false + ) | _ -> false let rec type_contains_ref ctx = function diff --git a/src/transSys.ml b/src/transSys.ml index ea476cd1a..8da7441c5 100644 --- a/src/transSys.ml +++ b/src/transSys.ml @@ -1101,7 +1101,7 @@ let define_and_declare_of_bounds let assert_global_constraints { global_constraints } assert_term = - List.iter (fun c -> assert_term c) global_constraints + List.iter (fun c -> assert_term (Term.convert_select c)) global_constraints let init_uf_def { init_uf_symbol; init_formals; init } = (init_uf_symbol, (init_formals, init)) diff --git a/tests/regression/success/free_const_subrange.lus b/tests/regression/success/free_const_subrange.lus new file mode 100644 index 000000000..3de4c43a2 --- /dev/null +++ b/tests/regression/success/free_const_subrange.lus @@ -0,0 +1,14 @@ + +type Nat = subrange [0,*] of int; + +type T = [Nat,bool]; +type Rec = struct { f:T }; + +const R: Rec; +const C: Nat^2; + +node N() returns (ok: bool) +let + check "P1" C[0] >= 0; + check "P2" R.f.%0 >= 0; +tel \ No newline at end of file