lang.v 29.9 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
16
| ShrOp | EqOp (rit : int_type) | NeOp (rit : int_type) | LtOp (rit : int_type)
| GtOp (rit : int_type) | LeOp (rit : int_type) | GeOp (rit : int_type) | Comma
17
18
19
20
(* 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
21
22
23
24
25
26

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

27
28
Section expr.
Local Unset Elimination Schemes.
Michael Sammler's avatar
Michael Sammler committed
29
30
31
32
33
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)
34
| CopyAllocId (ot1 : op_type) (e1 : expr) (e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
35
| Deref (o : order) (ot : op_type) (e : expr)
Michael Sammler's avatar
Michael Sammler committed
36
| CAS (ot : op_type) (e1 e2 e3 : expr)
37
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
38
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
39
| IfE (ot : op_type) (e1 e2 e3 : expr)
Lennard Gäher's avatar
Lennard Gäher committed
40
| Alloc (ly : layout) (e : expr)
Michael Sammler's avatar
Michael Sammler committed
41
42
43
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
44
45
46
47
48
49
50
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)) 
51
  ( (ot1 : op_type) (e1 e2 : expr), P e1  P e2  P (CopyAllocId ot1 e1 e2)) 
Michael Sammler's avatar
Michael Sammler committed
52
  ( (o : order) (ot : op_type) (e : expr), P e  P (Deref o ot e)) 
53
54
55
  ( (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
56
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
Lennard Gäher's avatar
Lennard Gäher committed
57
  ( (ly : layout) (e : expr), P e  P (Alloc ly e)) 
58
59
60
61
62
63
64
65
66
67
68
69
70
  ( (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
71
72
73
74
75

(** 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 :=
76
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
77
| Return (e : expr)
78
| IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
79
80
(* 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
81
| Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
Lennard Gäher's avatar
Lennard Gäher committed
82
| Free (ly : layout) (e : expr) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
83
84
85
86
87
88
89
90
91
92
93
| 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; ?*)
94
95
  f_code : gmap label stmt;
  f_init : label;
Michael Sammler's avatar
Michael Sammler committed
96
97
}.

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

Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
104
105
106
107
108
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
109
110
111
112
113
114
115
116
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);
}.

117
118
119
120
121
122
123
124
125
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)
126
| RTCopyAllocId (ot1 : op_type) (e1 : runtime_expr) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
127
| RTDeref (o : order) (ot : op_type) (e : runtime_expr)
128
129
130
| RTCall (f : runtime_expr) (args : list runtime_expr)
| RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
| RTConcat (es : list runtime_expr)
Lennard Gäher's avatar
Lennard Gäher committed
131
| RTAlloc (ly : layout) (e : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
132
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
133
134
135
136
137
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
138
| RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt)
139
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
Michael Sammler's avatar
Michael Sammler committed
140
| RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt)
Lennard Gäher's avatar
Lennard Gäher committed
141
| RTFree (ly : layout) (e : runtime_expr) (s : stmt)
142
143
144
145
| RTSkipS (s : stmt)
| RTStuckS
| RTExprS (e : runtime_expr) (s : stmt)
.
146

147
148
149
150
151
152
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)
153
  | CopyAllocId ot1 e1 e2 => RTCopyAllocId ot1 (to_rtexpr e1) (to_rtexpr e2)
Michael Sammler's avatar
Michael Sammler committed
154
  | Deref o ot e => RTDeref o ot (to_rtexpr e)
155
156
157
  | 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
158
  | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
Lennard Gäher's avatar
Lennard Gäher committed
159
  | Alloc ly e => RTAlloc ly (to_rtexpr e)
160
161
162
163
164
165
166
167
168
169
  | 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)
170
  | IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2
171
  | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
Michael Sammler's avatar
Michael Sammler committed
172
  | Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s
Lennard Gäher's avatar
Lennard Gäher committed
173
  | Free ly e s => RTFree ly (to_rtexpr e) s
174
175
176
177
  | SkipS s => RTSkipS s
  | StuckS => RTStuckS
  | ExprS e s => RTExprS (to_rtexpr e) s
  end.
178

179
180
181
182
183
184
185
186
187
188
189
190
191
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
192

193
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
194

195
196
(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
197
  match e with
198
199
200
201
  | 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)
202
  | CopyAllocId ot1 e1 e2 => CopyAllocId ot1 (subst x v e1) (subst x v e2)
203
204
205
206
  | 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
207
  | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
Lennard Gäher's avatar
Lennard Gäher committed
208
  | Alloc ly e => Alloc ly (subst x v e)
209
210
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
Michael Sammler's avatar
Michael Sammler committed
211
212
  end.

Michael Sammler's avatar
Michael Sammler committed
213
214
215
216
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
217
218
  end.

Michael Sammler's avatar
Michael Sammler committed
219
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
220
221
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
222
  | Return e => Return (subst_l xs e)
223
  | 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
224
  | 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
225
  | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
Lennard Gäher's avatar
Lennard Gäher committed
226
  | Free ly e s => Free ly (subst_l xs e) (subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
227
  | SkipS s => SkipS (subst_stmt xs s)
228
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
229
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
230
231
  end.

Michael Sammler's avatar
Michael Sammler committed
232
233
Definition subst_function (xs : list (var_name * val)) (f : function) : function := {|
  f_code := (subst_stmt xs) <$> f.(f_code);
234
235
236
  f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.

Michael Sammler's avatar
Michael Sammler committed
237
238
239
(*** Evaluation of operations *)

(* evaluation can be non-deterministic for comparing pointers *)
240
241
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
242
    val_to_Z v1 it = Some o 
Michael Sammler's avatar
Michael Sammler committed
243
244
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
245
    heap_state_loc_in_bounds (l offset{ly} o) 0 σ.(st_heap) 
246
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
247
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
Michael Sammler's avatar
Michael Sammler committed
248
    val_to_Z v1 it = Some o 
249
    val_to_loc v2 = Some l 
250
    heap_state_loc_in_bounds (l offset{ly} -o) 0 σ.(st_heap) 
251
252
    (* 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))
253
254
255
256
| PtrDiffOpPP v1 v2 σ l1 l2 ly v:
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
    l1.1 = l2.1 
257
    0 < ly.(ly_size) 
258
259
    valid_ptr l1 σ.(st_heap) 
    valid_ptr l2 σ.(st_heap) 
260
    val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some v 
261
    eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
262
| CmpOpPP v1 v2 σ l1 l2 v op e b rit:
Michael Sammler's avatar
Michael Sammler committed
263
264
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
Michael Sammler's avatar
Michael Sammler committed
265
    heap_loc_eq l1 l2 σ.(st_heap) = Some e 
266
    match op with
Michael Sammler's avatar
Michael Sammler committed
267
268
    | EqOp rit => Some (e, rit)
    | NeOp rit => Some (negb e, rit)
Michael Sammler's avatar
Michael Sammler committed
269
    | _ => None
270
271
    end = Some (b, rit) 
    val_of_Z (Z_of_bool b) rit None = Some v 
Michael Sammler's avatar
Michael Sammler committed
272
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
273
| RelOpPP v1 v2 σ l1 l2 p a1 a2 v b op rit:
Michael Sammler's avatar
Michael Sammler committed
274
275
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
Michael Sammler's avatar
Michael Sammler committed
276
277
278
279
280
    (* Note that this enforces that the locations have the same provenance. *)
    l1 = (ProvAlloc p, a1) 
    l2 = (ProvAlloc p, a2) 
    valid_ptr l1 σ.(st_heap)  valid_ptr l2 σ.(st_heap) 
    (* Equal comparison is handled by heap_loc_eq *)
Michael Sammler's avatar
Michael Sammler committed
281
    match op with
Michael Sammler's avatar
Michael Sammler committed
282
283
284
285
    | LtOp rit => Some (bool_decide (a1 < a2), rit)
    | GtOp rit => Some (bool_decide (a1 > a2), rit)
    | LeOp rit => Some (bool_decide (a1 <= a2), rit)
    | GeOp rit => Some (bool_decide (a1 >= a2), rit)
286
    | _ => None
287
288
    end = Some (b, rit) 
    val_of_Z (Z_of_bool b) rit None = Some v 
289
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
290
| RelOpII op v1 v2 v σ n1 n2 it b rit:
Michael Sammler's avatar
Michael Sammler committed
291
    match op with
292
293
294
295
296
297
    | EqOp rit => Some (bool_decide (n1 = n2), rit)
    | NeOp rit => Some (bool_decide (n1  n2), rit)
    | LtOp rit => Some (bool_decide (n1 < n2), rit)
    | GtOp rit => Some (bool_decide (n1 > n2), rit)
    | LeOp rit => Some (bool_decide (n1 <= n2), rit)
    | GeOp rit => Some (bool_decide (n1 >= n2), rit)
Michael Sammler's avatar
Michael Sammler committed
298
    | _ => None
299
    end = Some (b, rit) 
Michael Sammler's avatar
Michael Sammler committed
300
301
    val_to_Z v1 it = Some n1 
    val_to_Z v2 it = Some n2 
302
    val_of_Z (Z_of_bool b) rit None = Some v 
Michael Sammler's avatar
Michael Sammler committed
303
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
304
| ArithOpII op v1 v2 σ n1 n2 it n v:
Michael Sammler's avatar
Michael Sammler committed
305
306
307
308
309
310
311
    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
312
313
    | 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
314
315
316
    | 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
317
318
319
320
321
322
323
324
325
    (* 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
326
327
    | _ => None
    end = Some n 
Michael Sammler's avatar
Michael Sammler committed
328
329
330
    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 
331
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
332
333
| CommaOp ot1 ot2 σ v1 v2:
    eval_bin_op Comma ot1 ot2 σ v1 v2 v2
Michael Sammler's avatar
Michael Sammler committed
334
335
.

336
Inductive eval_un_op : un_op  op_type  state  val  val  Prop :=
337
| CastOpII itt its σ vs vt i:
Michael Sammler's avatar
Michael Sammler committed
338
339
    val_to_Z vs its = Some i 
    val_of_Z i itt (val_to_byte_prov vs) = Some vt 
340
341
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
342
343
    val_to_loc vs = Some l 
    val_of_loc l = vt 
344
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
Michael Sammler's avatar
Michael Sammler committed
345
| CastOpPI it σ vs vt l p:
346
    val_to_loc vs = Some l 
Michael Sammler's avatar
Michael Sammler committed
347
348
    l.1 = ProvAlloc p 
    val_of_Z l.2 it p = Some vt 
349
    block_alive l σ.(st_heap) 
350
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
351
352
353
354
355
356
| 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
357
358
| CastOpPINull it σ vs vt:
    vs = NULL 
Michael Sammler's avatar
Michael Sammler committed
359
    val_of_Z 0 it None = Some vt 
360
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
Michael Sammler's avatar
Michael Sammler committed
361
362
363
| CastOpIP it σ vs vt l l' a:
    val_to_Z vs it = Some a 
    l = (ProvAlloc (val_to_byte_prov vs), a) 
364
    (** This is using that the address 0 is never alive. *)
365
    l' = (if bool_decide (valid_ptr l σ.(st_heap)) then l else
366
367
368
369
370
            (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
371
    val_of_loc l' = vt 
372
    eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
373
| NegOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
374
375
    val_to_Z vs it = Some n 
    val_of_Z (-n) it None = Some vt 
376
    eval_un_op NegOp (IntOp it) σ vs vt
377
| NotIntOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
378
379
    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 
380
    eval_un_op NotIntOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
381
382
383
384
.

(*** Evaluation of Expressions *)

385
Inductive expr_step : expr  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
Michael Sammler's avatar
Michael Sammler committed
386
387
388
| SkipES v σ:
    expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
389
    eval_un_op op ot σ v v' 
Michael Sammler's avatar
Michael Sammler committed
390
391
    expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
392
    eval_bin_op op ot1 ot2 σ v1 v2 v' 
Michael Sammler's avatar
Michael Sammler committed
393
    expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
Michael Sammler's avatar
Michael Sammler committed
394
| DerefS o v l ot v' σ:
Michael Sammler's avatar
Michael Sammler committed
395
    let start_st st :=  n, st = if o is Na2Ord then RSt (S n) else RSt n in
396
397
398
399
400
401
402
403
    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
404
    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
405
    val_to_loc v = Some l 
Michael Sammler's avatar
Michael Sammler committed
406
407
    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
408
409
410
411
412
(* 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
413
    heap_at l1 (it_layout it) vo (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
414
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
415
    heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
416
417
    val_to_Z vo it = Some z1 
    val_to_Z ve it = Some z2 
Michael Sammler's avatar
Michael Sammler committed
418
    v3 `has_layout_val` it_layout it 
419
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
420
421
422
423
424
    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
425
    heap_at l1 (it_layout it) vo (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
426
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
427
    heap_at l2 (it_layout it) ve (λ st,  n, st = RSt n) σ.(st_heap).(hs_heap) 
Michael Sammler's avatar
Michael Sammler committed
428
429
    val_to_Z vo it = Some z1 
    val_to_Z ve it = Some z2 
Michael Sammler's avatar
Michael Sammler committed
430
    v3 `has_layout_val` it_layout it 
431
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
432
433
434
    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
435
| CallS lsa lsv σ hs' hs'' vf vs f rf fn fn' a:
436
    val_to_loc vf = Some f 
Michael Sammler's avatar
Michael Sammler committed
437
438
    f = fn_loc a 
    σ.(st_fntbl) !! a = Some fn 
439
440
441
    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
442
    fn' = subst_function (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv))) fn 
443
444
445
446
447
448
    (* 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 *)
Lennard Gäher's avatar
Lennard Gäher committed
449
    alloc_new_blocks σ.(st_heap) StackAlloc lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' 
450
    (* initialize the arguments with the supplied values *)
Lennard Gäher's avatar
Lennard Gäher committed
451
    alloc_new_blocks hs' StackAlloc lsa vs hs'' 
452
453
    (* 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
454
    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
455
| CallFailS σ vf vs f fn a:
456
    val_to_loc vf = Some f 
Michael Sammler's avatar
Michael Sammler committed
457
458
    f = fn_loc a 
    σ.(st_fntbl) !! a = Some fn 
459
460
    Forall2 has_layout_val vs fn.(f_args).*2 
    expr_step (Call (Val vf) (Val <$> vs)) σ [] AllocFailed σ []
Michael Sammler's avatar
Michael Sammler committed
461
462
| ConcatS vs σ:
    expr_step (Concat (Val <$> vs)) σ [] (Val (mjoin vs)) σ []
463
| CopyAllocIdS σ v1 v2 a it l:
Michael Sammler's avatar
Michael Sammler committed
464
    val_to_Z v1 it = Some a 
465
466
467
    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))) σ []
468
469
470
| IfES v ot e1 e2 b σ:
    cast_to_bool ot v σ.(st_heap) = Some b 
    expr_step (IfE ot (Val v) e1 e2) σ [] (if b then e1 else e2) σ []
Lennard Gäher's avatar
Lennard Gäher committed
471
472
473
474
475
476
477
478
| AllocS v l ly σ hs' :
    has_layout_val v ly 
    has_layout_loc l ly 
    alloc_new_block σ.(st_heap) HeapAlloc l v hs' 
    expr_step (Alloc ly (Val v)) σ [] (Val (val_of_loc l)) {| st_heap := hs'; st_fntbl := σ.(st_fntbl) |} []
| AllocFailS v ly σ :
    has_layout_val v ly 
    expr_step (Alloc ly (Val v)) σ [] AllocFailed σ []
Michael Sammler's avatar
Michael Sammler committed
479
480
481
(* no rule for StuckE *)
.

482
483
(*** 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
484
| AssignS (o : order) rf σ s v1 v2 l v' ot:
485
486
487
    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
488
    let end_stmt := if o is Na1Ord then Assign Na2Ord ot (Val v1) (Val v2) s else s in
489
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
490
491
492
    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) σ) []
493
494
495
| IfSS ot v s1 s2 rf σ b:
    cast_to_bool ot v σ.(st_heap) = Some b 
    stmt_step (IfS ot (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if b then s1 else s2))) σ []
496
| SwitchS rf σ v n m bs s def it :
Michael Sammler's avatar
Michael Sammler committed
497
    val_to_Z v it = Some n 
498
499
500
501
502
    ( 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) σ []
503
| ReturnS rf σ hs v:
Lennard Gäher's avatar
Lennard Gäher committed
504
    free_blocks σ.(st_heap) StackAlloc rf.(rf_locs) hs  (* Deallocate the stack. *)
505
    stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} []
Lennard Gäher's avatar
Lennard Gäher committed
506
507
508
509
510
| FreeS ly v l s rf σ hs' :
    val_to_loc v = Some l 
    has_layout_loc l ly 
    free_block σ.(st_heap) HeapAlloc l ly hs' 
    stmt_step (Free ly (Val v) s) rf σ [] (to_rtstmt rf s) {| st_fntbl := σ.(st_fntbl); st_heap := hs' |} []
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
| 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 σ [].

530
531
532
533
534
535
536
537
538
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).
Lennard Gäher's avatar
Lennard Gäher committed
539
540
  - repeat eapply alloc_new_blocks_invariant => //.
  - eapply alloc_new_block_invariant => //.
541
542
543
544
545
546
547
548
549
550
551
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
552
    match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
553
554
    by destruct o.
  - move => ??? _ Hfree Hinv. by eapply free_blocks_invariant.
Lennard Gäher's avatar
Lennard Gäher committed
555
  - move => ??? _ _ ???? Hfree Hinv. by eapply free_block_invariant.
556
557
558
559
560
561
562
563
564
565
566
567
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
568
569
(*** evaluation contexts *)
(** for expressions*)
570
Inductive expr_ectx :=
Michael Sammler's avatar
Michael Sammler committed
571
| UnOpCtx (op : un_op) (ot : op_type)
572
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
573
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
574
575
| CopyAllocIdLCtx (ot1 : op_type) (e2 : runtime_expr)
| CopyAllocIdRCtx (ot1 : op_type) (v1 : val)
Michael Sammler's avatar
Michael Sammler committed
576
| DerefCtx (o : order) (ot : op_type)
577
578
579
580
| 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
581
| CASRCtx (ot : op_type) (v1 v2 : val)
582
| ConcatCtx (vs : list val) (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
583
| IfECtx (ot : op_type) (e2 e3 : runtime_expr)
Lennard Gäher's avatar
Lennard Gäher committed
584
| AllocCtx (ly : layout)
Michael Sammler's avatar
Michael Sammler committed
585
586
587
| SkipECtx
.

588
Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
Michael Sammler's avatar
Michael Sammler committed
589
  match Ki with
590
591
592
  | 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
593
594
  | CopyAllocIdLCtx ot1 e2 => RTCopyAllocId ot1 e e2
  | CopyAllocIdRCtx ot1 v1 => RTCopyAllocId ot1 (Val v1) e
595
596
597
598
599
600
601
  | 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
602
  | IfECtx ot e2 e3 => RTIfE ot e e2 e3
Lennard Gäher's avatar
Lennard Gäher committed
603
  | AllocCtx ly => RTAlloc ly e
604
  | SkipECtx => RTSkipE e
Michael Sammler's avatar
Michael Sammler committed
605
606
607
608
609
  end.

(** Statements *)
Inductive stmt_ectx :=
(* Assignment is evalutated right to left, otherwise we need to split contexts *)
Michael Sammler's avatar
Michael Sammler committed
610
611
| 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
612
| ReturnCtx
Lennard Gäher's avatar
Lennard Gäher committed
613
| FreeCtx (ly : layout) (s : stmt)
614
| IfSCtx (ot : op_type) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
615
616
617
618
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
.

619
Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
Michael Sammler's avatar
Michael Sammler committed
620
  match Ki with
Michael Sammler's avatar
Michael Sammler committed
621
622
  | AssignRCtx o ot e1 s => RTAssign o ot e1 e s
  | AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s
623
  | ReturnCtx => RTReturn e
Lennard Gäher's avatar
Lennard Gäher committed
624
  | FreeCtx ly s => RTFree ly e s
625
  | IfSCtx ot s1 s2 => RTIfS ot e s1 s2
626
627
628
629
630
631
632
  | 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
633
634
  end.

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

637
638
639
Inductive lang_ectx :=
| ExprCtx (E : expr_ectx)
| StmtCtx (E : stmt_ectx) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
640

641
642
643
644
645
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
646

647
Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
Michael Sammler's avatar
Michael Sammler committed
648
  to_val e1 = None  to_val e2 = None 
649
650
  (Expr <$> (RTVal <$> vl1)) ++ e1 :: el1 = (Expr <$> (RTVal <$> vl2)) ++ e2 :: el2 
  vl1 = vl2  e1 = e2  el1 = el2.
Michael Sammler's avatar
Michael Sammler committed
651
Proof.
652
653
654
655
656
  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
657
658
Qed.

659
660
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
661
Proof.
662
  move => He. elim: vl2 vl1 => [[]//=*|v vl2 IH [|??]?]; csimpl in *; simplify_eq; eauto.
Michael Sammler's avatar
Michael Sammler committed
663
664
Qed.

665
666
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
667

668
669
670
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.
671

672
673
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.
674

675
676
677
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
678

679
680
681
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
682
Proof.
683
684
685
  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
686
687
Qed.

688
689
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
690
Proof.
691
692
693
694
695
  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
696
697
Qed.

698
Lemma c_lang_mixin : EctxiLanguageMixin of_val to_val lang_fill_item runtime_step.
Michael Sammler's avatar
Michael Sammler committed
699
Proof.
700
  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
701
Qed.
702
703
704
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
705

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

708
Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Michael Sammler's avatar
Michael Sammler committed
709
710
711
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
712
713
714
715
716
717
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
718
719
720
721

Canonical Structure mbyteO := leibnizO mbyte.
Canonical Structure functionO := leibnizO function.
Canonical Structure locO := leibnizO loc.
722
Canonical Structure alloc_idO := leibnizO alloc_id.
Michael Sammler's avatar
Michael Sammler committed
723
724
725
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
726
Canonical Structure allocationO := leibnizO allocation.