lang.v 28.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)
Michael Sammler's avatar
Michael Sammler committed
40
41
42
| SkipE (e : expr)
| StuckE (* stuck expression *)
.
43
44
45
46
47
48
49
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)) 
50
  ( (ot1 : op_type) (e1 e2 : expr), P e1  P e2  P (CopyAllocId ot1 e1 e2)) 
Michael Sammler's avatar
Michael Sammler committed
51
  ( (o : order) (ot : op_type) (e : expr), P e  P (Deref o ot e)) 
52
53
54
  ( (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
55
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
56
57
58
59
60
61
62
63
64
65
66
67
68
  ( (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
69
70
71
72
73

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

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

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

114
115
116
117
118
119
120
121
122
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)
123
| RTCopyAllocId (ot1 : op_type) (e1 : runtime_expr) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
124
| RTDeref (o : order) (ot : op_type) (e : runtime_expr)
125
126
127
| 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
128
| RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
129
130
131
132
133
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
134
| RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt)
135
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
Michael Sammler's avatar
Michael Sammler committed
136
| RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt)
137
138
139
140
| RTSkipS (s : stmt)
| RTStuckS
| RTExprS (e : runtime_expr) (s : stmt)
.
141

142
143
144
145
146
147
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)
148
  | CopyAllocId ot1 e1 e2 => RTCopyAllocId ot1 (to_rtexpr e1) (to_rtexpr e2)
Michael Sammler's avatar
Michael Sammler committed
149
  | Deref o ot e => RTDeref o ot (to_rtexpr e)
150
151
152
  | 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
153
  | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
154
155
156
157
158
159
160
161
162
163
  | 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)
164
  | IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2
165
  | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
Michael Sammler's avatar
Michael Sammler committed
166
  | Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s
167
168
169
170
  | SkipS s => RTSkipS s
  | StuckS => RTStuckS
  | ExprS e s => RTExprS (to_rtexpr e) s
  end.
171

172
173
174
175
176
177
178
179
180
181
182
183
184
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
185

186
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
187

188
189
(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
190
  match e with
191
192
193
194
  | 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)
195
  | CopyAllocId ot1 e1 e2 => CopyAllocId ot1 (subst x v e1) (subst x v e2)
196
197
198
199
  | 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
200
  | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
201
202
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
Michael Sammler's avatar
Michael Sammler committed
203
204
  end.

Michael Sammler's avatar
Michael Sammler committed
205
206
207
208
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
209
210
  end.

Michael Sammler's avatar
Michael Sammler committed
211
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
212
213
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
214
  | Return e => Return (subst_l xs e)
215
  | 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
216
  | 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
217
  | 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
218
  | SkipS s => SkipS (subst_stmt xs s)
219
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
220
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
221
222
  end.

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

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

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

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

(*** Evaluation of Expressions *)

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

469
470
(*** 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
471
| AssignS (o : order) rf σ s v1 v2 l v' ot:
472
473
474
    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
475
    let end_stmt := if o is Na1Ord then Assign Na2Ord ot (Val v1) (Val v2) s else s in
476
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
477
478
479
    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) σ) []
480
481
482
| 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))) σ []
483
| SwitchS rf σ v n m bs s def it :
Michael Sammler's avatar
Michael Sammler committed
484
    val_to_Z v it = Some n 
485
486
487
488
489
    ( 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) σ []
490
491
492
| 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 |} []
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
| 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 σ [].

512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
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
533
    match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
534
535
536
537
538
539
540
541
542
543
544
545
546
547
    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
548
549
(*** evaluation contexts *)
(** for expressions*)
550
Inductive expr_ectx :=
Michael Sammler's avatar
Michael Sammler committed
551
| UnOpCtx (op : un_op) (ot : op_type)
552
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
553
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
554
555
| CopyAllocIdLCtx (ot1 : op_type) (e2 : runtime_expr)
| CopyAllocIdRCtx (ot1 : op_type) (v1 : val)
Michael Sammler's avatar
Michael Sammler committed
556
| DerefCtx (o : order) (ot : op_type)
557
558
559
560
| 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
561
| CASRCtx (ot : op_type) (v1 v2 : val)
562
| ConcatCtx (vs : list val) (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
563
| IfECtx (ot : op_type) (e2 e3 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
564
565
566
| SkipECtx
.

567
Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
Michael Sammler's avatar
Michael Sammler committed
568
  match Ki with
569
570
571
  | 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
572
573
  | CopyAllocIdLCtx ot1 e2 => RTCopyAllocId ot1 e e2
  | CopyAllocIdRCtx ot1 v1 => RTCopyAllocId ot1 (Val v1) e
574
575
576
577
578
579
580
  | 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
581
  | IfECtx ot e2 e3 => RTIfE ot e e2 e3
582
  | SkipECtx => RTSkipE e
Michael Sammler's avatar
Michael Sammler committed
583
584
585
586
587
  end.

(** Statements *)
Inductive stmt_ectx :=
(* Assignment is evalutated right to left, otherwise we need to split contexts *)
Michael Sammler's avatar
Michael Sammler committed
588
589
| 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
590
| ReturnCtx
591
| IfSCtx (ot : op_type) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
592
593
594
595
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
.

596
Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
Michael Sammler's avatar
Michael Sammler committed
597
  match Ki with
Michael Sammler's avatar
Michael Sammler committed
598
599
  | AssignRCtx o ot e1 s => RTAssign o ot e1 e s
  | AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s
600
  | ReturnCtx => RTReturn e
601
  | IfSCtx ot s1 s2 => RTIfS ot e s1 s2
602
603
604
605
606
607
608
  | 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
609
610
  end.

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

613
614
615
Inductive lang_ectx :=
| ExprCtx (E : expr_ectx)
| StmtCtx (E : stmt_ectx) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
616

617
618
619
620
621
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
622

623
Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
Michael Sammler's avatar
Michael Sammler committed
624
  to_val e1 = None  to_val e2 = None 
625
626
  (Expr <$> (RTVal <$> vl1)) ++ e1 :: el1 = (Expr <$> (RTVal <$> vl2)) ++ e2 :: el2 
  vl1 = vl2  e1 = e2  el1 = el2.
Michael Sammler's avatar
Michael Sammler committed
627
Proof.
628
629
630
631
632
  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
633
634
Qed.

635
636
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
637
Proof.
638
  move => He. elim: vl2 vl1 => [[]//=*|v vl2 IH [|??]?]; csimpl in *; simplify_eq; eauto.
Michael Sammler's avatar
Michael Sammler committed
639
640
Qed.

641
642
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
643

644
645
646
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.
647

648
649
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.
650

651
652
653
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
654

655
656
657
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
658
Proof.
659
660
661
  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
662
663
Qed.

664
665
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
666
Proof.
667
668
669
670
671
  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
672
673
Qed.

674
Lemma c_lang_mixin : EctxiLanguageMixin of_val to_val lang_fill_item runtime_step.
Michael Sammler's avatar
Michael Sammler committed
675
Proof.
676
  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
677
Qed.
678
679
680
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
681

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

684
Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Michael Sammler's avatar
Michael Sammler committed
685
686
687
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
688
689
690
691
692
693
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
694
695
696
697

Canonical Structure mbyteO := leibnizO mbyte.
Canonical Structure functionO := leibnizO function.
Canonical Structure locO := leibnizO loc.
698
Canonical Structure alloc_idO := leibnizO alloc_id.
Michael Sammler's avatar
Michael Sammler committed
699
700
701
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
702
Canonical Structure allocationO := leibnizO allocation.