From 81cdac9270b74e4523fe6bf3056486aba575b6dc Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 7 Aug 2023 12:16:16 +0200 Subject: [PATCH 1/5] Minor optimization --- src/lustre/lustreAstNormalizer.ml | 19 ++++++++++++------- src/lustre/lustreNodeGen.ml | 3 +-- 2 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 35cee7f65..20731ec5d 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -334,13 +334,17 @@ let extract_array_size = function let generalize_to_array_expr name ind_vars expr nexpr = let vars = AH.vars expr in - let ind_vars = List.map (fun (i, _) -> i) (StringMap.bindings ind_vars) in + let ind_vars = List.map fst (StringMap.bindings ind_vars) in let ind_vars = List.filter (fun x -> A.SI.mem x vars) ind_vars in - let (eq_lhs, nexpr) = if List.length ind_vars = 0 - then A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr - else A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]), + let (eq_lhs, nexpr) = + match ind_vars with + | [] -> + A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr + | _ -> + A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]), A.ArrayIndex (dpos, nexpr, A.Ident (dpos, List.hd ind_vars)) - in eq_lhs, nexpr + in + eq_lhs, nexpr let mk_fresh_local force info pos is_ghost ind_vars expr_type expr = match (LocalCache.find_opt local_cache expr, force) with @@ -369,7 +373,7 @@ let mk_fresh_array_ctor info pos ind_vars expr_type expr size_expr = equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; } in nexpr, gids -let mk_fresh_node_arg_local info pos is_const ind_vars expr_type expr = +let mk_fresh_node_arg_local info pos is_const expr_type expr = match NodeArgCache.find_opt node_arg_cache expr with | Some nexpr -> nexpr, empty () | None -> @@ -377,6 +381,7 @@ let mk_fresh_node_arg_local info pos is_const ind_vars expr_type expr = let prefix = HString.mk_hstring (string_of_int !i) in let name = HString.concat2 prefix (HString.mk_hstring "_gklocal") in let nexpr = A.Ident (pos, name) in + let ind_vars = info.inductive_variables in 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)]; @@ -1193,7 +1198,7 @@ and normalize_expr ?guard info map = (StringMap.choose_opt info.inductive_variables) |> get |> snd else Chk.infer_type_expr info.context expr |> unwrap in - let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ivars ty nexpr in + let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ty nexpr in iexpr, union gids1 gids2, warnings in function (* ************************************************************************ *) diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index 662481a26..d2b489482 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -510,8 +510,7 @@ let rec expand_tuple' pos accum bounds lhs rhs = let expand_tuple pos lhs rhs = (* Format.eprintf "expand_tuple: \n"; *) expand_tuple' pos [] [] - (List.map (fun (i, e) -> (i, e)) (X.bindings lhs)) - (List.map (fun (i, e) -> (i, e)) (X.bindings rhs)) + (X.bindings lhs) (X.bindings rhs) let compile_contract_item map count scope kind pos name expr = let scope = List.map (fun (i, s) -> i, HString.string_of_hstring s) scope in From 30de6ec7c186bc0d870515579a4e5611875a8236 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 7 Aug 2023 13:06:49 +0200 Subject: [PATCH 2/5] Fix: push array select --- src/lustre/lustreExpr.ml | 13 ++++++++++- src/lustre/lustreExpr.mli | 7 ++++++ src/lustre/lustreNodeGen.ml | 18 +++++++++------- src/terms/term.ml | 24 +++++++++++++++++++++ src/terms/term.mli | 4 ++++ tests/regression/falsifiable/array-ite2.lus | 6 ++++++ 6 files changed, 63 insertions(+), 9 deletions(-) create mode 100644 tests/regression/falsifiable/array-ite2.lus diff --git a/src/lustre/lustreExpr.ml b/src/lustre/lustreExpr.ml index 911029d03..78c8b8121 100644 --- a/src/lustre/lustreExpr.ml +++ b/src/lustre/lustreExpr.ml @@ -3752,9 +3752,20 @@ let numeral_of_expr = Term.numeral_of_term let unsafe_term_of_expr e = (e : Term.t) let unsafe_expr_of_term t = t +let push_select { expr_init; expr_step; expr_type } = + let expr_init' = Term.push_select expr_init in + let expr_step' = Term.push_select expr_step in + { expr_init = expr_init'; + expr_step = expr_step'; + expr_type + } + +let mk_select_and_push e1 e2 = + mk_select e1 e2 |> push_select + (* Local Variables: compile-command: "make -k -C .." indent-tabs-mode: nil End: -*) \ No newline at end of file +*) diff --git a/src/lustre/lustreExpr.mli b/src/lustre/lustreExpr.mli index 82f2084bc..ba031ec03 100644 --- a/src/lustre/lustreExpr.mli +++ b/src/lustre/lustreExpr.mli @@ -558,6 +558,13 @@ val mk_let : (Var.t * expr) list -> t -> t val apply_subst : (Var.t * expr) list -> t -> t +(** Return an expression where the top-level selects of the initial and/or + the step expressions (if any) have been pushed *) +val push_select : t -> t + +(** Make select from an array and push it *) +val mk_select_and_push : t -> t -> t + (* Local Variables: compile-command: "make -k -C .." diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index d2b489482..d1a07c519 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -145,7 +145,7 @@ let array_select_of_bounds_term bounds e = *) let array_select_of_indexes_expr indexes e = - List.fold_left (fun e i -> E.mk_select e (E.mk_index_var i)) e indexes + List.fold_left (fun e i -> E.mk_select_and_push e (E.mk_index_var i)) e indexes (* Try to make the types of two expressions line up. * If one expression is an array but the other is not, then insert a 'select' @@ -332,7 +332,7 @@ let rec expand_tuple' pos accum bounds lhs rhs = if Type.is_array expr_type then let index_type = Type.index_type_of_array expr_type in let index_arg = E.mk_of_expr ~as_type:index_type (E.mk_int_expr (Numeral.of_int idx)) in - let indexed_expr = E.mk_select expr index_arg in + let indexed_expr = E.mk_select_and_push expr index_arg in let accum = expand_tuple' pos accum bounds [(lhs_index_tl, state_var)] [([], indexed_expr)] @@ -390,7 +390,9 @@ let rec expand_tuple' pos accum bounds lhs rhs = in let expr_type = expr.E.expr_type in let array_index_types = Type.all_index_types_of_array expr_type in - let over_index_types (e, i) _ = E.mk_select e (E.mk_index_var i), succ i in + let over_index_types (e, i) _ = + E.mk_select_and_push e (E.mk_index_var i), succ i + in let expr, _ = List.fold_left over_index_types (expr, 0) array_index_types in expand_tuple' pos accum (E.Bound b :: bounds) ((lhs_index_tl, state_var) :: lhs_tl) @@ -891,12 +893,12 @@ and compile_ast_expr let rec mk_store acc a ri x = match ri with | X.ArrayIntIndex vi :: ri' -> let i = E.mk_int (Numeral.of_int vi) in - let a' = List.fold_left E.mk_select a acc in + let a' = List.fold_left E.mk_select_and_push a acc in let x = mk_store [i] a' ri' x in E.mk_store a i x | X.ArrayVarIndex vi :: ri' -> let i = E.mk_of_expr vi in - let a' = List.fold_left E.mk_select a acc in + let a' = List.fold_left E.mk_select_and_push a acc in let x = mk_store [i] a' ri' x in E.mk_store a i x | _ :: ri' -> mk_store acc a ri' x @@ -911,7 +913,7 @@ and compile_ast_expr | X.ArrayIntIndex _ :: _ | X.ArrayVarIndex _ :: _ -> () | _ -> raise Not_found); let old_v = List.fold_left (fun (acc, cpt) _ -> - E.mk_select acc (E.mk_index_var cpt), cpt + 1) (v, 0) i |> fst + E.mk_select_and_push acc (E.mk_index_var cpt), cpt + 1) (v, 0) i |> fst in let new_v = X.find cindex cexpr2' in if Flags.Arrays.smt () then let v' = mk_store [] v cindex new_v in X.add [] v' a @@ -964,7 +966,7 @@ and compile_ast_expr | _ -> assert false in let expr = X.fold over_expr expr X.empty in if E.type_of_lustre_expr v |> Type.is_array then - X.map (fun e -> E.mk_select e index) expr + X.map (fun e -> E.mk_select_and_push e index) expr else expr (* | X.ArrayIntIndex _ :: _, _ -> let over_expr = fun j v vals -> match j with @@ -991,7 +993,7 @@ and compile_ast_expr X.fold (fun j -> X.add (top :: j)) e acc | _ -> assert false in X.fold over_expr expr X.empty - | [], e -> X.singleton X.empty_index (E.mk_select e index) + | [], e -> X.singleton X.empty_index (E.mk_select_and_push e index) in push compiled_expr in diff --git a/src/terms/term.ml b/src/terms/term.ml index 00b95b473..13d919c09 100644 --- a/src/terms/term.ml +++ b/src/terms/term.ml @@ -1935,6 +1935,30 @@ let indexes_of_state_var sv term = (* inds *) +let push_select term = + let rec push_select' i t = + match destruct t with + | T.App (s, args) -> ( + match Symbol.node_of_symbol s, args with + | `ITE, [p; l; r] -> ( + mk_ite + p + (push_select' i l) + (push_select' i r) + ) + | _ -> (mk_select t i) + ) + | _ -> (mk_select t i) + in + match destruct term with + | T.App (s, args) -> ( + match Symbol.node_of_symbol s, args with + | `SELECT _, [a; i] -> ( + push_select' i a + ) + | _ -> term + ) + | _ -> term (* Return set of state variables at given offsets in term *) diff --git a/src/terms/term.mli b/src/terms/term.mli index d42bb2be6..5eb861246 100644 --- a/src/terms/term.mli +++ b/src/terms/term.mli @@ -725,6 +725,10 @@ val reinterpret_select : t -> t (** Return (array) indexes of a state variable appearing in a term *) val indexes_of_state_var : StateVar.t -> t -> t list list +(** Return a term where the top-level select of the given term has been pushed + until reaching a subterm that is not an ITE. If the top-level symbol is not + a select, then the given term is returned unaltered *) +val push_select : t -> t (** {1 Statistics} *) diff --git a/tests/regression/falsifiable/array-ite2.lus b/tests/regression/falsifiable/array-ite2.lus new file mode 100644 index 000000000..3f89a3bc8 --- /dev/null +++ b/tests/regression/falsifiable/array-ite2.lus @@ -0,0 +1,6 @@ + +node N(p: bool; A,B: int^2) returns (C: int^2); +let + C[i] = (if p then A else B)[i]; + check C[0]=0; +tel From 327212810c4ca4d82773bbaf115dc31c609af644 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 7 Aug 2023 13:22:27 +0200 Subject: [PATCH 3/5] Fix array access with subrange index --- src/lustre/lustreExpr.ml | 6 ++---- tests/regression/success/array-subrange-index.lus | 8 ++++++++ 2 files changed, 10 insertions(+), 4 deletions(-) create mode 100644 tests/regression/success/array-subrange-index.lus diff --git a/src/lustre/lustreExpr.ml b/src/lustre/lustreExpr.ml index 78c8b8121..bb96b8ee8 100644 --- a/src/lustre/lustreExpr.ml +++ b/src/lustre/lustreExpr.ml @@ -3562,8 +3562,7 @@ let type_of_select = function (function t -> - (* Second argument must match index type of array *) - if Type.check_type (Type.index_type_of_array s) t then + if (Type.is_int t || Type.is_int_range t) then (* Return type of array elements *) Type.elem_type_of_array s @@ -3605,8 +3604,7 @@ let type_of_store = function (fun i v -> - (* Second argument must match index type of array *) - if Type.check_type i (Type.index_type_of_array s) && + if (Type.is_int i || Type.is_int_range i) && Type.check_type (Type.elem_type_of_array s) v then diff --git a/tests/regression/success/array-subrange-index.lus b/tests/regression/success/array-subrange-index.lus new file mode 100644 index 000000000..7943e446d --- /dev/null +++ b/tests/regression/success/array-subrange-index.lus @@ -0,0 +1,8 @@ + +type I = subrange [0,1] of int; + +node N(j: I) returns (B: int^2) +let + B[i] = 0; + check B[j]=0; +tel \ No newline at end of file From 342ce3ff7c10430d2e89f06e94ad89c5db81f2d3 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 7 Aug 2023 15:54:29 +0200 Subject: [PATCH 4/5] Abstract array literals Commit 519ac4d fixed some issues related to array literals but introduced new issues. This commit follows a different approach with the aim of addressing all the issues. A new auxiliary equation of the form v = [...] is introduced for each array literal so that only these new introduced equations are expanded in Lustre Nodes. Fixes #994. --- src/lustre/generatedIdentifiers.ml | 3 + src/lustre/generatedIdentifiers.mli | 1 + src/lustre/lustreAstInlineConstants.ml | 18 ++-- src/lustre/lustreAstNormalizer.ml | 28 ++++++ src/lustre/lustreIndex.ml | 12 ++- src/lustre/lustreIndex.mli | 1 + src/lustre/lustreNodeGen.ml | 94 +++++++++++-------- .../falsifiable/array-node-output.lus | 7 ++ tests/regression/success/array-struct-ite.lus | 12 +++ tests/regression/success/test-issue-994.lus | 8 ++ 10 files changed, 135 insertions(+), 49 deletions(-) create mode 100644 tests/regression/falsifiable/array-node-output.lus create mode 100644 tests/regression/success/array-struct-ite.lus create mode 100644 tests/regression/success/test-issue-994.lus diff --git a/src/lustre/generatedIdentifiers.ml b/src/lustre/generatedIdentifiers.ml index 9322afb9f..7eb3491bc 100644 --- a/src/lustre/generatedIdentifiers.ml +++ b/src/lustre/generatedIdentifiers.ml @@ -68,6 +68,7 @@ type t = { * LustreAst.expr) list; nonvacuity_props: StringSet.t; + array_literal_vars: StringSet.t; } (* String constant used in lustreDesugarIfBlocks.ml and lustreDesugarFrameBlocks.ml @@ -106,6 +107,7 @@ let union ids1 ids2 = { expanded_variables = StringSet.union ids1.expanded_variables ids2.expanded_variables; equations = ids1.equations @ ids2.equations; nonvacuity_props = StringSet.union ids1.nonvacuity_props ids2.nonvacuity_props; + array_literal_vars = StringSet.union ids1.array_literal_vars ids2.array_literal_vars; } (* Same as union_keys, but we don't assume that identifiers are unique *) @@ -127,4 +129,5 @@ let union_keys2 key id1 id2 = match key, id1, id2 with expanded_variables = StringSet.empty; equations = []; nonvacuity_props = StringSet.empty; + array_literal_vars = StringSet.empty; } diff --git a/src/lustre/generatedIdentifiers.mli b/src/lustre/generatedIdentifiers.mli index 2e751d8d4..17c4f97a1 100644 --- a/src/lustre/generatedIdentifiers.mli +++ b/src/lustre/generatedIdentifiers.mli @@ -68,6 +68,7 @@ type t = { * LustreAst.expr) list; nonvacuity_props: StringSet.t; + array_literal_vars: StringSet.t; (* Variables equal to an array literal *) } (* String constant used in lustreDesugarIfBlocks.ml and lustreDesugarFrameBlocks.ml diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 10afe68ff..238deac2a 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -222,14 +222,18 @@ and simplify_array_index: TC.tc_context -> Lib.position -> LA.expr -> LA.expr -> = fun ctx pos e1 idx -> let e1' = simplify_expr ctx e1 in let idx' = simplify_expr ctx idx in + let raise_error () = + raise (Out_of_bounds (pos, "Array element access out of bounds.")) + in match e1' with | LA.GroupExpr (_, ArrayExpr, es) -> (match (eval_int_expr ctx idx) with - | Ok i -> if List.length es > i - then List.nth es i - else - (raise (Out_of_bounds (pos, "Array element access out of bounds."))) + | Ok i -> if List.length es > i then List.nth es i else raise_error () | Error _ -> LA.ArrayIndex (pos, e1', idx')) + | LA.ArrayConstr (_, v, s) -> + (match (eval_int_expr ctx idx), (eval_int_expr ctx s) with + | Ok i, Ok j -> if j > i then v else raise_error () + | _, _ -> LA.ArrayIndex (pos, e1', idx')) | _ -> ArrayIndex (pos, e1', idx') (** picks out the idx'th component of an array if it can *) @@ -353,10 +357,10 @@ and simplify_expr ?(is_guarded = false) ctx = | LA.ArrayConstr (pos, e1, e2) -> let e1' = simplify_expr ~is_guarded ctx e1 in let e2' = simplify_expr ~is_guarded ctx e2 in - let e' = LA.ArrayConstr (pos, e1', e2') in - (match (eval_int_expr ctx e2) with + let e' = LA.ArrayConstr (pos, e1', e2') in e' + (*(match (eval_int_expr ctx e2) with | Ok size -> LA.GroupExpr (pos, LA.ArrayExpr, Lib.list_init (fun _ -> e1') size) - | Error _ -> e') + | Error _ -> e')*) | LA.ArrayIndex (pos, e1, e2) -> simplify_array_index ctx pos e1 e2 | LA.ArrayConcat (pos, e1, e2) as e-> (match (simplify_expr ~is_guarded ctx e1, simplify_expr ~is_guarded ctx e2) with diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index 20731ec5d..30f4c327d 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -1187,6 +1187,26 @@ and combine_args_with_const info args flags = |> snd |> List.rev and normalize_expr ?guard info map = + let abstract_array_literal info expr nexpr = + let ivars = info.inductive_variables in + let pos = AH.pos_of_expr expr in + let ty = if expr_has_inductive_var ivars expr |> is_some then + (StringMap.choose_opt info.inductive_variables) |> get |> snd + else Chk.infer_type_expr info.context expr |> unwrap + in + let nexpr, gids = mk_fresh_local false info pos false ivars ty nexpr in + let id = + match nexpr with + | A.Ident (_, name) -> name + | _ -> assert false + in + let gids = + { gids with + array_literal_vars = StringSet.add id gids.array_literal_vars + } + in + nexpr, gids + in let abstract_node_arg ?guard force is_const info map expr = let nexpr, gids1, warnings = normalize_expr ?guard info map expr in if should_not_abstract force nexpr then @@ -1326,6 +1346,14 @@ and normalize_expr ?guard info map = let ivars = info.inductive_variables in let iexpr, gids2= mk_fresh_array_ctor info pos ivars ty nexpr size_expr in ArrayConstr (pos, iexpr, size_expr), union gids1 gids2, warnings + | GroupExpr (pos, ArrayExpr, expr_list) as expr -> + let nexpr_list, gids1, warnings = normalize_list + (normalize_expr ?guard:None info map) + expr_list + in + let nexpr = A.GroupExpr (pos, ArrayExpr, nexpr_list) in + let nexpr, gids2 = abstract_array_literal info expr nexpr in + nexpr, union gids1 gids2, warnings (* ************************************************************************ *) (* Variable renaming to ease handling contract scopes *) (* ************************************************************************ *) diff --git a/src/lustre/lustreIndex.ml b/src/lustre/lustreIndex.ml index 8b13a13e5..3bbe1aee5 100644 --- a/src/lustre/lustreIndex.ml +++ b/src/lustre/lustreIndex.ml @@ -266,6 +266,16 @@ let top_max_index t = with Not_found -> (-1) +let filter_array_indices index = List.filter ( + function + | ArrayVarIndex _ + | ArrayIntIndex _ -> false + | RecordIndex _ + | TupleIndex _ + | ListIndex _ + | AbstractTypeIndex _ -> true) + index + let compatible_one_index i1 i2 = match i1, i2 with | RecordIndex s1, RecordIndex s2 -> s1 = s2 | TupleIndex i1, TupleIndex i2 -> i1 = i2 @@ -309,7 +319,7 @@ let mk_scope_for_index index = |> String.length |> string_of_int |> Ident.of_string) - index + (filter_array_indices index) |> Scope.mk_scope diff --git a/src/lustre/lustreIndex.mli b/src/lustre/lustreIndex.mli index 657d62677..99f6e1254 100644 --- a/src/lustre/lustreIndex.mli +++ b/src/lustre/lustreIndex.mli @@ -101,6 +101,7 @@ val array_vars_of_index : index -> StateVar.t list [Invalid_argument "top_max_index"] if the first index is not a list *) val top_max_index : 'a t -> int +val filter_array_indices : index -> index val compatible_indexes : index -> index -> bool diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index d1a07c519..30690a541 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -61,6 +61,7 @@ type compiler_state = { type identifier_maps = { state_var : StateVar.t LustreIdent.Hashtbl.t; expr : LustreExpr.t LustreIndex.t LustreIdent.Hashtbl.t; + array_literal_index : LustreExpr.t LustreIndex.t LustreIdent.Hashtbl.t; source : LustreNode.state_var_source StateVar.StateVarHashtbl.t; bounds : (LustreExpr.expr LustreExpr.bound_or_fixed list) StateVar.StateVarHashtbl.t; @@ -112,6 +113,7 @@ let pp_print_identifier_maps ppf maps = let empty_identifier_maps node_name = { state_var = H.create 7; expr = H.create 7; + array_literal_index = H.create 7; source = SVT.create 7; bounds = SVT.create 7; array_index = H.create 7; @@ -168,21 +170,11 @@ let coalesce_array2 e1 e2 = only one state variable *) let state_var_of_expr expr = expr |> E.state_vars_of_expr |> SVS.choose -let filter_array_indices index = List.filter ( - function - | X.ArrayVarIndex _ - | X.ArrayIntIndex _ -> false - | X.RecordIndex _ - | X.TupleIndex _ - | X.ListIndex _ - | X.AbstractTypeIndex _ -> true) - index - let mk_state_var_name ident index = Format.asprintf "%a%a" (I.pp_print_ident true) ident (X.pp_print_index true) (* Filter out array indexes *) - (filter_array_indices index) + (X.filter_array_indices index) let bounds_of_index index = List.fold_left (fun acc -> function @@ -192,6 +184,25 @@ let bounds_of_index index = | _ -> acc ) [] index + +let update_array_literal_index map scope sv_ident index = + let compute_expr expr = + try + let t = H.find !map.array_literal_index sv_ident in + X.add index expr t + with Not_found -> X.singleton index expr + in + let state_var_name = mk_state_var_name sv_ident index in + let flatten_scopes = X.mk_scope_for_index index in + try + let state_var = StateVar.state_var_of_string + (state_var_name, + (List.map Ident.to_string (scope @ flatten_scopes))) + in + H.replace !map.array_literal_index sv_ident (compute_expr (E.mk_var state_var)) + with Not_found -> + assert false + (* Create a state variable for from an indexed state variable in a scope *) let mk_state_var @@ -308,6 +319,13 @@ let rec expand_tuple' pos accum bounds lhs rhs = " : ") " ; ") rhs; *) match lhs, rhs with + (* No more equations, return in original order *) + | [], [] -> accum + (* Indexes are not of equal length *) + | _, [] + | [], _ -> + internal_error pos "Type mismatch in equation: indexes not of equal length"; + assert false (* All indexes consumed *) | ([], state_var) :: lhs_tl, ([], expr) :: rhs_tl -> @@ -317,15 +335,9 @@ let rec expand_tuple' pos accum bounds lhs rhs = (* Only array indexes may be left at head of indexes *) | (X.ArrayVarIndex b :: lhs_index_tl, state_var) :: lhs_tl, ([], expr) :: rhs_tl -> - let expr_type = E.type_of_lustre_expr expr in - let bounds = if Type.is_array expr_type - then bounds - else (E.Bound b :: bounds) - in - expand_tuple' pos accum bounds + expand_tuple' pos accum (E.Bound b :: bounds) ((lhs_index_tl, state_var) :: lhs_tl) (([], expr) :: rhs_tl) - | (X.ArrayIntIndex _ :: _, _) :: _, [] -> accum | (X.ArrayIntIndex idx :: lhs_index_tl, state_var) :: lhs_tl, ([], expr) :: rhs_tl -> let expr_type = E.type_of_lustre_expr expr in @@ -495,13 +507,6 @@ let rec expand_tuple' pos accum bounds lhs rhs = | (X.AbstractTypeIndex _ :: _, _) :: _, (X.ListIndex _ :: _, _) :: _ | (X.AbstractTypeIndex _ :: _, _) :: _, (X.ArrayIntIndex _ :: _, _) :: _ | (X.AbstractTypeIndex _ :: _, _) :: _, (X.ArrayVarIndex _ :: _, _) :: _ - (* No more equations, return in original order *) - | [], [] -> accum - (* Indexes are not of equal length *) - | _, [] - | [], _ -> - internal_error pos "Type mismatch in equation: indexes not of equal length"; - assert false | (_ :: _, _) :: _, ([], _) :: _ | ([], _) :: _, (_ :: _, _) :: _ -> (internal_error pos "Type mismatch in equation: head indexes do not match"; @@ -538,6 +543,7 @@ let rec compile ctx gids decls = G.state_var_bounds = output.state_var_bounds} and compile_ast_type + ?(expand=false) (cstate:compiler_state) (ctx:Ctx.tc_context) map @@ -623,7 +629,7 @@ and compile_ast_type let array_size = (List.hd (X.values array_size')).expr_init in (* Old code does flattening here, but that flattening is only ever used once! And it is for a check, in lustreDeclarations line 423 *) - if AH.expr_is_const size_expr then + if expand then let upper = E.numeral_of_expr array_size in let result = ref X.empty in for ix = 0 to (Numeral.to_int upper - 1) do @@ -941,7 +947,7 @@ and compile_ast_expr else *) let over_indices = fun j (e:LustreExpr.t) a -> let e' = state_var_of_expr e |> E.mk_var - in X.add (X.ArrayVarIndex array_size :: j) e' a + in X.add (j @ [X.ArrayVarIndex array_size]) e' a in let result = X.fold over_indices cexpr X.empty in result @@ -1174,10 +1180,6 @@ and compile_node node_scope pos ctx cstate map outputs cond restart ident args d let ast_group_expr = A.GroupExpr (dummy_pos, A.ExprList, ast) in let cexpr = compile_ast_expr cstate ctx [] map ast_group_expr in let cexpr = flatten_list_indexes cexpr in - let cexpr_bindings = cexpr |> X.bindings - |> List.map (fun (indices, t) -> filter_array_indices indices, t) - in - let cexpr = List.fold_left (fun acc (index, e) -> X.add index e acc) X.empty cexpr_bindings in let over_indices i input_sv expr accum = let sv = state_var_of_expr expr in N.set_state_var_instance sv pos ident input_sv; @@ -1426,7 +1428,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.Input) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add (X.ListIndex n :: index) state_var accum | None -> accum @@ -1456,7 +1457,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.Output) in - let index = filter_array_indices index in let index' = if is_single then index else X.ListIndex n :: index in @@ -1486,7 +1486,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.Local) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add index state_var accum | None -> accum @@ -1515,11 +1514,22 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (if is_ghost then Some N.KGhost else None) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add index state_var accum | None -> accum - in let result = X.fold over_indices index_types X.empty in + in + let result = X.fold over_indices index_types X.empty in + if GI.StringSet.mem id gids.GI.array_literal_vars then ( + (* Store expanded type index *) + let index_types' = compile_ast_type ~expand:true cstate ctx map expr_type in + X.iter + (fun index _ -> + update_array_literal_index map (node_scope @ I.reserved_scope) + ident + index + ) + index_types' + ) ; result :: glocals in List.fold_left over_generated_locals [] locals_list (* ****************************************************************** *) @@ -1538,7 +1548,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.KGhost) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add index state_var accum | None -> accum @@ -1562,7 +1571,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.KLocal) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add index state_var accum | None -> accum @@ -1592,7 +1600,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type None in - let index = filter_array_indices index in match possible_state_var with | Some(state_var) -> if not (StateVar.is_input state_var) @@ -1668,7 +1675,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.Oracle) in - let index = filter_array_indices index in match possible_state_var with | Some(state_var) -> (match closed_sv with @@ -1695,7 +1701,6 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it index_type (Some N.Oracle) in - let index = filter_array_indices index in match possible_state_var with | Some state_var -> X.add index state_var accum | None -> accum @@ -1883,6 +1888,13 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it map := { !map with contract_scope }; let eq_lhs, indexes = match lhs with | A.StructDef (_, []) -> X.empty, 0 + | A.StructDef (_, [A.SingleIdent (_, i)]) when (GI.StringSet.mem i gids.GI.array_literal_vars) -> ( + (* Use expanded version of the equation *) + let ident = mk_ident i in + let idx = H.find !map.array_literal_index ident in + let result = X.map (fun e -> state_var_of_expr e) idx in + result, 0 + ) | A.StructDef (_, [e]) -> (compile_struct_item e) | A.StructDef (_, l) -> let construct_index i j e a = X.add (X.ListIndex i :: j) e a in diff --git a/tests/regression/falsifiable/array-node-output.lus b/tests/regression/falsifiable/array-node-output.lus new file mode 100644 index 000000000..a9d9b3743 --- /dev/null +++ b/tests/regression/falsifiable/array-node-output.lus @@ -0,0 +1,7 @@ +node imported F() returns (z:int^3); + +node N() returns (y:int^3); +let + y = F(); + check y[0]=0; +tel diff --git a/tests/regression/success/array-struct-ite.lus b/tests/regression/success/array-struct-ite.lus new file mode 100644 index 000000000..e72d7a51a --- /dev/null +++ b/tests/regression/success/array-struct-ite.lus @@ -0,0 +1,12 @@ +const N = 3; + +type rec = { + x: int; + y: int; +}; + +node N(in: rec^N; e: rec) returns (out: rec^N); +let + out[i] = if i = 0 then e else in[i]; + check out[0]=e; +tel \ No newline at end of file diff --git a/tests/regression/success/test-issue-994.lus b/tests/regression/success/test-issue-994.lus new file mode 100644 index 000000000..8cffd0e64 --- /dev/null +++ b/tests/regression/success/test-issue-994.lus @@ -0,0 +1,8 @@ +type rational = { n: int; d: int }; + +node Test () returns () +var rats: rational^4; +let + rats[i] = if i = 0 then rational { n = 0 ; d = 1} else rational { n = rats[i-1].n ; d = 1}; + check rats[0].n=0; +tel \ No newline at end of file From 5c27d8fede6ae317fa648cb24dc972efd24b3b13 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 8 Aug 2023 23:41:45 +0200 Subject: [PATCH 5/5] Fix multidimensional array constructor Fixes #951 --- src/lustre/lustreNodeGen.ml | 3 ++- tests/regression/success/test-issue-951.lus | 12 ++++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/regression/success/test-issue-951.lus diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index 30690a541..d41f2d058 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -405,7 +405,8 @@ let rec expand_tuple' pos accum bounds lhs rhs = let over_index_types (e, i) _ = E.mk_select_and_push e (E.mk_index_var i), succ i in - let expr, _ = List.fold_left over_index_types (expr, 0) array_index_types in + let start = (List.length lhs_index_tl + 1) - List.length array_index_types in + let expr, _ = List.fold_left over_index_types (expr, start) array_index_types in expand_tuple' pos accum (E.Bound b :: bounds) ((lhs_index_tl, state_var) :: lhs_tl) ((rhs_index_tl, expr) :: rhs_tl) diff --git a/tests/regression/success/test-issue-951.lus b/tests/regression/success/test-issue-951.lus new file mode 100644 index 000000000..d7970e529 --- /dev/null +++ b/tests/regression/success/test-issue-951.lus @@ -0,0 +1,12 @@ +node master__Operator1 ( input1:int^3 ) returns ( output1:int^3^2 ) + var + Edge_3:int^3; + Edge_4:int^3^2; + + let + Edge_3 = input1; + Edge_4 = Edge_3 ^ 2; + output1 = Edge_4; + --%MAIN ; + check output1[1][0] = input1[0]; + tel \ No newline at end of file