Commit 2933e60f authored by Michael Sammler's avatar Michael Sammler
Browse files

Added ternary operator

parent 86a526cc
Pipeline #41040 passed with stage
in 13 minutes and 58 seconds
......@@ -6,77 +6,101 @@ Set Default Proof Using "Type".
(* Generated from [examples/tests.c]. *)
Section code.
Definition file_0 : string := "examples/tests.c".
Definition loc_2 : location_info := LocationInfo file_0 5 2 5 19.
Definition loc_3 : location_info := LocationInfo file_0 6 2 6 13.
Definition loc_4 : location_info := LocationInfo file_0 7 2 7 12.
Definition loc_5 : location_info := LocationInfo file_0 8 2 8 14.
Definition loc_6 : location_info := LocationInfo file_0 9 2 9 13.
Definition loc_7 : location_info := LocationInfo file_0 11 2 11 21.
Definition loc_8 : location_info := LocationInfo file_0 12 2 12 21.
Definition loc_9 : location_info := LocationInfo file_0 13 2 13 21.
Definition loc_10 : location_info := LocationInfo file_0 14 2 14 21.
Definition loc_11 : location_info := LocationInfo file_0 15 2 15 21.
Definition loc_12 : location_info := LocationInfo file_0 17 2 17 17.
Definition loc_13 : location_info := LocationInfo file_0 18 2 18 16.
Definition loc_14 : location_info := LocationInfo file_0 19 2 19 16.
Definition loc_15 : location_info := LocationInfo file_0 20 2 20 16.
Definition loc_16 : location_info := LocationInfo file_0 21 2 21 16.
Definition loc_17 : location_info := LocationInfo file_0 23 2 23 9.
Definition loc_19 : location_info := LocationInfo file_0 21 9 21 16.
Definition loc_22 : location_info := LocationInfo file_0 21 5 21 7.
Definition loc_24 : location_info := LocationInfo file_0 21 6 21 7.
Definition loc_25 : location_info := LocationInfo file_0 21 6 21 7.
Definition loc_26 : location_info := LocationInfo file_0 20 9 20 16.
Definition loc_29 : location_info := LocationInfo file_0 20 5 20 7.
Definition loc_31 : location_info := LocationInfo file_0 20 6 20 7.
Definition loc_32 : location_info := LocationInfo file_0 20 6 20 7.
Definition loc_33 : location_info := LocationInfo file_0 19 9 19 16.
Definition loc_36 : location_info := LocationInfo file_0 19 5 19 7.
Definition loc_38 : location_info := LocationInfo file_0 19 6 19 7.
Definition loc_39 : location_info := LocationInfo file_0 19 6 19 7.
Definition loc_40 : location_info := LocationInfo file_0 18 9 18 16.
Definition loc_43 : location_info := LocationInfo file_0 18 5 18 7.
Definition loc_45 : location_info := LocationInfo file_0 18 6 18 7.
Definition loc_46 : location_info := LocationInfo file_0 18 6 18 7.
Definition loc_47 : location_info := LocationInfo file_0 17 10 17 17.
Definition loc_50 : location_info := LocationInfo file_0 17 5 17 8.
Definition loc_52 : location_info := LocationInfo file_0 17 6 17 8.
Definition loc_53 : location_info := LocationInfo file_0 17 6 17 8.
Definition loc_54 : location_info := LocationInfo file_0 15 14 15 21.
Definition loc_57 : location_info := LocationInfo file_0 15 5 15 12.
Definition loc_58 : location_info := LocationInfo file_0 15 5 15 7.
Definition loc_59 : location_info := LocationInfo file_0 15 5 15 7.
Definition loc_60 : location_info := LocationInfo file_0 15 11 15 12.
Definition loc_61 : location_info := LocationInfo file_0 15 11 15 12.
Definition loc_62 : location_info := LocationInfo file_0 14 14 14 21.
Definition loc_65 : location_info := LocationInfo file_0 14 5 14 12.
Definition loc_66 : location_info := LocationInfo file_0 14 5 14 7.
Definition loc_67 : location_info := LocationInfo file_0 14 5 14 7.
Definition loc_68 : location_info := LocationInfo file_0 14 11 14 12.
Definition loc_69 : location_info := LocationInfo file_0 14 11 14 12.
Definition loc_70 : location_info := LocationInfo file_0 13 14 13 21.
Definition loc_73 : location_info := LocationInfo file_0 13 5 13 12.
Definition loc_74 : location_info := LocationInfo file_0 13 5 13 7.
Definition loc_75 : location_info := LocationInfo file_0 13 5 13 7.
Definition loc_76 : location_info := LocationInfo file_0 13 11 13 12.
Definition loc_77 : location_info := LocationInfo file_0 13 11 13 12.
Definition loc_78 : location_info := LocationInfo file_0 12 14 12 21.
Definition loc_81 : location_info := LocationInfo file_0 12 5 12 12.
Definition loc_82 : location_info := LocationInfo file_0 12 5 12 7.
Definition loc_83 : location_info := LocationInfo file_0 12 5 12 7.
Definition loc_84 : location_info := LocationInfo file_0 12 11 12 12.
Definition loc_85 : location_info := LocationInfo file_0 12 11 12 12.
Definition loc_86 : location_info := LocationInfo file_0 11 14 11 21.
Definition loc_89 : location_info := LocationInfo file_0 11 5 11 12.
Definition loc_90 : location_info := LocationInfo file_0 11 5 11 7.
Definition loc_91 : location_info := LocationInfo file_0 11 5 11 7.
Definition loc_92 : location_info := LocationInfo file_0 11 11 11 12.
Definition loc_93 : location_info := LocationInfo file_0 11 11 11 12.
Definition loc_94 : location_info := LocationInfo file_0 9 11 9 12.
Definition loc_97 : location_info := LocationInfo file_0 8 12 8 13.
Definition loc_100 : location_info := LocationInfo file_0 7 10 7 11.
Definition loc_103 : location_info := LocationInfo file_0 6 11 6 12.
Definition loc_106 : location_info := LocationInfo file_0 5 17 5 18.
Definition loc_2 : location_info := LocationInfo file_0 7 2 7 19.
Definition loc_3 : location_info := LocationInfo file_0 8 2 8 13.
Definition loc_4 : location_info := LocationInfo file_0 9 2 9 12.
Definition loc_5 : location_info := LocationInfo file_0 10 2 10 14.
Definition loc_6 : location_info := LocationInfo file_0 11 2 11 13.
Definition loc_7 : location_info := LocationInfo file_0 13 2 13 21.
Definition loc_8 : location_info := LocationInfo file_0 14 2 14 21.
Definition loc_9 : location_info := LocationInfo file_0 15 2 15 21.
Definition loc_10 : location_info := LocationInfo file_0 16 2 16 21.
Definition loc_11 : location_info := LocationInfo file_0 17 2 17 21.
Definition loc_12 : location_info := LocationInfo file_0 19 2 19 17.
Definition loc_13 : location_info := LocationInfo file_0 20 2 20 16.
Definition loc_14 : location_info := LocationInfo file_0 21 2 21 16.
Definition loc_15 : location_info := LocationInfo file_0 22 2 22 16.
Definition loc_16 : location_info := LocationInfo file_0 23 2 23 16.
Definition loc_17 : location_info := LocationInfo file_0 25 2 25 9.
Definition loc_19 : location_info := LocationInfo file_0 23 9 23 16.
Definition loc_22 : location_info := LocationInfo file_0 23 5 23 7.
Definition loc_24 : location_info := LocationInfo file_0 23 6 23 7.
Definition loc_25 : location_info := LocationInfo file_0 23 6 23 7.
Definition loc_26 : location_info := LocationInfo file_0 22 9 22 16.
Definition loc_29 : location_info := LocationInfo file_0 22 5 22 7.
Definition loc_31 : location_info := LocationInfo file_0 22 6 22 7.
Definition loc_32 : location_info := LocationInfo file_0 22 6 22 7.
Definition loc_33 : location_info := LocationInfo file_0 21 9 21 16.
Definition loc_36 : location_info := LocationInfo file_0 21 5 21 7.
Definition loc_38 : location_info := LocationInfo file_0 21 6 21 7.
Definition loc_39 : location_info := LocationInfo file_0 21 6 21 7.
Definition loc_40 : location_info := LocationInfo file_0 20 9 20 16.
Definition loc_43 : location_info := LocationInfo file_0 20 5 20 7.
Definition loc_45 : location_info := LocationInfo file_0 20 6 20 7.
Definition loc_46 : location_info := LocationInfo file_0 20 6 20 7.
Definition loc_47 : location_info := LocationInfo file_0 19 10 19 17.
Definition loc_50 : location_info := LocationInfo file_0 19 5 19 8.
Definition loc_52 : location_info := LocationInfo file_0 19 6 19 8.
Definition loc_53 : location_info := LocationInfo file_0 19 6 19 8.
Definition loc_54 : location_info := LocationInfo file_0 17 14 17 21.
Definition loc_57 : location_info := LocationInfo file_0 17 5 17 12.
Definition loc_58 : location_info := LocationInfo file_0 17 5 17 7.
Definition loc_59 : location_info := LocationInfo file_0 17 5 17 7.
Definition loc_60 : location_info := LocationInfo file_0 17 11 17 12.
Definition loc_61 : location_info := LocationInfo file_0 17 11 17 12.
Definition loc_62 : location_info := LocationInfo file_0 16 14 16 21.
Definition loc_65 : location_info := LocationInfo file_0 16 5 16 12.
Definition loc_66 : location_info := LocationInfo file_0 16 5 16 7.
Definition loc_67 : location_info := LocationInfo file_0 16 5 16 7.
Definition loc_68 : location_info := LocationInfo file_0 16 11 16 12.
Definition loc_69 : location_info := LocationInfo file_0 16 11 16 12.
Definition loc_70 : location_info := LocationInfo file_0 15 14 15 21.
Definition loc_73 : location_info := LocationInfo file_0 15 5 15 12.
Definition loc_74 : location_info := LocationInfo file_0 15 5 15 7.
Definition loc_75 : location_info := LocationInfo file_0 15 5 15 7.
Definition loc_76 : location_info := LocationInfo file_0 15 11 15 12.
Definition loc_77 : location_info := LocationInfo file_0 15 11 15 12.
Definition loc_78 : location_info := LocationInfo file_0 14 14 14 21.
Definition loc_81 : location_info := LocationInfo file_0 14 5 14 12.
Definition loc_82 : location_info := LocationInfo file_0 14 5 14 7.
Definition loc_83 : location_info := LocationInfo file_0 14 5 14 7.
Definition loc_84 : location_info := LocationInfo file_0 14 11 14 12.
Definition loc_85 : location_info := LocationInfo file_0 14 11 14 12.
Definition loc_86 : location_info := LocationInfo file_0 13 14 13 21.
Definition loc_89 : location_info := LocationInfo file_0 13 5 13 12.
Definition loc_90 : location_info := LocationInfo file_0 13 5 13 7.
Definition loc_91 : location_info := LocationInfo file_0 13 5 13 7.
Definition loc_92 : location_info := LocationInfo file_0 13 11 13 12.
Definition loc_93 : location_info := LocationInfo file_0 13 11 13 12.
Definition loc_94 : location_info := LocationInfo file_0 11 11 11 12.
Definition loc_97 : location_info := LocationInfo file_0 10 12 10 13.
Definition loc_100 : location_info := LocationInfo file_0 9 10 9 11.
Definition loc_103 : location_info := LocationInfo file_0 8 11 8 12.
Definition loc_106 : location_info := LocationInfo file_0 7 17 7 18.
Definition loc_111 : location_info := LocationInfo file_0 30 2 30 16.
Definition loc_112 : location_info := LocationInfo file_0 31 2 31 27.
Definition loc_113 : location_info := LocationInfo file_0 32 2 32 64.
Definition loc_114 : location_info := LocationInfo file_0 32 9 32 62.
Definition loc_115 : location_info := LocationInfo file_0 32 9 32 57.
Definition loc_116 : location_info := LocationInfo file_0 32 10 32 34.
Definition loc_117 : location_info := LocationInfo file_0 32 10 32 16.
Definition loc_118 : location_info := LocationInfo file_0 32 11 32 16.
Definition loc_119 : location_info := LocationInfo file_0 32 20 32 34.
Definition loc_120 : location_info := LocationInfo file_0 32 37 32 52.
Definition loc_121 : location_info := LocationInfo file_0 32 37 32 48.
Definition loc_122 : location_info := LocationInfo file_0 32 38 32 39.
Definition loc_123 : location_info := LocationInfo file_0 32 42 32 43.
Definition loc_124 : location_info := LocationInfo file_0 32 46 32 47.
Definition loc_125 : location_info := LocationInfo file_0 32 51 32 52.
Definition loc_126 : location_info := LocationInfo file_0 32 55 32 56.
Definition loc_127 : location_info := LocationInfo file_0 32 61 32 62.
Definition loc_128 : location_info := LocationInfo file_0 31 9 31 25.
Definition loc_129 : location_info := LocationInfo file_0 31 9 31 20.
Definition loc_130 : location_info := LocationInfo file_0 31 10 31 11.
Definition loc_131 : location_info := LocationInfo file_0 31 14 31 15.
Definition loc_132 : location_info := LocationInfo file_0 31 18 31 19.
Definition loc_133 : location_info := LocationInfo file_0 31 24 31 25.
Definition loc_134 : location_info := LocationInfo file_0 30 14 30 15.
(* Definition of function [test1]. *)
Definition impl_test1 : function := {|
......@@ -286,4 +310,36 @@ Section code.
]> $
)%E
|}.
(* Definition of function [test_ternary]. *)
Definition impl_test_ternary : function := {|
f_args := [
];
f_local_vars := [
("local", it_layout i32)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"local" <-{ it_layout i32 } LocInfoE loc_134 (i2v 0 i32) ;
locinfo: loc_112 ;
assert: (LocInfoE loc_128 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_128 ((LocInfoE loc_129 (IfE
(IntOp i32)
(LocInfoE loc_130 (i2v 2 i32))
(LocInfoE loc_131 (i2v 3 i32))
(LocInfoE loc_132 (i2v 2 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_133 (i2v 3 i32)))))) ;
locinfo: loc_113 ;
assert: (LocInfoE loc_114 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_114 ((LocInfoE loc_115 (IfE
(IntOp i32)
(LocInfoE loc_116 ((LocInfoE loc_117 (&(LocInfoE loc_118 ("local")))) !={PtrOp, PtrOp} (LocInfoE loc_119 (NULL))))
(LocInfoE loc_120 ((LocInfoE loc_121 (IfE
(IntOp i32)
(LocInfoE loc_122 (i2v 1 i32))
(LocInfoE loc_123 (i2v 1 i32))
(LocInfoE loc_124 (i2v 0 i32)))) +{IntOp i32, IntOp i32} (LocInfoE loc_125 (i2v 3 i32))))
(LocInfoE loc_126 (i2v 2 i32)))) ={IntOp i32, IntOp i32} (LocInfoE loc_127 (i2v 4 i32)))))) ;
Return (VOID)
]> $
)%E
|}.
End code.
From refinedc.typing Require Import typing.
From refinedc.examples.tests Require Import generated_code.
From refinedc.examples.tests Require Import generated_spec.
Set Default Proof Using "Type".
(* Generated from [examples/tests.c]. *)
Section proof_test_ternary.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [test_ternary]. *)
Lemma type_test_ternary :
typed_function impl_test_ternary type_of_test_ternary.
Proof.
Open Scope printing_sugar.
start_function "test_ternary" ([]) => local_local.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "test_ternary" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "test_ternary".
Qed.
End proof_test_ternary.
......@@ -11,4 +11,8 @@ Section spec.
(* Specifications for function [test1]. *)
Definition type_of_test1 :=
fn( () : (); True) () : (), (void); True.
(* Specifications for function [test_ternary]. *)
Definition type_of_test_ternary :=
fn( () : (); True) () : (), (void); True.
End spec.
generated_proof_test1.v
generated_proof_test_ternary.v
#include <stddef.h>
#include <stdbool.h>
// Random tests.
[[rc::returns("void")]]
......@@ -22,3 +24,10 @@ void test1(){
return;
}
[[rc::returns("void")]]
void test_ternary(){
int local = 0;
assert((2 ? 3 : 2) == 3);
assert((&local != NULL ? (true ? 1 : 0) + 3 : 2) == 4);
}
......@@ -528,7 +528,12 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
let e3 = translate_expr false None e3 in
let e = locate (CopyAID(e3, e2)) in
if lval then locate (LValue(e)) else e
| AilEcond(e1,e2,e3) -> not_impl loc "expr cond"
| AilEcond(e1,e2,e3) ->
let ty = op_type_of_tc (loc_of e1) (tc_of e1) in
let e1 = translate_expr lval None e1 in
let e2 = translate_expr lval None e2 in
let e3 = translate_expr lval None e3 in
locate (IfE(ty, e1, e2, e3))
| AilEcast(q,c_ty,e) ->
begin
match c_ty with
......
......@@ -47,6 +47,7 @@ and expr_aux =
| Deref of bool (* Atomic? *) * layout * expr
| CAS of op_type * expr * expr * expr
| Call of expr * expr list
| IfE of op_type * expr * expr * expr
| SkipE of expr
| Use of bool (* Atomic? *) * layout * expr
| AddrOf of expr
......
......@@ -177,6 +177,9 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
List.iteri fn es
in
pp "Call (%a) [@@{expr} %a ]" pp_expr e pp_args es
| IfE(ty,e1,e2,e3) ->
pp "IfE@ (%a)@ (%a)@ (%a)@ (%a)" pp_op_type ty
pp_expr e1 pp_expr e2 pp_expr e3
| SkipE(e) ->
pp "SkipE (%a)" pp_expr e
| Use(atomic,lay,e) ->
......
......@@ -307,6 +307,7 @@ Inductive expr :=
| CAS (ot : op_type) (e1 e2 e3 : expr)
| Call (f : expr) (args : list expr)
| Concat (es : list expr)
| IfE (ot : op_type) (e1 e2 e3 : expr)
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
......@@ -322,6 +323,7 @@ Lemma expr_ind (P : expr → Prop) :
( (ot : op_type) (e1 e2 e3 : expr), P e1 P e2 P e3 P (CAS ot e1 e2 e3))
( (f : expr) (args : list expr), P f Forall P args P (Call f args))
( (es : list expr), Forall P es P (Concat es))
( (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)
(e : expr), P e.
......@@ -389,6 +391,7 @@ with rtexpr :=
| RTCall (f : runtime_expr) (args : list runtime_expr)
| RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
| RTConcat (es : list runtime_expr)
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
......@@ -412,6 +415,7 @@ Fixpoint to_rtexpr (e : expr) : runtime_expr :=
| Call f args => RTCall (to_rtexpr f) (to_rtexpr <$> args)
| CAS ot e1 e2 e3 => RTCAS ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
| Concat es => RTConcat (to_rtexpr <$> es)
| IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
| SkipE e => RTSkipE (to_rtexpr e)
| StuckE => RTStuckE
end.
......@@ -781,6 +785,7 @@ Fixpoint subst (x : var_name) (v : val) (e : expr) : expr :=
| Call e es => Call (subst x v e) (subst x v <$> es)
| CAS ly e1 e2 e3 => CAS ly (subst x v e1) (subst x v e2) (subst x v e3)
| Concat el => Concat (subst x v <$> el)
| IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
| SkipE e => SkipE (subst x v e)
| StuckE => StuckE
end.
......@@ -1029,6 +1034,9 @@ comparing pointers? (see lambda rust) *)
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
expr_step (CopyAllocId (Val v1) (Val v2)) σ [] (Val (val_of_loc (l2.1, l1.2))) σ []
| IfES v it e1 e2 n σ:
val_to_int v it = Some n
expr_step (IfE (IntOp it) (Val v) e1 e2) σ [] (if bool_decide (n 0) then e1 else e2) σ []
(* no rule for StuckE *)
.
......@@ -1088,6 +1096,7 @@ Inductive expr_ectx :=
| CASMCtx (ot : op_type) (v1 : val) (e3 : runtime_expr)
| CASRCtx (ot : op_type) (v1 v2 : val)
| ConcatCtx (vs : list val) (es : list runtime_expr)
| IfECtx (ot : op_type) (e2 e3 : runtime_expr)
| SkipECtx
.
......@@ -1105,6 +1114,7 @@ Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
| CASMCtx ot v1 e3 => RTCAS ot (Val v1) e e3
| CASRCtx ot v1 v2 => RTCAS ot (Val v1) (Val v2) e
| ConcatCtx vs es => RTConcat ((Expr <$> (RTVal <$> vs)) ++ e :: es)
| IfECtx ot e2 e3 => RTIfE ot e e2 e3
| SkipECtx => RTSkipE e
end.
......
......@@ -443,6 +443,19 @@ Lemma wp_offset_of_union Φ ul m E:
Φ (i2v 0 size_t) - WP OffsetOfUnion ul m @ E {{ Φ }}.
Proof. by iApply @wp_value. Qed.
Lemma wp_if Φ it v e1 e2 n:
val_to_int v it = Some n
(if decide (n = 0) then WP coerce_rtexpr e2 {{ Φ }} else WP coerce_rtexpr e1 {{ Φ }}) -
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.
Qed.
Lemma wp_skip Φ v E:
Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
......
......@@ -17,6 +17,7 @@ Inductive expr :=
| CAS (ot : op_type) (e1 e2 e3 : expr)
| Call (f : expr) (args : list expr)
| Concat (es : list expr)
| IfE (op : op_type) (e1 e2 e3 : expr)
| SkipE (e : expr)
| StuckE
(* new constructors *)
......@@ -47,6 +48,7 @@ Lemma expr_ind (P : expr → Prop) :
( (ot : op_type) (e1 e2 e3 : expr), P e1 P e2 P e3 P (CAS ot e1 e2 e3))
( (f : expr) (args : list expr), P f Forall P args P (Call f args))
( (es : list expr), Forall P es P (Concat es))
( (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)
( (o : order) (ly : layout) (e : expr), P e P (Use o ly e))
......@@ -63,17 +65,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.
}
20: {
21: {
apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
}
20: {
21: {
apply Hmacro. apply Forall_true => ?. by apply: FIX.
}
all: auto.
......@@ -91,6 +93,7 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| CAS ot e1 e2 e3 => lang.CAS ot (to_expr e1) (to_expr e2) (to_expr e3)
| Call f args => lang.Call (to_expr f) (to_expr <$> args)
| Concat es => lang.Concat (to_expr <$> es)
| 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
| Use o ly e => notation.Use o ly (to_expr e)
......@@ -153,6 +156,11 @@ Ltac of_expr e :=
let args := of_expr args in constr:(Call f args)
| lang.Concat ?es =>
let es := of_expr es in constr:(Concat es)
| lang.IfE ?ot ?e1 ?e2 ?e3 =>
let e1 := of_expr e1 in
let e2 := of_expr e2 in
let e3 := of_expr e3 in
constr:(IfE ot e1 e2 e3)
| lang.SkipE ?e =>
let e := of_expr e in constr:(SkipE e)
| lang.StuckE => constr:(StuckE e)
......@@ -180,6 +188,7 @@ Inductive ectx_item :=
| CallLCtx (args : list expr)
| CallRCtx (f : val) (vl : list val) (el : list expr)
| ConcatCtx (vs : list val) (es : list expr)
| IfECtx (ot : op_type) (e2 e3 : expr)
| SkipECtx
(* new constructors *)
| UseCtx (o : order) (ly : layout)
......@@ -207,6 +216,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| CallLCtx args => Call e args
| CallRCtx f vl el => Call (Val f) ((Val <$> vl) ++ e :: el)
| ConcatCtx vs es => Concat ((Val <$> vs) ++ e :: es)
| IfECtx ot e2 e3 => IfE ot e e2 e3
| SkipECtx => SkipE e
| UseCtx o l => Use o l e
| AddrOfCtx => AddrOf e
......@@ -256,6 +266,9 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
Some (Ks ++ [CallLCtx args], e') else
(* TODO: handle arguments? *) None
| Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ => 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)
| SkipE e1 =>
if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [SkipECtx], e') else Some ([], e)
......@@ -305,6 +318,7 @@ Proof.
apply: [lang.CallLCtx _]|
apply: [lang.CallRCtx _ _ _]|
apply: [lang.ConcatCtx _ _]|
apply: [lang.IfECtx _ _ _]|
apply: [lang.SkipECtx]|
apply: [lang.DerefCtx _ _]|
apply: []|
......@@ -314,7 +328,7 @@ Proof.
apply: [lang.BinOpRCtx _ _ _ _]|
apply: []|..
]).
move: K => [||||||||||||||||n|||] * //=.
move: K => [|||||||||||||||||n|||] * //=.
- (** Call *)
do 2 f_equal.
rewrite !fmap_app !fmap_cons. repeat f_equal; eauto.
......@@ -503,6 +517,7 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
| CAS ot e1 e2 e3 => CAS ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
| Call f args => Call (subst_l xs f) (subst_l xs <$> args)
| Concat es => Concat (subst_l xs <$> es)
| IfE ot e1 e2 e3 => IfE ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
| SkipE e => SkipE (subst_l xs e)
| StuckE => StuckE
| Use o ly e => Use o ly (subst_l xs e)
......
......@@ -43,7 +43,7 @@ Ltac convert_to_i2p_tac P ::=
| typed_un_op ?v ?ty ?o ?ot ?T => uconstr:(((_ : TypedUnOp _ _ _ _) _).(i2p_proof))
| typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?T => uconstr:(((_ : TypedCopyAllocId _ _ _ _) _).(i2p_proof))
| typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _).(i2p_proof))
| typed_if ?v ?ty ?s1 ?s2 ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedIf _ _) _ _ _ _ _ _ _).(i2p_proof))
| typed_if ?ot ?v ?ty ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))
| typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _ _).(i2p_proof))
| typed_assert ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _) _ _ _ _ _ _).(i2p_proof))
| typed_read_end ?a ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _) _).(i2p_proof))
......@@ -185,6 +185,7 @@ Ltac liRExpr :=
| W.OffsetOf _ _ => notypeclasses refine (tac_fast_apply (type_offset_of _ _ _) _)
| W.AnnotExpr _ ?a _ => notypeclasses refine (tac_fast_apply (type_annot_expr _ _ _ _) _)
| W.StructInit _ _ => notypeclasses refine (tac_fast_apply (type_struct_init _ _ _) _)
| W.IfE _ _ _ _ => notypeclasses refine (tac_fast_apply (type_ife _ _ _ _ _) _)
| W.SkipE _ => notypeclasses refine (tac_fast_apply (type_skipe' _ _) _)
| W.MacroE _ _ _ => notypeclasses refine (tac_fast_apply (type_macro_expr _ _ _) _)
| _ => fail "do_expr: unknown expr" e
......