Skip to content
GitLab
Commit 7158d4dd authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Improvement in the handling of boolean expressions. 

The following changes are introduced:
- If-statements and asserts have now an op-type.
- If-statements are primitive (not encoded with switch).
- The && and || operators are implemented using IfE.
- The front-end uses better types for conditionals and asserts.
parent 230fb1b3
Pipeline #50542 passed with stage
in 16 minutes and 33 seconds
Hide whitespace changes
Inline Side-by-side
examples/tests.c
View file @ 7158d4dd
#include <stddef.h>
#include <stdbool.h>
#include <stdint.h>
// Random tests.
[[rc::returns("void")]]
......@@ -79,3 +80,15 @@ int inline_global1() {
int inline_global2() {
return inline_global1();
}
[[rc::returns("void")]]
void test_logical(){
if ((1 && 2) || 0/0) {
assert(1);
} else {
assert(0);
}
assert((1 && 2) == 1 && (2 || 0) == 1);
if(INT_MAX) { assert(1); } else { assert(0); }
assert(UINT_MAX);
}
frontend/ail_to_coq.ml
View file @ 7158d4dd
......@@ -456,8 +456,8 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
| Gt -> GtOp
| Le -> LeOp
| Ge -> GeOp
| And -> not_impl loc "nested && operator"
| Or -> not_impl loc "nested || operator"
| And -> LazyAndOp
| Or -> LazyOrOp
| Comma -> CommaOp
| Arithmetic(op) ->
arith_op := true;
......@@ -813,30 +813,6 @@ and translate_call : type a. a call_place -> loc -> bool -> ail_expr
in
Call_simple(e, es)
type bool_expr =
| BE_leaf of ail_expr
| BE_neg of bool_expr
| BE_and of bool_expr * bool_expr
| BE_or of bool_expr * bool_expr
let rec bool_expr : ail_expr -> bool_expr = fun e ->
match strip_expr e with
| AilEbinary(e1,And,e2) -> BE_and(bool_expr e1, bool_expr e2)
| AilEbinary(e1,Or ,e2) -> BE_or(bool_expr e1, bool_expr e2)
| AilEbinary(e1,Eq ,e2) ->
begin
let be1 = bool_expr e1 in
let be2 = bool_expr e2 in
match (is_const_0 e1, be1, is_const_0 e2, be2) with
| (false, _ , false, _ )
| (true , _ , true , _ )
| (false, BE_leaf(_), true , _ )
| (true , _ , false, BE_leaf(_)) -> BE_leaf(e)
| (false, _ , true , _ ) -> BE_neg(be1)
| (true , _ , false, _ ) -> BE_neg(be2)
end
| _ -> BE_leaf(e)
let add_block ?annots id s blocks =
if SMap.mem id blocks then assert false;
let annots =
......@@ -846,35 +822,6 @@ let add_block ?annots id s blocks =
in
SMap.add id (annots, s) blocks
let translate_bool_expr then_goto else_goto blocks e =
let rec translate then_goto else_goto blocks be =
match be with
| BE_leaf(e) ->
let e = translate_expr false (Some(OpInt(ItBool))) e in
(mkloc (If(e, then_goto, else_goto)) e.loc, blocks)
| BE_neg(be) ->
translate else_goto then_goto blocks be
| BE_and(be1,be2) ->
let id = fresh_block_id () in
let id_goto = noloc (Goto(id)) in (* FIXME loc *)
let (s, blocks) = translate id_goto else_goto blocks be1 in
let blocks =
let (s, blocks) = translate then_goto else_goto blocks be2 in
add_block id s blocks
in
(s, blocks)
| BE_or (be1,be2) ->
let id = fresh_block_id () in
let id_goto = noloc (Goto(id)) in (* FIXME loc *)
let (s, blocks) = translate then_goto id_goto blocks be1 in
let blocks =
let (s, blocks) = translate then_goto else_goto blocks be2 in
add_block id s blocks
in
(s, blocks)
in
translate then_goto else_goto blocks (bool_expr e)
(* Insert local variables. *)
let insert_bindings bindings =
let fn (id, ((loc, _, _), _, c_ty)) =
......@@ -996,6 +943,11 @@ let k_stack_print : out_channel -> k_data list -> unit = fun oc l ->
let translate_block stmts blocks ret_ty =
let translate_bool_expr then_goto else_goto e =
let ot = op_type_of_tc (loc_of e) (tc_of e) in
let e = translate_expr false None e in
mkloc (If(ot, e, then_goto, else_goto)) e.loc
in
let rec trans extra_attrs swstk ks stmts blocks =
let open AilSyntax in
if debug then Printf.eprintf "[trans] %a" k_stack_print ks;
......@@ -1052,8 +1004,9 @@ let translate_block stmts blocks ret_ty =
let loc_full = loc_of e in
match strip_expr e with
| AilEassert(e) ->
let e = translate_expr false (Some(OpInt(ItBool))) e in
locate (Assert(e, stmt))
let ot = op_type_of_tc (loc_of e) (tc_of e) in
let e = translate_expr false None e in
locate (Assert(ot, e, stmt))
| AilEassign(e1,e2) ->
let atomic = is_atomic_tc (tc_of e1) in
let e1 = translate_expr true None e1 in
......@@ -1131,7 +1084,7 @@ let translate_block stmts blocks ret_ty =
let blocks = add_block id_else s blocks in
(blocks, mkloc (Goto(id_else)) s.loc)
in
translate_bool_expr then_goto else_goto blocks e
(translate_bool_expr then_goto else_goto e, blocks)
| AilSwhile(e,s,_) ->
let attrs = extra_attrs @ attrs in
let id_cond = fresh_block_id () in
......@@ -1153,9 +1106,7 @@ let translate_block stmts blocks ret_ty =
(blocks, mkloc (Goto(id_body)) s.loc)
in
(* Translate the condition. *)
let (s, blocks) =
translate_bool_expr goto_body goto_cont blocks e
in
let s = translate_bool_expr goto_body goto_cont e in
let blocks =
let annots =
attrs_used := true;
......@@ -1188,7 +1139,7 @@ let translate_block stmts blocks ret_ty =
(blocks, locate (Goto(id_body)))
in
(* Translate the condition. *)
let (s, blocks) = translate_bool_expr goto_body goto_cont blocks e in
let s = translate_bool_expr goto_body goto_cont e in
let blocks =
let annots =
attrs_used := true;
......
frontend/coq_ast.ml
View file @ 7158d4dd
......@@ -32,6 +32,7 @@ type un_op =
type bin_op =
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | CommaOp
| LazyAndOp | LazyOrOp
type value =
| Null
......@@ -69,8 +70,8 @@ and stmt_aux =
| Switch of int_type * expr * (string * int) list * stmt list * stmt
| Assign of bool (* Atomic? *) * op_type * expr * expr * stmt
| SkipS of stmt
| If of expr * stmt * stmt
| Assert of expr * stmt
| If of op_type * expr * stmt * stmt
| Assert of op_type * expr * stmt
| ExprS of expr_annot option * expr * stmt
(* The integers are respecively the alignment and the size. *)
......
frontend/coq_pp.ml
View file @ 7158d4dd
......@@ -110,23 +110,25 @@ let pp_un_op : Coq_ast.un_op pp = fun ff op ->
let pp_bin_op : Coq_ast.bin_op pp = fun ff op ->
pp_str ff @@
match op with
| AddOp -> "+"
| SubOp -> "-"
| MulOp -> "×"
| DivOp -> "/"
| ModOp -> "%"
| AndOp -> "&"
| OrOp -> "|"
| XorOp -> "^"
| ShlOp -> "<<"
| ShrOp -> ">>"
| EqOp -> "="
| NeOp -> "!="
| LtOp -> "<"
| GtOp -> ">"
| LeOp -> "≤"
| GeOp -> "≥"
| CommaOp -> ","
| AddOp -> "+"
| SubOp -> "-"
| MulOp -> "×"
| DivOp -> "/"
| ModOp -> "%"
| AndOp -> "&"
| OrOp -> "|"
| XorOp -> "^"
| ShlOp -> "<<"
| ShrOp -> ">>"
| EqOp -> "="
| NeOp -> "!="
| LtOp -> "<"
| GtOp -> ">"
| LeOp -> "≤"
| GeOp -> "≥"
| CommaOp -> ","
| LazyAndOp -> "&&"
| LazyOrOp -> "||"
let rec pp_expr : Coq_ast.expr pp = fun ff e ->
let pp fmt = Format.fprintf ff fmt in
......@@ -278,11 +280,11 @@ let rec pp_stmt : Coq_ast.stmt pp = fun ff stmt ->
pp_expr e1 pp_op_type ot order pp_expr e2 pp_stmt stmt
| SkipS(stmt) ->
pp_stmt ff stmt
| If(e,stmt1,stmt2) ->
pp "if: @[<hov 0>%a@]@;then@;@[<v 2>%a@]@;else@;@[<v 2>%a@]"
pp_expr e pp_stmt stmt1 pp_stmt stmt2
| Assert(e, stmt) ->
pp "assert: (%a) ;@;%a" pp_expr e pp_stmt stmt
| If(ot,e,stmt1,stmt2) ->
pp "if{%a}: @[<hov 0>%a@]@;then@;@[<v 2>%a@]@;else@;@[<v 2>%a@]"
pp_op_type ot pp_expr e pp_stmt stmt1 pp_stmt stmt2
| Assert(ot,e,stmt) ->
pp "assert{%a}: (%a) ;@;%a" pp_op_type ot pp_expr e pp_stmt stmt
| ExprS(annot, e, stmt) ->
Option.iter (Option.iter (pp "annot: (%s) ;@;")) annot;
pp "expr: (%a) ;@;%a" pp_expr e pp_stmt stmt
......
theories/lang/lang.v
View file @ 7158d4dd
......@@ -72,6 +72,7 @@ hardware threads). *)
Inductive stmt :=
| Goto (b : label)
| Return (e : expr)
| IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
(* m: map from values of e to indices into bs, def: default *)
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
......@@ -129,6 +130,7 @@ with rtexpr :=
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
| RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt)
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt)
| RTSkipS (s : stmt)
......@@ -158,6 +160,7 @@ Definition to_rtstmt (rf : runtime_function) (s : stmt) : runtime_expr :=
Stmt rf $ match s with
| Goto b => RTGoto b
| Return e => RTReturn (to_rtexpr e)
| IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2
| Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
| Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s
| SkipS s => RTSkipS s
......@@ -208,6 +211,7 @@ Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
match s with
| Goto b => Goto b
| Return e => Return (subst_l xs e)
| IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
| Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
| Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
| SkipS s => SkipS (subst_stmt xs s)
......@@ -507,6 +511,9 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
v2 `has_layout_val` (ot_layout ot) →
heap_at l (ot_layout ot) v' start_st σ.(st_heap).(hs_heap) →
stmt_step (Assign o ot (Val v1) (Val v2) s) rf σ [] (to_rtstmt rf end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
| IfSS it v s1 s2 rf σ n:
val_to_Z v it = Some n →
stmt_step (IfS (IntOp it) (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (n ≠ 0) then s1 else s2))) σ []
| SwitchS rf σ v n m bs s def it :
val_to_Z v it = Some n →
(∀ i : nat, m !! n = Some i → is_Some (bs !! i)) →
......@@ -615,6 +622,7 @@ Inductive stmt_ectx :=
| AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt)
| ReturnCtx
| IfSCtx (ot : op_type) (s1 s2 : stmt)
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
.
......@@ -624,6 +632,7 @@ Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
| AssignRCtx o ot e1 s => RTAssign o ot e1 e s
| AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s
| ReturnCtx => RTReturn e
| IfSCtx ot s1 s2 => RTIfS ot e s1 s2
| SwitchCtx it m bs def => RTSwitch it e m bs def
| ExprSCtx s => RTExprS e s
end.
......
theories/lang/lifting.v
View file @ 7158d4dd
......@@ -618,15 +618,14 @@ Proof. by iApply @wp_value. Qed.
Lemma wp_if Φ it v e1 e2 n:
val_to_Z v it = Some n →
(if decide (n = 0) then WP e2 {{ Φ }} else WP e1 {{ Φ }}) -∗
(if bool_decide (n ≠ 0) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -∗
WP IfE (IntOp it) (Val v) e1 e2 {{ Φ }}.
Proof.
iIntros (?) "HΦ".
iApply wp_lift_expr_step; auto.
iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using IfES.
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame.
by case_decide; case_bool_decide.
iSplit => //. iFrame. by case_bool_decide.
Qed.
Lemma wp_skip Φ v E:
......@@ -944,20 +943,22 @@ Proof.
- iDestruct "Hs" as "[_ Hs]". by iApply "Hs".
Qed.
Lemma wps_if Q Ψ v s1 s2 n:
val_to_Z v bool_it = Some n →
(if decide (n = 0) then WPs s2 {{ Q, Ψ }} else WPs s1 {{ Q, Ψ }}) -∗
WPs (if: (Val v) then s1 else s2) {{ Q , Ψ }}.
Lemma wps_if Q Ψ it v s1 s2 n:
val_to_Z v it = Some n →
(if bool_decide (n ≠ 0) then WPs s1 {{ Q, Ψ }} else WPs s2 {{ Q, Ψ }}) -∗
WPs (if{IntOp it}: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
iIntros (Hn) "Hs". iApply wps_switch' => //=.
1: by apply map_Forall_insert_2; eauto; apply map_Forall_empty.
rewrite right_id. by iSplit; iIntros (?); simplify_map_eq.
iIntros (Hn) "Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
iApply wp_lift_stmt_step. iIntros (?) "Hσ".
iModIntro. iSplit; first by eauto 8 using IfSS.
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ". case_bool_decide; by iApply "Hs".
Qed.
Lemma wps_assert Q Ψ v s n:
val_to_Z v bool_it = Some n → n ≠ 0 →
Lemma wps_assert Q Ψ it v s n:
val_to_Z v it = Some n → n ≠ 0 →
WPs s {{ Q, Ψ }} -∗
WPs (assert: Val v; s) {{ Q , Ψ }}.
WPs (assert{IntOp it}: Val v; s) {{ Q , Ψ }}.
Proof.
iIntros (Hv Hn) "Hs". rewrite /notation.Assert.
iApply wps_if => //. by case_decide.
......
theories/lang/notation.v
View file @ 7158d4dd
......@@ -60,14 +60,28 @@ Notation "e1 <-{ ot , o } e2 ; s" := (Assign o ot e1%E e2%E s%E)
(at level 80, s at level 200, format "'[v' e1 '<-{' ot ',' o '}' e2 ';' '/' s ']'") : expr_scope.
Notation "e1 <-{ ot } e2 ; s" := (Assign Na1Ord ot e1%E e2%E s%E)
(at level 80, s at level 200, format "'[v' e1 '<-{' ot '}' e2 ';' '/' s ']'") : expr_scope.
Notation "'if:' e1 'then' s1 'else' s2" := (Switch bool_it e1%E {[ 0 := 0%nat ]} [s2%E] s1%E)
(at level 102, e1, s1, s2 at level 150, format "'[v' 'if:' e1 'then' '/ ' s1 '/' 'else' '/ ' s2 ']'") : expr_scope.
Notation "'if{' ot '}' ':' e1 'then' s1 'else' s2" := (IfS ot e1%E s1%E s2%E)
(at level 102, e1, s1, s2 at level 150, format "'[v' 'if{' ot '}' ':' e1 'then' '/ ' s1 '/' 'else' '/ ' s2 ']'") : expr_scope.
Notation "'expr:' e ; s" := (ExprS e%E s%E)
(at level 80, s at level 200, format "'[v' 'expr:' e ';' '/' s ']'") : expr_scope.
Definition Assert (e : expr) (s : stmt) : stmt := (if: e then s else StuckS)%E.
Notation "'assert:' e ; s" := (Assert e%E s%E)
(at level 80, s at level 200, format "'[v' 'assert:' e ';' '/' s ']'") : expr_scope.
Definition LogicalAnd (ot1 ot2 : op_type) (e1 e2 : expr) : expr :=
(IfE ot1 e1 (IfE ot2 e2 (i2v 1 i32) (i2v 0 i32)) (i2v 0 i32)).
Notation "e1 &&{ ot1 , ot2 } e2" := (LogicalAnd ot1 ot2 e1 e2)
(at level 70, format "e1 &&{ ot1 , ot2 } e2") : expr_scope.
Arguments LogicalAnd : simpl never.
Typeclasses Opaque LogicalAnd.
Definition LogicalOr (ot1 ot2 : op_type) (e1 e2 : expr) : expr :=
(IfE ot1 e1 (i2v 1 i32) (IfE ot2 e2 (i2v 1 i32) (i2v 0 i32))).
Notation "e1 ||{ ot1 , ot2 } e2" := (LogicalOr ot1 ot2 e1 e2)
(at level 70, format "e1 ||{ ot1 , ot2 } e2") : expr_scope.
Arguments LogicalOr : simpl never.
Typeclasses Opaque LogicalOr.
Definition Assert (ot : op_type) (e : expr) (s : stmt) : stmt := (if{ ot }: e then s else StuckS)%E.
Notation "'assert{' ot '}' ':' e ; s" := (Assert ot e%E s%E)
(at level 80, s at level 200, format "'[v' 'assert{' ot '}' ':' e ';' '/' s ']'") : expr_scope.
Arguments Assert : simpl never.
Typeclasses Opaque Assert.
......@@ -181,10 +195,6 @@ Example test1 (l : loc) ly ot :
(ExprS (Call l [ Val (val_of_loc l); Val (val_of_loc l)]) ((Assign ScOrd ly l l) (Goto "a"))).
Proof. simpl. reflexivity. Abort.
Example test_if (l : loc) :
(if: l then Goto "a" else Goto "b")%E = (Switch bool_it l {[ 0 := 0%nat ]} [Goto "b"] (Goto "a")).
Proof. reflexivity. Abort.
Example test_get_member (l : loc) (s : struct_layout) ot :
(!{ot} (!{ot, ScOrd} l) at{s} "a")%E = GetMember (Deref Na1Ord ot (Deref ScOrd ot l%E)) s "a".
Proof. simpl. reflexivity. Abort.
theories/lang/tactics.v
View file @ 7158d4dd
<
......@@ -21,6 +21,8 @@ Inductive expr :=
| SkipE (e : expr)
| StuckE
(* new constructors *)
| LogicalAnd (ot1 ot2 : op_type) (e1 e2 : expr)
| LogicalOr (ot1 ot2 : op_type) (e1 e2 : expr)
| Use (o : order) (ot : op_type) (e : expr)
| AddrOf (e : expr)
| LValue (e : expr)
......@@ -51,6 +53,8 @@ Lemma expr_ind (P : expr → Prop) :
(∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) →
(∀ (e : expr), P e → P (SkipE e)) →
(P StuckE) →
(∀ (ot1 ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalAnd ot1 ot2 e1 e2)) →
(∀ (ot1 ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalOr ot1 ot2 e1 e2)) →
(∀ (o : order) (ot : op_type) (e : expr), P e → P (Use o ot e)) →
(∀ (e : expr), P e → P (AddrOf e)) →
(∀ (e : expr), P e → P (LValue e)) →
......@@ -65,17 +69,17 @@ Lemma expr_ind (P : expr → Prop) :
(∀ (e : lang.expr), P (Expr e)) → ∀ (e : expr), P e.
Proof.
move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ???????????? Hstruct Hmacro ?.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro ?.
9: {
apply Hcall; [ |apply Forall_true => ?]; by apply: FIX.
}
9: {
apply Hconcat. apply Forall_true => ?. by apply: FIX.
}
21: {
23: {
apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
}
21: {
23: {
apply Hmacro. apply Forall_true => ?. by apply: FIX.
}
all: auto.
......@@ -96,6 +100,8 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| IfE ot e1 e2 e3 => lang.IfE ot (to_expr e1) (to_expr e2) (to_expr e3)
| SkipE e => lang.SkipE (to_expr e)
| StuckE => lang.StuckE
| LogicalAnd ot1 ot2 e1 e2 => notation.LogicalAnd ot1 ot2 (to_expr e1) (to_expr e2)
| LogicalOr ot1 ot2 e1 e2 => notation.LogicalOr ot1 ot2 (to_expr e1) (to_expr e2)
| Use o ot e => notation.Use o ot (to_expr e)
| AddrOf e => notation.AddrOf (to_expr e)
| LValue e => notation.LValue (to_expr e)
......@@ -137,6 +143,14 @@ Ltac of_expr e :=
let e := of_expr e in constr:(GetMemberUnion e ul m)
| notation.OffsetOf ?s ?m => constr:(OffsetOf s m)
| notation.OffsetOfUnion ?ul ?m => constr:(OffsetOfUnion ul m)
| notation.LogicalAnd ?ot1 ?ot2 ?e1 ?e2 =>
let e1 := of_expr e1 in
let e2 := of_expr e2 in
constr:(LogicalAnd ot1 ot2 e1 e2)
| notation.LogicalOr ?ot1 ?ot2 ?e1 ?e2 =>
let e1 := of_expr e1 in
let e2 := of_expr e2 in
constr:(LogicalOr ot1 ot2 e1 e2)
| notation.Use ?o ?ot ?e =>
let e := of_expr e in constr:(Use o ot e)
| lang.Val ?x => constr:(Val x)
......@@ -265,7 +279,7 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
if find_expr_fill f bind_val is Some (Ks, e') then
Some (Ks ++ [CallLCtx args], e') else
(* TODO: handle arguments? *) None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ => None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ | LogicalOr _ _ _ _ => None
| IfE ot e1 e2 e3 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e)
......@@ -353,14 +367,14 @@ Local Unset Elimination Schemes.
Inductive stmt :=
| Goto (b : label)
| Return (e : expr)
| IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
| SkipS (s : stmt)
| StuckS
| ExprS (e : expr) (s : stmt)
| If (e : expr) (s1 s2 : stmt)
| Assert (e : expr) (s : stmt)
| Assert (ot : op_type) (e : expr) (s : stmt)
| AnnotStmt (n : nat) {A} (a : A) (s : stmt)
| LocInfoS (a : location_info) (s : stmt)
(* for opaque statements *)
......@@ -370,19 +384,19 @@ End stmt.
Lemma stmt_ind (P : stmt → Prop):
(∀ b : label, P (Goto b)) →
(∀ e : expr, P (Return e)) →
(∀ (ot : op_type) (e : expr) (s1 : stmt), P s1 → ∀ s2 : stmt, P s2 → P (IfS ot e s1 s2)) →
(∀ (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt), P def → Forall P bs → P (Switch it e m bs def)) →
(∀ (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt), P s → P (Assign o ot e1 e2 s)) →
(∀ s : stmt, P s → P (SkipS s)) →
(P StuckS) →
(∀ (e : expr) (s : stmt), P s → P (ExprS e s)) →
(∀ (e : expr) (s1 : stmt), P s1 → ∀ s2 : stmt, P s2 → P (If e s1 s2)) →
(∀ (e : expr) (s : stmt), P s → P (Assert e s)) →
(∀ (ot : op_type) (e : expr) (s : stmt), P s → P (Assert ot e s)) →
(∀ (n : nat) (A : Type) (a : A) (s : stmt), P s → P (AnnotStmt n a s)) →
(∀ (a : location_info) (s : stmt), P s → P (LocInfoS a s)) →
(∀ s : lang.stmt, P (Stmt s)) → ∀ s : stmt, P s.
Proof.
move => *. generalize dependent P => P. match goal with | s : stmt |- _ => revert s end.
fix FIX 1. move => [ ^s] ?? Hswitch *. 3: {
fix FIX 1. move => [ ^s] ??? Hswitch *. 4: {
apply Hswitch; first by apply: FIX. elim: sbs; auto.
}
all: auto.
......@@ -393,13 +407,13 @@ Fixpoint to_stmt (s : stmt) : lang.stmt :=
match s with
| Goto b => lang.Goto b
| Return e => lang.Return (to_expr e)
| IfS ot e s1 s2 => (if{ot}: to_expr e then to_stmt s1 else to_stmt s2)%E
| Switch it e m bs def => lang.Switch it (to_expr e) m (to_stmt <$> bs) (to_stmt def)
| Assign o ot e1 e2 s => lang.Assign o ot (to_expr e1) (to_expr e2) (to_stmt s)
| SkipS s => lang.SkipS (to_stmt s)
| StuckS => lang.StuckS
| ExprS e s => lang.ExprS (to_expr e) (to_stmt s)
| If e s1 s2 => (if: to_expr e then to_stmt s1 else to_stmt s2)%E
| Assert e s => (assert: to_expr e; to_stmt s)%E
| Assert ot e s => (assert{ot}: to_expr e; to_stmt s)%E
| AnnotStmt n a s => notation.AnnotStmt n a (to_stmt s)
| LocInfoS a s => notation.LocInfo a (to_stmt s)
| Stmt s => s
......@@ -419,15 +433,15 @@ Ltac of_stmt s :=
| notation.LocInfo ?a ?s =>
let s := of_stmt s in
constr:(LocInfoS a s)
| (assert: ?e ; ?s)%E =>
| (assert{?ot}: ?e ; ?s)%E =>
let e := of_expr e in
let s := of_stmt s in
constr:(Assert e s)
| (if: ?e then ?s1 else ?s2)%E =>
constr:(Assert ot e s)
| (if{?ot}: ?e then ?s1 else ?s2)%E =>
let e := of_expr e in
let s1 := of_stmt s1 in
let s2 := of_stmt s2 in
constr:(If e s1 s2)
constr:(IfS ot e s1 s2)
| lang.Goto ?b => constr:(Goto b)
| lang.Return ?e =>
let e := of_expr e in constr:(Return e)
......@@ -456,10 +470,10 @@ Inductive stmt_ectx :=
| AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt)
| ReturnCtx
| IfSCtx (ot : op_type) (s1 s2 : stmt)
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
| IfCtx (s1 s2 : stmt)
| AssertCtx (s : stmt)
| AssertCtx (ot : op_type) (s : stmt)
.
Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=
......@@ -468,9 +482,9 @@ Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=