Skip to content

Commit

Permalink
Abstract array literals
Browse files Browse the repository at this point in the history
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 kind2-mc#994.
  • Loading branch information
daniel-larraz committed Aug 7, 2023
1 parent 3272128 commit 342ce3f
Show file tree
Hide file tree
Showing 10 changed files with 135 additions and 49 deletions.
3 changes: 3 additions & 0 deletions src/lustre/generatedIdentifiers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand All @@ -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;
}
1 change: 1 addition & 0 deletions src/lustre/generatedIdentifiers.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 11 additions & 7 deletions src/lustre/lustreAstInlineConstants.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down
28 changes: 28 additions & 0 deletions src/lustre/lustreAstNormalizer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
(* ************************************************************************ *)
Expand Down
12 changes: 11 additions & 1 deletion src/lustre/lustreIndex.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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


Expand Down
1 change: 1 addition & 0 deletions src/lustre/lustreIndex.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
94 changes: 53 additions & 41 deletions src/lustre/lustreNodeGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 ->
Expand All @@ -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
Expand Down Expand Up @@ -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";
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
(* ****************************************************************** *)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 342ce3f

Please sign in to comment.