lang.v 29.8 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings.
From stdpp Require Import gmap list.
Michael Sammler's avatar
Michael Sammler committed
4
From refinedc.lang Require Export base byte layout int_type loc val heap struct.
Michael Sammler's avatar
Michael Sammler committed
5
6
7
Set Default Proof Using "Type".
Open Scope Z_scope.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
8
9
10
(** * Definition of the language *)

Definition label := string.
Michael Sammler's avatar
Michael Sammler committed
11
12
13
14

(* see http://compcert.inria.fr/doc/html/compcert.cfrontend.Cop.html#binary_operation *)
Inductive bin_op : Set :=
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
15
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | Comma
16
17
18
19
(* Ptr is the second argument and offset the first *)
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout)
| PtrDiffOp (ly : layout).

Michael Sammler's avatar
Michael Sammler committed
20
21
22
23
24
25

Inductive un_op : Set :=
| NotBoolOp | NotIntOp | NegOp | CastOp (ot : op_type).
Inductive order : Set :=
| ScOrd | Na1Ord | Na2Ord.

26
27
Section expr.
Local Unset Elimination Schemes.
Michael Sammler's avatar
Michael Sammler committed
28
29
30
31
32
Inductive expr :=
| Var (x : var_name)
| Val (v : val)
| UnOp (op : un_op) (ot : op_type) (e : expr)
| BinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr)
33
| CopyAllocId (ot1 : op_type) (e1 : expr) (e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
34
| Deref (o : order) (ot : op_type) (e : expr)
Michael Sammler's avatar
Michael Sammler committed
35
| CAS (ot : op_type) (e1 e2 e3 : expr)
36
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
37
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
38
| IfE (ot : op_type) (e1 e2 e3 : expr)
Michael Sammler's avatar
Michael Sammler committed
39
40
41
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
42
43
44
45
46
47
48
End expr.
Arguments Call _%E _%E.
Lemma expr_ind (P : expr  Prop) :
  ( (x : var_name), P (Var x)) 
  ( (v : val), P (Val v)) 
  ( (op : un_op) (ot : op_type) (e : expr), P e  P (UnOp op ot e)) 
  ( (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr), P e1  P e2  P (BinOp op ot1 ot2 e1 e2)) 
49
  ( (ot1 : op_type) (e1 e2 : expr), P e1  P e2  P (CopyAllocId ot1 e1 e2)) 
Michael Sammler's avatar
Michael Sammler committed
50
  ( (o : order) (ot : op_type) (e : expr), P e  P (Deref o ot e)) 
51
52
53
  ( (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)) 
Michael Sammler's avatar
Michael Sammler committed
54
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
55
56
57
58
59
60
61
62
63
64
65
66
67
  ( (e : expr), P e  P (SkipE e)) 
  (P StuckE) 
   (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 *.
  8: { apply Hcall; [ |apply Forall_true => ?]; by apply: FIX. }
  8: { apply Hconcat. apply Forall_true => ?. by apply: FIX. }
  all: auto.
Qed.

Global Instance val_inj : Inj (=) (=) Val.
Proof. by move => ?? [->]. Qed.
Michael Sammler's avatar
Michael Sammler committed
68
69
70
71
72

(** Note that there is no explicit Fork. Instead the initial state can
contain multiple threads (like a processor which has a fixed number of
hardware threads). *)
Inductive stmt :=
73
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
74
| Return (e : expr)
75
| IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
76
77
(* 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)
Michael Sammler's avatar
Michael Sammler committed
78
| Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
79
80
81
82
83
84
85
86
87
88
89
| SkipS (s : stmt)
| StuckS (* stuck statement *)
| ExprS (e : expr) (s : stmt)
.

Arguments Switch _%E _%E _%E.

Record function := {
  f_args : list (var_name * layout);
  f_local_vars : list (var_name * layout);
  (* TODO should we add this: f_ret : layout; ?*)
90
91
  f_code : gmap label stmt;
  f_init : label;
Michael Sammler's avatar
Michael Sammler committed
92
93
}.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
94
(* TODO: put both function and bytes in the same heap or make pointers disjoint *)
Michael Sammler's avatar
Michael Sammler committed
95
Record state := {
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
96
  st_heap: heap_state;
Michael Sammler's avatar
Michael Sammler committed
97
  st_fntbl: gmap addr function;
Michael Sammler's avatar
Michael Sammler committed
98
99
}.

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
100
101
102
103
104
Definition heap_fmap (f : heap  heap) (σ : state) := {|
  st_heap := {| hs_heap := f σ.(st_heap).(hs_heap); hs_allocs := σ.(st_heap).(hs_allocs) |};
  st_fntbl := σ.(st_fntbl);
|}.

Michael Sammler's avatar
Michael Sammler committed
105
106
107
108
109
110
111
112
Record runtime_function := {
  (* locations of args and local vars are substitued in the body *)
  rf_fn : function;
  (* locations in the stack frame (locations of arguments and local
  vars allocated on Call, need to be freed by Return) *)
  rf_locs: list (loc * layout);
}.

113
114
115
116
117
118
119
120
121
Inductive runtime_expr :=
| Expr (e : rtexpr)
| Stmt (rf : runtime_function) (s : rtstmt)
| AllocFailed
with rtexpr :=
| RTVar (x : var_name)
| RTVal (v : val)
| RTUnOp (op : un_op) (ot : op_type) (e : runtime_expr)
| RTBinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : runtime_expr)
122
| RTCopyAllocId (ot1 : op_type) (e1 : runtime_expr) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
123
| RTDeref (o : order) (ot : op_type) (e : runtime_expr)
124
125
126
| RTCall (f : runtime_expr) (args : list runtime_expr)
| RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
| RTConcat (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
127
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
128
129
130
131
132
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
133
| RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt)
134
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
Michael Sammler's avatar
Michael Sammler committed
135
| RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt)
136
137
138
139
| RTSkipS (s : stmt)
| RTStuckS
| RTExprS (e : runtime_expr) (s : stmt)
.
140

141
142
143
144
145
146
Fixpoint to_rtexpr (e : expr) : runtime_expr :=
  Expr $ match e with
  | Var x => RTVar x
  | Val v => RTVal v
  | UnOp op ot e => RTUnOp op ot (to_rtexpr e)
  | BinOp op ot1 ot2 e1 e2 => RTBinOp op ot1 ot2 (to_rtexpr e1) (to_rtexpr e2)
147
  | CopyAllocId ot1 e1 e2 => RTCopyAllocId ot1 (to_rtexpr e1) (to_rtexpr e2)
Michael Sammler's avatar
Michael Sammler committed
148
  | Deref o ot e => RTDeref o ot (to_rtexpr e)
149
150
151
  | 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)
Michael Sammler's avatar
Michael Sammler committed
152
  | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
153
154
155
156
157
158
159
160
161
162
  | SkipE e => RTSkipE (to_rtexpr e)
  | StuckE => RTStuckE
  end.
Definition coerce_rtexpr := to_rtexpr.
Coercion coerce_rtexpr : expr >-> runtime_expr.
Arguments coerce_rtexpr : simpl never.
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)
163
  | IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2
164
  | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
Michael Sammler's avatar
Michael Sammler committed
165
  | Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s
166
167
168
169
  | SkipS s => RTSkipS s
  | StuckS => RTStuckS
  | ExprS e s => RTExprS (to_rtexpr e) s
  end.
170

171
172
173
174
175
176
177
178
179
180
181
182
183
Global Instance to_rtexpr_inj : Inj (=) (=) to_rtexpr.
Proof.
  elim => [ ^ e1 ] [ ^ e2 ] // ?; simplify_eq => //; try naive_solver.
  - f_equal. naive_solver.
    generalize dependent e2args.
    revert select (Forall _ _). elim. by case.
    move => ????? [|??]//. naive_solver.
  - generalize dependent e2es.
    revert select (Forall _ _). elim. by case.
    move => ????? [|??]//. naive_solver.
Qed.
Global Instance to_rtstmt_inj : Inj2 (=) (=) (=) to_rtstmt.
Proof. move => ? s1 ? s2 [-> ]. elim: s1 s2 => [ ^ e1 ] [ ^ e2 ] // ?; simplify_eq => //. Qed.
Michael Sammler's avatar
Michael Sammler committed
184

185
Implicit Type (l : loc) (re : rtexpr) (v : val) (h : heap) (σ : state) (ly : layout) (rs : rtstmt) (s : stmt) (sgn : signed) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
186

187
188
(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
189
  match e with
190
191
192
193
  | Var y => if bool_decide (x = y) then Val v else Var y
  | Val v => Val v
  | UnOp op ot e => UnOp op ot (subst x v e)
  | BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst x v e1) (subst x v e2)
194
  | CopyAllocId ot1 e1 e2 => CopyAllocId ot1 (subst x v e1) (subst x v e2)
195
196
197
198
  | Deref o l e => Deref o l (subst x v e)
  | 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)
Michael Sammler's avatar
Michael Sammler committed
199
  | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
200
201
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
Michael Sammler's avatar
Michael Sammler committed
202
203
  end.

Michael Sammler's avatar
Michael Sammler committed
204
205
206
207
Fixpoint subst_l (xs : list (var_name * val)) (e : expr)  : expr :=
  match xs with
  | (x, v)::xs' => subst_l xs' (subst x v e)
  | _ => e
Michael Sammler's avatar
Michael Sammler committed
208
209
  end.

Michael Sammler's avatar
Michael Sammler committed
210
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
211
212
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
213
  | Return e => Return (subst_l xs e)
214
  | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
Michael Sammler's avatar
Michael Sammler committed
215
  | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
Michael Sammler's avatar
Michael Sammler committed
216
  | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
217
  | SkipS s => SkipS (subst_stmt xs s)
218
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
219
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
220
221
  end.

Michael Sammler's avatar
Michael Sammler committed
222
223
Definition subst_function (xs : list (var_name * val)) (f : function) : function := {|
  f_code := (subst_stmt xs) <$> f.(f_code);
224
225
226
  f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.

Michael Sammler's avatar
Michael Sammler committed
227
228
229
(*** Evaluation of operations *)

(* evaluation can be non-deterministic for comparing pointers *)
230
231
Inductive eval_bin_op : bin_op  op_type  op_type  state  val  val  val  Prop :=
| PtrOffsetOpIP v1 v2 σ o l ly it:
Michael Sammler's avatar
Michael Sammler committed
232
    val_to_Z v1 it = Some o 
Michael Sammler's avatar
Michael Sammler committed
233
234
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
235
    heap_state_loc_in_bounds (l offset{ly} o) 0 σ.(st_heap) 
236
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
237
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
Michael Sammler's avatar
Michael Sammler committed
238
    val_to_Z v1 it = Some o 
239
    val_to_loc v2 = Some l 
240
    heap_state_loc_in_bounds (l offset{ly} -o) 0 σ.(st_heap) 
241
242
    (* TODO: should we have an alignment check here? *)
    eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} -o))
243
244
245
246
| PtrDiffOpPP v1 v2 σ l1 l2 ly v:
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
    l1.1 = l2.1 
247
    0 < ly.(ly_size) 
248
249
    valid_ptr l1 σ.(st_heap) 
    valid_ptr l2 σ.(st_heap) 
250
    val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some v 
251
    eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
252
| RelOpPNull v1 v2 σ l v op b p a:
Michael Sammler's avatar
Michael Sammler committed
253
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
254
    l = (ProvAlloc p, a) 
Michael Sammler's avatar
Michael Sammler committed
255
    v2 = NULL 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
256
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
Michael Sammler's avatar
Michael Sammler committed
257
258
259
260
261
262
263
264
    match op with
    | EqOp => Some false
    | NeOp => Some true
    | _ => None
    end = Some b 
    val_of_Z (Z_of_bool b) i32 None = Some v 
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullP v1 v2 σ l v op b p a:
Michael Sammler's avatar
Michael Sammler committed
265
    v1 = NULL 
Michael Sammler's avatar
Michael Sammler committed
266
267
268
269
270
271
272
273
274
275
276
    val_to_loc v2 = Some l 
    l = (ProvAlloc p, a) 
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
    match op with
    | EqOp => Some false
    | NeOp => Some true
    | _ => None
    end = Some b 
    val_of_Z (Z_of_bool b) i32 None = Some v 
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullNull v1 v2 σ v op b:
Michael Sammler's avatar
Michael Sammler committed
277
278
    v1 = NULL 
    v2 = NULL 
Michael Sammler's avatar
Michael Sammler committed
279
280
281
282
283
284
285
286
    match op with
    | EqOp => Some true
    | NeOp => Some false
    | _ => None
    end = Some b 
    val_of_Z (Z_of_bool b) i32 None = Some v 
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpPP v1 v2 σ l1 l2 p1 p2 a1 a2 v b op:
Michael Sammler's avatar
Michael Sammler committed
287
288
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
Michael Sammler's avatar
Michael Sammler committed
289
290
291
292
    (* Note that this is technically redundant due to the valid_ptr,
    but we still have it for clarity. *)
    l1 = (ProvAlloc p1, a1) 
    l2 = (ProvAlloc p2, a2) 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
293
    valid_ptr l1 σ.(st_heap)  valid_ptr l2 σ.(st_heap) 
294
    match op with
Michael Sammler's avatar
Michael Sammler committed
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
    | EqOp => Some (bool_decide (a1 = a2))
    | NeOp => Some (bool_decide (a1  a2))
    | LtOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 < a2)) else None
    | GtOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 > a2)) else None
    | LeOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 <= a2)) else None
    | GeOp => if bool_decide (p1 = p2) then Some (bool_decide (a1 >= a2)) else None
    | _ => None
    end = Some b 
    val_of_Z (Z_of_bool b) i32 None = Some v 
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpFnPP v1 v2 σ l1 l2 a1 a2 v b op:
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
    l1 = (ProvFnPtr, a1) 
    l2 = (ProvFnPtr, a2) 
    match op with
    | EqOp => Some (bool_decide (a1 = a2))
    | NeOp => Some (bool_decide (a1  a2))
313
314
    | _ => None
    end = Some b 
Michael Sammler's avatar
Michael Sammler committed
315
    val_of_Z (Z_of_bool b) i32 None = Some v 
316
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
317
| RelOpII op v1 v2 v σ n1 n2 it b:
Michael Sammler's avatar
Michael Sammler committed
318
319
320
321
322
323
324
325
326
    match op with
    | EqOp => Some (bool_decide (n1 = n2))
    | NeOp => Some (bool_decide (n1  n2))
    | LtOp => Some (bool_decide (n1 < n2))
    | GtOp => Some (bool_decide (n1 > n2))
    | LeOp => Some (bool_decide (n1 <= n2))
    | GeOp => Some (bool_decide (n1 >= n2))
    | _ => None
    end = Some b 
Michael Sammler's avatar
Michael Sammler committed
327
328
    val_to_Z v1 it = Some n1 
    val_to_Z v2 it = Some n2 
Michael Sammler's avatar
Michael Sammler committed
329
330
    (* TODO: What is the right int type of the result here? C seems to
    use i32 but maybe we don't want to hard code that. *)
Michael Sammler's avatar
Michael Sammler committed
331
332
    val_of_Z (Z_of_bool b) i32 None = Some v 
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
333
| ArithOpII op v1 v2 σ n1 n2 it n v:
Michael Sammler's avatar
Michael Sammler committed
334
335
336
337
338
339
340
    match op with
    | AddOp => Some (n1 + n2)
    | SubOp => Some (n1 - n2)
    | MulOp => Some (n1 * n2)
    (* we need to take `quot` and `rem` here for the correct rounding
    behavior, i.e. rounding towards 0 (instead of `div` and `mod`,
    which round towards floor)*)
Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
341
342
    | DivOp => if bool_decide (n2  0) then Some (n1 `quot` n2) else None
    | ModOp => if bool_decide (n2  0) then Some (n1 `rem` n2) else None
Michael Sammler's avatar
Michael Sammler committed
343
344
345
    | AndOp => Some (Z.land n1 n2)
    | OrOp => Some (Z.lor n1 n2)
    | XorOp => Some (Z.lxor n1 n2)
Fengmin Zhu's avatar
Ci/bits    
Fengmin Zhu committed
346
347
348
349
350
351
352
353
354
    (* For shift operators (`ShlOp` and `ShrOp`), behaviors are defined if:
       - lhs is nonnegative, and
       - rhs (also nonnegative) is less than the number of bits in lhs.
       See: https://en.cppreference.com/w/c/language/operator_arithmetic, "Shift operators". *)
    | ShlOp => if bool_decide (0  n1  0  n2 < bits_per_int it) then Some (n1  n2) else None
    (* NOTE: when lhs is negative, Coq's `≫` is not semantically equivalent to C's `>>`.
       Counterexample: Coq `-1000 ≫ 10 = 0`; C `-1000 >> 10 == -1`.
       This is because `≫` is implemented by `Z.div`. *)
    | ShrOp => if bool_decide (0  n1  0  n2 < bits_per_int it) then Some (n1  n2) else None
Michael Sammler's avatar
Michael Sammler committed
355
356
    | _ => None
    end = Some n 
Michael Sammler's avatar
Michael Sammler committed
357
358
359
    val_to_Z v1 it = Some n1 
    val_to_Z v2 it = Some n2 
    val_of_Z (if it_signed it then n else n `mod` int_modulus it) it None = Some v 
360
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
361
362
| CommaOp ot1 ot2 σ v1 v2:
    eval_bin_op Comma ot1 ot2 σ v1 v2 v2
Michael Sammler's avatar
Michael Sammler committed
363
364
.

365
Inductive eval_un_op : un_op  op_type  state  val  val  Prop :=
366
| CastOpII itt its σ vs vt i:
Michael Sammler's avatar
Michael Sammler committed
367
368
    val_to_Z vs its = Some i 
    val_of_Z i itt (val_to_byte_prov vs) = Some vt 
369
370
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
371
372
    val_to_loc vs = Some l 
    val_of_loc l = vt 
373
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
Michael Sammler's avatar
Michael Sammler committed
374
| CastOpPI it σ vs vt l p:
375
    val_to_loc vs = Some l 
Michael Sammler's avatar
Michael Sammler committed
376
377
    l.1 = ProvAlloc p 
    val_of_Z l.2 it p = Some vt 
378
    block_alive l σ.(st_heap) 
379
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
380
381
382
383
384
385
| CastOpPIFn it σ vs vt l:
    val_to_loc vs = Some l 
    l.1 = ProvFnPtr 
    val_of_Z l.2 it None = Some vt 
    is_Some (σ.(st_fntbl) !! l.2) 
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
386
387
| CastOpPINull it σ vs vt:
    vs = NULL 
Michael Sammler's avatar
Michael Sammler committed
388
    val_of_Z 0 it None = Some vt 
389
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
Michael Sammler's avatar
Michael Sammler committed
390
391
392
| CastOpIP it σ vs vt l l' a:
    val_to_Z vs it = Some a 
    l = (ProvAlloc (val_to_byte_prov vs), a) 
393
    (** This is using that the address 0 is never alive. *)
394
    l' = (if bool_decide (valid_ptr l σ.(st_heap)) then l else
395
396
397
398
399
            (if bool_decide (a = 0) then NULL_loc else
               if bool_decide (is_Some (σ.(st_fntbl) !! l.2)) then
                 (ProvFnPtr, a)
               else
                 (ProvAlloc None, a))) 
Michael Sammler's avatar
Michael Sammler committed
400
    val_of_loc l' = vt 
401
    eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
402
| NegOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
403
404
    val_to_Z vs it = Some n 
    val_of_Z (-n) it None = Some vt 
405
    eval_un_op NegOp (IntOp it) σ vs vt
406
| NotIntOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
407
408
    val_to_Z vs it = Some n 
    val_of_Z (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it None = Some vt 
409
    eval_un_op NotIntOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
410
411
412
413
.

(*** Evaluation of Expressions *)

414
Inductive expr_step : expr  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
Michael Sammler's avatar
Michael Sammler committed
415
416
417
| SkipES v σ:
    expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
418
    eval_un_op op ot σ v v' 
Michael Sammler's avatar
Michael Sammler committed
419
420
    expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
421
    eval_bin_op op ot1 ot2 σ v1 v2 v' 
Michael Sammler's avatar
Michael Sammler committed
422
    expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
Michael Sammler's avatar
Michael Sammler committed
423
| DerefS o v l ot v' σ:
Michael Sammler's avatar
Michael Sammler committed
424
    let start_st st :=  n, st = if o is Na2Ord then RSt (S n) else RSt n in
425
426
427
428
429
430
431
432
    let end_st st :=
      match o, st with
      | Na1Ord, Some (RSt n)     => RSt (S n)
      | Na2Ord, Some (RSt (S n)) => RSt n
      | ScOrd , Some st          => st
      |  _    , _                => WSt (* unreachable *)
      end
    in
Michael Sammler's avatar
Michael Sammler committed
433
    let end_expr := if o is Na1Ord then Deref Na2Ord ot (Val v) else Val (mem_cast v' ot (dom _ σ.(st_fntbl), σ.(st_heap))) in
Michael Sammler's avatar
Michael Sammler committed
434
    val_to_loc v = Some l 
Michael Sammler's avatar
Michael Sammler committed
435
436
    heap_at l (ot_layout ot) v' start_st σ.(st_heap).(hs_heap) 
    expr_step (Deref o ot (Val v)) σ [] end_expr (heap_fmap (heap_upd l v' end_st) σ) []
Michael Sammler's avatar
Michael Sammler committed
437
438
439
440
441
(* TODO: look at CAS and see whether it makes sense. Also allow
comparing pointers? (see lambda rust) *)
(* corresponds to atomic_compare_exchange_strong, see https://en.cppreference.com/w/c/atomic/atomic_compare_exchange *)
| CasFailS l1 l2 vo ve σ z1 z2 v1 v2 v3 it:
    val_to_loc v1 = Some l1 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
442
    heap_at l1 (it_layout it) vo (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
443
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
444
    heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
445
446
    val_to_Z vo it = Some z1 
    val_to_Z ve it = Some z2 
Michael Sammler's avatar
Michael Sammler committed
447
    v3 `has_layout_val` it_layout it 
448
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
449
450
451
452
453
    z1  z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool false)) (heap_fmap (heap_upd l2 vo (λ _, RSt 0%nat)) σ) []
| CasSucS l1 l2 it vo ve σ z1 z2 v1 v2 v3:
    val_to_loc v1 = Some l1 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
454
    heap_at l1 (it_layout it) vo (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
455
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
456
    heap_at l2 (it_layout it) ve (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
457
458
    val_to_Z vo it = Some z1 
    val_to_Z ve it = Some z2 
Michael Sammler's avatar
Michael Sammler committed
459
    v3 `has_layout_val` it_layout it 
460
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
461
462
463
    z1 = z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool true)) (heap_fmap (heap_upd l1 v3 (λ _, RSt 0%nat)) σ) []
Michael Sammler's avatar
Michael Sammler committed
464
| CallS lsa lsv σ hs' hs'' vf vs f rf fn fn' a:
465
    val_to_loc vf = Some f 
Michael Sammler's avatar
Michael Sammler committed
466
467
    f = fn_loc a 
    σ.(st_fntbl) !! a = Some fn 
468
469
470
    length lsa = length fn.(f_args) 
    length lsv = length fn.(f_local_vars) 
    (* substitute the variables in fn with the corresponding locations *)
Michael Sammler's avatar
Michael Sammler committed
471
    fn' = subst_function (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv))) fn 
472
473
474
475
476
477
    (* check the layout of the arguments *)
    Forall2 has_layout_val vs fn.(f_args).*2 
    (* ensure that locations are aligned *)
    Forall2 has_layout_loc lsa fn.(f_args).*2 
    Forall2 has_layout_loc lsv fn.(f_local_vars).*2 
    (* initialize the local vars to poison *)
Michael Sammler's avatar
Michael Sammler committed
478
    alloc_new_blocks σ.(st_heap) lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' 
479
    (* initialize the arguments with the supplied values *)
Michael Sammler's avatar
Michael Sammler committed
480
    alloc_new_blocks hs' lsa vs hs'' 
481
482
    (* add used blocks allocations  *)
    rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} 
Michael Sammler's avatar
Michael Sammler committed
483
    expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) {| st_heap := hs''; st_fntbl := σ.(st_fntbl)|} []
Michael Sammler's avatar
Michael Sammler committed
484
| CallFailS σ vf vs f fn a:
485
    val_to_loc vf = Some f 
Michael Sammler's avatar
Michael Sammler committed
486
487
    f = fn_loc a 
    σ.(st_fntbl) !! a = Some fn 
488
489
    Forall2 has_layout_val vs fn.(f_args).*2 
    expr_step (Call (Val vf) (Val <$> vs)) σ [] AllocFailed σ []
Michael Sammler's avatar
Michael Sammler committed
490
491
| ConcatS vs σ:
    expr_step (Concat (Val <$> vs)) σ [] (Val (mjoin vs)) σ []
492
| CopyAllocIdS σ v1 v2 a it l:
Michael Sammler's avatar
Michael Sammler committed
493
    val_to_Z v1 it = Some a 
494
495
496
    val_to_loc v2 = Some l 
    valid_ptr (l.1, a) σ.(st_heap) 
    expr_step (CopyAllocId (IntOp it) (Val v1) (Val v2)) σ [] (Val (val_of_loc (l.1, a))) σ []
Michael Sammler's avatar
Michael Sammler committed
497
| IfES v it e1 e2 n σ:
Michael Sammler's avatar
Michael Sammler committed
498
    val_to_Z v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
499
    expr_step (IfE (IntOp it) (Val v) e1 e2) σ [] (if bool_decide (n  0) then e1 else e2)  σ []
Michael Sammler's avatar
Michael Sammler committed
500
501
502
(* no rule for StuckE *)
.

503
504
(*** Evaluation of statements *)
Inductive stmt_step : stmt  runtime_function  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
Michael Sammler's avatar
Michael Sammler committed
505
| AssignS (o : order) rf σ s v1 v2 l v' ot:
506
507
508
    let start_st st := st = if o is Na2Ord then WSt else RSt 0%nat in
    let end_st _ := if o is Na1Ord then WSt else RSt 0%nat in
    let end_val  := if o is Na1Ord then v' else v2 in
Michael Sammler's avatar
Michael Sammler committed
509
    let end_stmt := if o is Na1Ord then Assign Na2Ord ot (Val v1) (Val v2) s else s in
510
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
511
512
513
    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) σ) []
514
515
516
| 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))) σ []
517
| SwitchS rf σ v n m bs s def it :
Michael Sammler's avatar
Michael Sammler committed
518
    val_to_Z v it = Some n 
519
520
521
522
523
    ( i : nat, m !! n = Some i  is_Some (bs !! i)) 
    stmt_step (Switch it (Val v) m bs def) rf σ [] (to_rtstmt rf (default def (i  m !! n; bs !! i))) σ []
| GotoS rf σ b s :
    rf.(rf_fn).(f_code) !! b = Some s 
    stmt_step (Goto b) rf σ [] (to_rtstmt rf s) σ []
524
525
526
| ReturnS rf σ hs v:
    free_blocks σ.(st_heap) rf.(rf_locs) hs  (* Deallocate the stack. *)
    stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} []
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
| SkipSS rf σ s :
    stmt_step (SkipS s) rf σ [] (to_rtstmt rf s) σ []
| ExprSS rf σ s v:
    stmt_step (ExprS (Val v) s) rf σ [] (to_rtstmt rf s) σ []
(* no rule for StuckS *)
.

(*** Evaluation of runtime_expr *)
Inductive runtime_step : runtime_expr  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
| ExprStep e σ κs e' σ' efs:
    expr_step e σ κs e' σ' efs 
    runtime_step (to_rtexpr e) σ κs e' σ' efs
| StmtStep s rf σ κs e' σ' efs:
    stmt_step s rf σ κs e' σ' efs 
    runtime_step (to_rtstmt rf s) σ κs e' σ' efs
| AllocFailedStep σ :
    (* Alloc failure is nb, not ub so we go into an infinite loop*)
    runtime_step AllocFailed σ [] AllocFailed σ [].

546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
Lemma expr_step_preserves_invariant e1 e2 σ1 σ2 κs efs:
  expr_step e1 σ1 κs e2 σ2 efs 
  heap_state_invariant σ1.(st_heap) 
  heap_state_invariant σ2.(st_heap).
Proof.
  move => [] // *.
  all: repeat select (heap_at _ _ _ _ _) ltac:(fun H => destruct H as [?[?[??]]]).
  all: try (rewrite /heap_fmap/=; eapply heap_update_heap_state_invariant => //).
  all: try (unfold has_layout_val in *; by etransitivity).
  repeat eapply alloc_new_blocks_invariant => //.
Qed.

Lemma stmt_step_preserves_invariant s rf e σ1 σ2 κs efs:
  stmt_step s rf σ1 κs e σ2 efs 
  heap_state_invariant σ1.(st_heap) 
  heap_state_invariant σ2.(st_heap).
Proof.
  move => [] //; clear.
  - move => o *.
    revert select (heap_at _ _ _ _ _) => -[?[?[??]]].
    rewrite /heap_fmap/=. eapply heap_update_heap_state_invariant => //.
Michael Sammler's avatar
Michael Sammler committed
567
    match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
568
569
570
571
572
573
574
575
576
577
578
579
580
581
    by destruct o.
  - move => ??? _ Hfree Hinv. by eapply free_blocks_invariant.
Qed.

Lemma runtime_step_preserves_invariant e1 e2 σ1 σ2 κs efs:
  runtime_step e1 σ1 κs e2 σ2 efs 
  heap_state_invariant σ1.(st_heap) 
  heap_state_invariant σ2.(st_heap).
Proof.
  move => [] // *.
  - by eapply expr_step_preserves_invariant.
  - by eapply stmt_step_preserves_invariant.
Qed.

Michael Sammler's avatar
Michael Sammler committed
582
583
(*** evaluation contexts *)
(** for expressions*)
584
Inductive expr_ectx :=
Michael Sammler's avatar
Michael Sammler committed
585
| UnOpCtx (op : un_op) (ot : op_type)
586
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
587
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
588
589
| CopyAllocIdLCtx (ot1 : op_type) (e2 : runtime_expr)
| CopyAllocIdRCtx (ot1 : op_type) (v1 : val)
Michael Sammler's avatar
Michael Sammler committed
590
| DerefCtx (o : order) (ot : op_type)
591
592
593
594
| CallLCtx (args : list runtime_expr)
| CallRCtx (f : val) (vl : list val) (el : list runtime_expr)
| CASLCtx (ot : op_type) (e2 e3 : runtime_expr)
| CASMCtx (ot : op_type) (v1 : val) (e3 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
595
| CASRCtx (ot : op_type) (v1 v2 : val)
596
| ConcatCtx (vs : list val) (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
597
| IfECtx (ot : op_type) (e2 e3 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
598
599
600
| SkipECtx
.

601
Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
Michael Sammler's avatar
Michael Sammler committed
602
  match Ki with
603
604
605
  | UnOpCtx op ot => RTUnOp op ot e
  | BinOpLCtx op ot1 ot2 e2 => RTBinOp op ot1 ot2 e e2
  | BinOpRCtx op ot1 ot2 v1 => RTBinOp op ot1 ot2 (Val v1) e
606
607
  | CopyAllocIdLCtx ot1 e2 => RTCopyAllocId ot1 e e2
  | CopyAllocIdRCtx ot1 v1 => RTCopyAllocId ot1 (Val v1) e
608
609
610
611
612
613
614
  | DerefCtx o l => RTDeref o l e
  | CallLCtx args => RTCall e args
  | CallRCtx f vl el => RTCall (Val f) ((Expr <$> (RTVal <$> vl)) ++ e :: el)
  | CASLCtx ot e2 e3 => RTCAS ot e e2 e3
  | 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)
Michael Sammler's avatar
Michael Sammler committed
615
  | IfECtx ot e2 e3 => RTIfE ot e e2 e3
616
  | SkipECtx => RTSkipE e
Michael Sammler's avatar
Michael Sammler committed
617
618
619
620
621
  end.

(** Statements *)
Inductive stmt_ectx :=
(* Assignment is evalutated right to left, otherwise we need to split contexts *)
Michael Sammler's avatar
Michael Sammler committed
622
623
| AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
624
| ReturnCtx
625
| IfSCtx (ot : op_type) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
626
627
628
629
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
.

630
Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
Michael Sammler's avatar
Michael Sammler committed
631
  match Ki with
Michael Sammler's avatar
Michael Sammler committed
632
633
  | AssignRCtx o ot e1 s => RTAssign o ot e1 e s
  | AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s
634
  | ReturnCtx => RTReturn e
635
  | IfSCtx ot s1 s2 => RTIfS ot e s1 s2
636
637
638
639
640
641
642
  | SwitchCtx it m bs def => RTSwitch it e m bs def
  | ExprSCtx s => RTExprS e s
  end.
Definition to_val (e : runtime_expr) : option val :=
  match e with
  | Expr (RTVal v) => Some v
  | _ => None
Michael Sammler's avatar
Michael Sammler committed
643
644
  end.

645
Definition of_val (v : val) : runtime_expr := Expr (RTVal v).
Michael Sammler's avatar
Michael Sammler committed
646

647
648
649
Inductive lang_ectx :=
| ExprCtx (E : expr_ectx)
| StmtCtx (E : stmt_ectx) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
650

651
652
653
654
655
Definition lang_fill_item (Ki : lang_ectx) (e : runtime_expr) : runtime_expr :=
  match Ki with
  | ExprCtx E => Expr (expr_fill_item E e)
  | StmtCtx E rf => Stmt rf (stmt_fill_item E e)
  end.
Michael Sammler's avatar
Michael Sammler committed
656

657
Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
Michael Sammler's avatar
Michael Sammler committed
658
  to_val e1 = None  to_val e2 = None 
659
660
  (Expr <$> (RTVal <$> vl1)) ++ e1 :: el1 = (Expr <$> (RTVal <$> vl2)) ++ e2 :: el2 
  vl1 = vl2  e1 = e2  el1 = el2.
Michael Sammler's avatar
Michael Sammler committed
661
Proof.
662
663
664
665
666
  revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
  - done.
  - subst. by inversion H1.
  - subst. by inversion H2.
  - destruct (IHvl1 vl2); auto. split; f_equal; auto.
Michael Sammler's avatar
Michael Sammler committed
667
668
Qed.

669
670
Lemma list_expr_val_eq_false vl1 vl2 e el :
  to_val e = None  to_rtexpr <$> (Val <$> vl1) = (Expr <$> (RTVal <$> vl2)) ++ e :: el  False.
Michael Sammler's avatar
Michael Sammler committed
671
Proof.
672
  move => He. elim: vl2 vl1 => [[]//=*|v vl2 IH [|??]?]; csimpl in *; simplify_eq; eauto.
Michael Sammler's avatar
Michael Sammler committed
673
674
Qed.

675
676
Lemma of_to_val (e : runtime_expr) v : to_val e = Some v  Expr (RTVal v) = e.
Proof. case: e => // -[]//. naive_solver. Qed.
Michael Sammler's avatar
Michael Sammler committed
677

678
679
680
Lemma val_stuck e1 σ1 κ e2 σ2 ef :
  runtime_step e1 σ1 κ e2 σ2 ef  to_val e1 = None.
Proof. destruct 1 => //. revert select (expr_step _ _ _ _ _ _). by destruct 1. Qed.
681

682
683
Instance fill_item_inj Ki : Inj (=) (=) (lang_fill_item Ki).
Proof. destruct Ki as [E|E ?]; destruct E; intros ???; simplify_eq/=; auto with f_equal. Qed.
684

685
686
687
Lemma fill_item_val Ki e :
  is_Some (to_val (lang_fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki as [[]|[] ?]; simplify_option_eq; eauto. Qed.
Michael Sammler's avatar
Michael Sammler committed
688

689
690
691
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
  to_val e1 = None  to_val e2 = None 
  lang_fill_item Ki1 e1 = lang_fill_item Ki2 e2  Ki1 = Ki2.
Michael Sammler's avatar
Michael Sammler committed
692
Proof.
693
694
695
  move: Ki1 Ki2 => [ ^ Ki1] [ ^Ki2] He1 He2 ? //; simplify_eq; try done; f_equal.
  all: destruct Ki1E, Ki2E => //; simplify_eq => //.
  all: efeed pose proof list_expr_val_eq_inv as HEQ; [| | done |] => //; naive_solver.
Michael Sammler's avatar
Michael Sammler committed
696
697
Qed.

698
699
Lemma expr_ctx_step_val Ki e σ1 κ e2 σ2 ef :
  runtime_step (lang_fill_item Ki e) σ1 κ e2 σ2 ef  is_Some (to_val e).
Michael Sammler's avatar
Michael Sammler committed
700
Proof.
701
702
703
704
705
  destruct Ki as [[]|[]?]; inversion 1; simplify_eq.
  all: try (revert select (expr_step _ _ _ _ _ _)).
  all: try (revert select (stmt_step _ _ _ _ _ _ _)).
  all: inversion 1; simplify_eq/=; eauto.
  all: apply not_eq_None_Some; intros ?; by eapply list_expr_val_eq_false.
Michael Sammler's avatar
Michael Sammler committed
706
707
Qed.

708
Lemma c_lang_mixin : EctxiLanguageMixin of_val to_val lang_fill_item runtime_step.
Michael Sammler's avatar
Michael Sammler committed
709
Proof.
710
  split => //; eauto using of_to_val, val_stuck, fill_item_inj, fill_item_val, fill_item_no_val_inj, expr_ctx_step_val.
Michael Sammler's avatar
Michael Sammler committed
711
Qed.
712
713
714
Canonical Structure c_ectxi_lang := EctxiLanguage c_lang_mixin.
Canonical Structure c_ectx_lang := EctxLanguageOfEctxi c_ectxi_lang.
Canonical Structure c_lang := LanguageOfEctx c_ectx_lang.
Michael Sammler's avatar
Michael Sammler committed
715

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
716
(** * Useful instances and canonical structures *)
Michael Sammler's avatar
Michael Sammler committed
717

718
Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Michael Sammler's avatar
Michael Sammler committed
719
720
721
Instance val_inhabited : Inhabited val := _.
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Instance stmt_inhabited : Inhabited stmt := populate (Goto "a").
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
722
723
724
725
726
727
Instance function_inhabited : Inhabited function :=
  populate {| f_args := []; f_local_vars := []; f_code := ; f_init := "" |}.
Instance heap_state_inhabited : Inhabited heap_state :=
  populate {| hs_heap := inhabitant; hs_allocs := inhabitant; |}.
Instance state_inhabited : Inhabited state :=
  populate {| st_heap := inhabitant; st_fntbl := inhabitant; |}.
Michael Sammler's avatar
Michael Sammler committed
728
729
730
731

Canonical Structure mbyteO := leibnizO mbyte.
Canonical Structure functionO := leibnizO function.
Canonical Structure locO := leibnizO loc.
732
Canonical Structure alloc_idO := leibnizO alloc_id.
Michael Sammler's avatar
Michael Sammler committed
733
734
735
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
736
Canonical Structure allocationO := leibnizO allocation.