Skip to content

Commit

Permalink
Merge pull request #950 from lorchrob/frame-if-ivc-refine
Browse files Browse the repository at this point in the history 
Refining IVC analysis for frame and if blocks
  • Loading branch information
@daniel-larraz
daniel-larraz authored Mar 10, 2023
2 parents be1c9a7 + 5a91491 commit d244725
Show file tree
Hide file tree
Showing 3 changed files with 130 additions and 58 deletions.
148 changes: 101 additions & 47 deletions src/lustre/lustreDesugarFrameBlocks.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,12 @@ type warning = [

let mk_warning pos kind = `LustreDesugarFrameBlocksWarning (pos, kind)

type eq_or_framecond =
| Eq of A.eq_lhs
| FCond of A.eq_lhs

(* First position is frame block header, second position is of the specific equation *)
let pos_list_map : (Lib.position * A.eq_lhs * Lib.position) list HString.HStringHashtbl.t =
let pos_list_map : (Lib.position * eq_or_framecond) list HString.HStringHashtbl.t =
HString.HStringHashtbl.create 20

let warn_unguarded_pres nis pos =
Expand All @@ -77,68 +81,81 @@ let split3 triples =
(** Parses an expression and replaces any ITE oracles with the 'fill'
expression (which is stuttering, ie, 'pre variable').
*)
let rec fill_ite_helper fill = function
let rec fill_ite_helper frame_pos node_id lhs id fill = function
(* Replace all oracles with 'fill' *)
| A.Ident (pos, i) ->
(* See if 'i' is of the form "n_iboracle" *)
if GI.var_is_iboracle i then fill else A.Ident(pos, i)
if GI.var_is_iboracle i
then (
(* First, record that frame var "i" was actually used for stuttering *)
let frame_info = [(frame_pos, FCond lhs)] in
(* If there is already a binding, we want to retain the old 'frame_info' *)
let frame_info = match HString.HStringHashtbl.find_opt pos_list_map node_id with
| Some frame_info2 -> frame_info @ frame_info2
| None -> frame_info
in
HString.HStringHashtbl.add pos_list_map node_id frame_info;

fill
)
else A.Ident(pos, i)

(* Everything else is just recursing to find Idents *)
| Pre (a, e) -> Pre (a, fill_ite_helper fill e)
| Arrow (a, e1, e2) -> Arrow (a, fill_ite_helper fill e1, fill_ite_helper fill e2)
| Pre (a, e) -> Pre (a, fill_ite_helper frame_pos node_id lhs id fill e)
| Arrow (a, e1, e2) -> Arrow (a, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| Const _ as e -> e
| ModeRef _ as e -> e

| RecordProject (a, e, b) -> RecordProject (a, fill_ite_helper fill e, b)
| ConvOp (a, b, e) -> ConvOp (a, b, fill_ite_helper fill e)
| UnaryOp (a, b, e) -> UnaryOp (a, b, fill_ite_helper fill e)
| Current (a, e) -> Current (a, fill_ite_helper fill e)
| When (a, e, b) -> When (a, fill_ite_helper fill e, b)
| TupleProject (a, e, b) -> TupleProject (a, fill_ite_helper fill e, b)
| Quantifier (a, b, c, e) -> Quantifier (a, b, c, fill_ite_helper fill e)
| BinaryOp (a, b, e1, e2) -> BinaryOp (a, b, fill_ite_helper fill e1, fill_ite_helper fill e2)
| CompOp (a, b, e1, e2) -> CompOp (a, b, fill_ite_helper fill e1, fill_ite_helper fill e2)
| ArrayConcat (a, e1, e2) -> ArrayConcat (a, fill_ite_helper fill e1, fill_ite_helper fill e2)
| ArrayIndex (a, e1, e2) -> ArrayIndex (a, fill_ite_helper fill e1, fill_ite_helper fill e2)
| ArrayConstr (a, e1, e2) -> ArrayConstr (a, fill_ite_helper fill e1, fill_ite_helper fill e2)
| Fby (a, e1, b, e2) -> Fby (a, fill_ite_helper fill e1, b, fill_ite_helper fill e2)
| TernaryOp (a, b, e1, e2, e3) -> TernaryOp (a, b, fill_ite_helper fill e1, fill_ite_helper fill e2, fill_ite_helper fill e3)
| ArraySlice (a, e1, (e2, e3)) -> ArraySlice (a, fill_ite_helper fill e1, (fill_ite_helper fill e2, fill_ite_helper fill e3))
| RecordProject (a, e, b) -> RecordProject (a, fill_ite_helper frame_pos node_id lhs id fill e, b)
| ConvOp (a, b, e) -> ConvOp (a, b, fill_ite_helper frame_pos node_id lhs id fill e)
| UnaryOp (a, b, e) -> UnaryOp (a, b, fill_ite_helper frame_pos node_id lhs id fill e)
| Current (a, e) -> Current (a, fill_ite_helper frame_pos node_id lhs id fill e)
| When (a, e, b) -> When (a, fill_ite_helper frame_pos node_id lhs id fill e, b)
| TupleProject (a, e, b) -> TupleProject (a, fill_ite_helper frame_pos node_id lhs id fill e, b)
| Quantifier (a, b, c, e) -> Quantifier (a, b, c, fill_ite_helper frame_pos node_id lhs id fill e)
| BinaryOp (a, b, e1, e2) -> BinaryOp (a, b, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| CompOp (a, b, e1, e2) -> CompOp (a, b, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| ArrayConcat (a, e1, e2) -> ArrayConcat (a, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| ArrayIndex (a, e1, e2) -> ArrayIndex (a, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| ArrayConstr (a, e1, e2) -> ArrayConstr (a, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2)
| Fby (a, e1, b, e2) -> Fby (a, fill_ite_helper frame_pos node_id lhs id fill e1, b, fill_ite_helper frame_pos node_id lhs id fill e2)
| TernaryOp (a, b, e1, e2, e3) -> TernaryOp (a, b, fill_ite_helper frame_pos node_id lhs id fill e1, fill_ite_helper frame_pos node_id lhs id fill e2, fill_ite_helper frame_pos node_id lhs id fill e3)
| ArraySlice (a, e1, (e2, e3)) -> ArraySlice (a, fill_ite_helper frame_pos node_id lhs id fill e1, (fill_ite_helper frame_pos node_id lhs id fill e2, fill_ite_helper frame_pos node_id lhs id fill e3))

| GroupExpr (a, b, l) -> GroupExpr (a, b, List.map (fill_ite_helper fill) l)
| NArityOp (a, b, l) -> NArityOp (a, b, List.map (fill_ite_helper fill) l)
| Call (a, b, l) -> Call (a, b, List.map (fill_ite_helper fill) l)
| CallParam (a, b, c, l) -> CallParam (a, b, c, List.map (fill_ite_helper fill) l)
| GroupExpr (a, b, l) -> GroupExpr (a, b, List.map (fill_ite_helper frame_pos node_id lhs id fill) l)
| NArityOp (a, b, l) -> NArityOp (a, b, List.map (fill_ite_helper frame_pos node_id lhs id fill) l)
| Call (a, b, l) -> Call (a, b, List.map (fill_ite_helper frame_pos node_id lhs id fill) l)
| CallParam (a, b, c, l) -> CallParam (a, b, c, List.map (fill_ite_helper frame_pos node_id lhs id fill) l)

| Merge (a, b, l) -> Merge (a, b,
List.combine
(List.map fst l)
(List.map (fill_ite_helper fill) (List.map snd l)))
(List.map (fill_ite_helper frame_pos node_id lhs id fill) (List.map snd l)))

| RecordExpr (a, b, l) -> RecordExpr (a, b,
List.combine
(List.map fst l)
(List.map (fill_ite_helper fill) (List.map snd l)))
(List.map (fill_ite_helper frame_pos node_id lhs id fill) (List.map snd l)))

| RestartEvery (a, b, l, e) ->
RestartEvery (a, b, List.map (fill_ite_helper fill) l, fill_ite_helper fill e)
RestartEvery (a, b, List.map (fill_ite_helper frame_pos node_id lhs id fill) l, fill_ite_helper frame_pos node_id lhs id fill e)
| Activate (a, b, e, r, l) ->
Activate (a, b, (fill_ite_helper fill) e, (fill_ite_helper fill) r, List.map (fill_ite_helper fill) l)
Activate (a, b, (fill_ite_helper frame_pos node_id lhs id fill) e, (fill_ite_helper frame_pos node_id lhs id fill) r, List.map (fill_ite_helper frame_pos node_id lhs id fill) l)
| Condact (a, e, r, b, l1, l2) ->
Condact (a, (fill_ite_helper fill) e, (fill_ite_helper fill) r, b,
List.map (fill_ite_helper fill) l1, List.map (fill_ite_helper fill) l2)
Condact (a, (fill_ite_helper frame_pos node_id lhs id fill) e, (fill_ite_helper frame_pos node_id lhs id fill) r, b,
List.map (fill_ite_helper frame_pos node_id lhs id fill) l1, List.map (fill_ite_helper frame_pos node_id lhs id fill) l2)

| StructUpdate (a, e1, li, e2) ->
A.StructUpdate (a, fill_ite_helper fill e1,
A.StructUpdate (a, fill_ite_helper frame_pos node_id lhs id fill e1,
List.map (function
| A.Label (a, b) -> A.Label (a, b)
| Index (a, e) -> Index (a, fill_ite_helper fill e)
| Index (a, e) -> Index (a, fill_ite_helper frame_pos node_id lhs id fill e)
) li,
fill_ite_helper fill e2)
fill_ite_helper frame_pos node_id lhs id fill e2)

(** Helper function to generate node equations when an initialized variable in the
frame block is left undefined in the frame block body. *)
let generate_undefined_nes nis ne = match ne with
let generate_undefined_nes f_pos node_id nis ne = match ne with
| A.Equation (pos, (StructDef(_, [SingleIdent(_, id)]) as lhs), init) ->
(* Find the corresponding node item in frame block body. *)
let res = List.find_opt (fun ni -> match ni with
Expand All @@ -150,7 +167,17 @@ let generate_undefined_nes nis ne = match ne with
(* Already defined in frame block *)
| Some _ -> R.ok []
(* Fill in equation in frame block body *)
| None -> R.ok [A.Body(A.Equation(pos, lhs, Arrow(pos2, init, Pre(pos2, Ident (pos2, id)))))]
| None ->
(* First, record that frame var "id" was actually used for stuttering *)
let frame_info = [(f_pos, FCond lhs)] in
(* If there is already a binding, we want to retain the old 'frame_info' *)
let frame_info = match HString.HStringHashtbl.find_opt pos_list_map node_id with
| Some frame_info2 -> frame_info @ frame_info2
| None -> frame_info
in
HString.HStringHashtbl.add pos_list_map node_id frame_info;

R.ok [A.Body(A.Equation(pos, lhs, Arrow(pos2, init, Pre(pos2, Ident (pos2, id)))))]
)
| A.Equation (pos, (StructDef(_, [ArrayDef(_, id1, id2)]) as lhs), init) ->
(* Find the corresponding node item in frame block body. *)
Expand All @@ -168,7 +195,17 @@ let generate_undefined_nes nis ne = match ne with
(* Already defined in frame block *)
| Some _ -> R.ok []
(* Fill in equation in frame block body *)
| None -> R.ok [A.Body(A.Equation(pos, lhs, Arrow(pos2, init, Pre(pos2, build_array_index (List.rev id2)))))]
| None ->
(* First, record that frame var "id1" was actually used for stuttering *)
let frame_info = [(f_pos, FCond lhs)] in
(* If there is already a binding, we want to retain the old 'frame_info' *)
let frame_info = match HString.HStringHashtbl.find_opt pos_list_map node_id with
| Some frame_info2 -> frame_info @ frame_info2
| None -> frame_info
in
HString.HStringHashtbl.add pos_list_map node_id frame_info;

R.ok [A.Body(A.Equation(pos, lhs, Arrow(pos2, init, Pre(pos2, build_array_index (List.rev id2)))))]
)
(* Assert in frame block guard *)
| A.Assert(pos, _) -> mk_error pos (MisplacedNodeItemError (A.Body ne))
Expand All @@ -180,7 +217,7 @@ let generate_undefined_nes nis ne = match ne with
(** Helper function to generate node equations when a variable in the
frame block var list is left undefined in the frame block body AND has
no initialization. *)
let generate_undefined_nes_no_init pos nes nis var =
let generate_undefined_nes_no_init node_id pos nes nis var =
(* Find var's corresponding node item in frame block body *)
match (List.find_opt (fun ni -> match ni with
| A.Body (A.Equation (_, StructDef(_, [SingleIdent(_, i)]), _)) when i = var -> true
Expand All @@ -199,14 +236,25 @@ let generate_undefined_nes_no_init pos nes nis var =
with
(* Already defined in frame block initialization *)
| Some _ -> R.ok []
| None -> R.ok [A.Body(A.Equation(pos, StructDef(pos, [SingleIdent (pos, var)]), Pre(pos, Ident (pos, var))))]
| None ->
let lhs = A.StructDef(pos, [SingleIdent (pos, var)]) in
(* First, record that frame var "var" was actually used for stuttering *)
let frame_info = [(pos, FCond lhs)] in
(* If there is already a binding, we want to retain the old 'frame_info' *)
let frame_info = match HString.HStringHashtbl.find_opt pos_list_map node_id with
| Some frame_info2 -> frame_info @ frame_info2
| None -> frame_info
in
HString.HStringHashtbl.add pos_list_map node_id frame_info;

R.ok [A.Body(A.Equation(pos, lhs, Pre(pos, Ident (pos, var))))]




(** Helper function to fill in ITE oracles and guard equations with specified
initialization values (if present). *)
let fill_ite_oracles nes ni =
let fill_ite_oracles f_pos node_id nes ni =
match ni with
| A.Body (Equation (pos, (StructDef(_, [SingleIdent(_, i)]) as lhs), e)) ->
(* Find initialization value *)
Expand All @@ -218,9 +266,9 @@ match ni with
(match init with
| Some init ->
R.ok (A.Body (Equation (pos, lhs, (A.Arrow (pos2, init,
fill_ite_helper (A.Pre (pos2, Ident(pos2, i))) e)))))
fill_ite_helper f_pos node_id lhs i (A.Pre (pos2, Ident(pos2, i))) e)))))
| None ->
R.ok (A.Body (Equation (pos, lhs, fill_ite_helper
R.ok (A.Body (Equation (pos, lhs, fill_ite_helper f_pos node_id lhs i
(A.Pre (pos2, Ident(pos2, i)))
e))))
| A.Body (Equation (pos, (StructDef(_, [ArrayDef(_, i1, inds1)]) as lhs), e)) ->
Expand All @@ -234,9 +282,9 @@ match ni with
(match init with
| Some init ->
R.ok (A.Body (Equation (pos, lhs, (A.Arrow (pos2, init,
fill_ite_helper (A.Pre (pos2, array_index)) e)))))
fill_ite_helper f_pos node_id lhs i1 (A.Pre (pos2, array_index)) e)))))
| None ->
R.ok (A.Body (Equation (pos, lhs, fill_ite_helper
R.ok (A.Body (Equation (pos, lhs, fill_ite_helper f_pos node_id lhs i1
(A.Pre (pos2, array_index))
e))))
(* The following node items should not be in frame blocks. In particular,
Expand All @@ -263,22 +311,28 @@ match ni with
let desugar_node_item node_id ni = match ni with
(* All multiple assignment is removed in lustreRemoveMultAssign.ml *)
| A.FrameBlock (pos, vars, nes, nis) ->
let* nis = R.seq (List.map (fill_ite_oracles nes) nis) in
let* nis2 = R.seq (List.map (generate_undefined_nes nis) nes) in
let* nis = R.seq (List.map (fill_ite_oracles pos node_id nes) nis) in
let* nis2 = R.seq (List.map (generate_undefined_nes pos node_id nis) nes) in
let nis2 = List.flatten nis2 in
let* nis3 = R.seq (List.map (generate_undefined_nes_no_init pos nes nis) vars) in
let* nis3 = R.seq (List.map (generate_undefined_nes_no_init node_id pos nes nis) vars) in
let nis3 = List.flatten nis3 in
let warnings = warn_unguarded_pres (nis @ nis3) pos |> List.flatten in


(* Frame block header info *)
let frame_info = (List.map (fun ne -> match ne with
| A.Equation (_, lhs, expr) -> (pos, lhs, AH.pos_of_expr expr)
| A.Equation (_, lhs, expr) -> (AH.pos_of_expr expr, Eq lhs)
| _ -> assert false) nes) in
(* If there is already a binding, we want to retain the old 'frame_info' *)
let frame_info = match HString.HStringHashtbl.find_opt pos_list_map node_id with
| Some frame_info2 -> frame_info @ frame_info2
| None -> frame_info
in
(* Record node equation LHSs so we can add state var defs later *)
HString.HStringHashtbl.add pos_list_map node_id frame_info;



R.ok ([], nis @ nis2 @ nis3, warnings)
| _ -> R.ok ([], [ni], [])

Expand Down
6 changes: 5 additions & 1 deletion src/lustre/lustreDesugarFrameBlocks.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,12 @@ type warning = [

val warning_message : warning_kind -> string

type eq_or_framecond =
| Eq of A.eq_lhs
| FCond of A.eq_lhs

(* First position is frame block header, second position is of the specific equation *)
val pos_list_map :(Lib.position * A.eq_lhs * Lib.position) list HString.HStringHashtbl.t
val pos_list_map : (Lib.position * eq_or_framecond) list HString.HStringHashtbl.t

val desugar_frame_blocks :
A.declaration list ->
Expand Down
34 changes: 24 additions & 10 deletions src/lustre/lustreNodeGen.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1910,9 +1910,19 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it
match lhs with
| A.StructDef (_, []) -> eqns
| _ -> (
let eq_lhs, indexes = match lhs with
let (eq_lhs, indexes), is_generated = match lhs with
| A.StructDef (_, []) -> assert false (* (X.empty, 0) *)
| A.StructDef (_, [e]) -> compile_struct_item e
| A.StructDef (_, [e]) as lhs1 ->
(* Detect if equation is result of desugaring a frame block *)
let is_generated = match HString.HStringHashtbl.find_opt LDF.pos_list_map i with
| None -> false
| Some frame_infos -> (
match List.find_opt (fun (_, lhs) -> match lhs with | LDF.FCond lhs2 -> lhs1 = lhs2 | _ -> false)
frame_infos with
| None -> false
| Some _ -> true
) in
compile_struct_item e, is_generated
| A.StructDef (_, l) ->
let construct_index =
fun i j e a -> X.add (X.ListIndex i :: j) e a
Expand All @@ -1922,9 +1932,9 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it
i + 1, X.fold (construct_index i) t accum
in
let _, res = List.fold_left over_items (0, X.empty) l
in res, 0
in (res, 0), false
in
let lhs_bounds = gen_lhs_bounds false eq_lhs ast_expr indexes in
let lhs_bounds = gen_lhs_bounds is_generated eq_lhs ast_expr indexes in
let eq_rhs = compile_ast_expr cstate ctx lhs_bounds map ast_expr in
let eq_rhs = flatten_list_indexes eq_rhs in
(* Format.eprintf "lhs: %[email protected]: %a@.@."
Expand Down Expand Up @@ -2071,13 +2081,17 @@ and compile_node_decl gids is_function cstate ctx i ext inputs outputs locals it
match HString.HStringHashtbl.find_opt LDF.pos_list_map i with
| Some frame_infos ->
(* Get state variables for frame block variables *)
List.iter (fun (pos, lhs, pos2) ->
let lhs, _ = (match lhs with
| A.StructDef (_, [e]) -> compile_struct_item e
List.iter (fun (pos, def) ->
(match def with
(* Adding state vars for frame block equations *)
| LDF.Eq A.StructDef (_, [e]) ->
let lhs, _ = compile_struct_item e in
List.iter (fun (i, sv) -> N.add_state_var_def sv (N.ProperEq (pos, rm_array_var_index i))) (X.bindings lhs);
(* Adding state vars for frame block headers *)
| FCond A.StructDef (_, [e]) ->
let lhs, _ = compile_struct_item e in
List.iter (fun (_, sv) -> N.add_state_var_def sv (N.FrameBlock pos)) (X.bindings lhs);
| _ -> assert false)
in
List.iter (fun (_, sv) -> N.add_state_var_def sv (N.FrameBlock pos)) (X.bindings lhs);
List.iter (fun (i, sv) -> N.add_state_var_def sv (N.ProperEq (pos2, rm_array_var_index i))) (X.bindings lhs);
) frame_infos;
| None -> ()
);
Expand Down

0 comments on commit d244725

Please sign in to comment.