lang.v 27.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.
4
From refinedc.lang Require Export base byte layout int_type loc val heap.
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.
11
12
Definition var_name := string.

Michael Sammler's avatar
Michael Sammler committed
13
14
15
16
17
18
Inductive op_type : Set :=
| IntOp (i : int_type) | PtrOp.

(* 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
19
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | Comma
Michael Sammler's avatar
Michael Sammler committed
20
(* Ptr is the second argument and pffset the first *)
21
| PtrOffsetOp (ly : layout) | PtrNegOffsetOp (ly : layout).
Michael Sammler's avatar
Michael Sammler committed
22
23
24
25
26
27

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

28
29
Section expr.
Local Unset Elimination Schemes.
Michael Sammler's avatar
Michael Sammler committed
30
31
32
33
34
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)
35
| CopyAllocId (ot1 : op_type) (e1 : expr) (e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
36
37
| Deref (o : order) (ly : layout) (e : expr)
| CAS (ot : op_type) (e1 e2 e3 : expr)
38
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
39
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
40
| IfE (ot : op_type) (e1 e2 e3 : 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)) 
52
53
54
55
  ( (o : order) (ly : layout) (e : expr), P e  P (Deref o ly e)) 
  ( (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)) 
57
58
59
60
61
62
63
64
65
66
67
68
69
  ( (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
70
71
72
73
74

(** 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 :=
75
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
| Return (e : expr)
(* m: map from values of e to indices into bs, def: default *)
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| Assign (o : order) (ly : layout) (e1 e2 : expr) (s : stmt)
| 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)
124
125
126
127
| RTDeref (o : order) (ly : layout) (e : runtime_expr)
| 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
134
135
136
137
138
139
| RTSkipE (e : runtime_expr)
| RTStuckE
with rtstmt :=
| RTGoto (b : label)
| RTReturn (e : runtime_expr)
| RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| RTAssign (o : order) (ly : layout) (e1 e2 : runtime_expr) (s : stmt)
| 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)
148
149
150
151
  | Deref o ly e => RTDeref o ly (to_rtexpr e)
  | 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
163
164
165
166
167
168
  | 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)
  | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
  | Assign o ly e1 e2 s => RTAssign o ly (to_rtexpr e1) (to_rtexpr e2) s
  | SkipS s => RTSkipS s
  | StuckS => RTStuckS
  | ExprS e s => RTExprS (to_rtexpr e) s
  end.
169

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

184
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
185

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

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

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

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

Michael Sammler's avatar
Michael Sammler committed
225
226
227
(*** Evaluation of operations *)

(* evaluation can be non-deterministic for comparing pointers *)
228
229
Inductive eval_bin_op : bin_op  op_type  op_type  state  val  val  val  Prop :=
| PtrOffsetOpIP v1 v2 σ o l ly it:
230
    val_to_Z_weak v1 it = Some o 
Michael Sammler's avatar
Michael Sammler committed
231
232
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
233
    heap_state_loc_in_bounds (l offset{ly} o) 0 σ.(st_heap) 
234
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
235
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
236
    val_to_Z_weak v1 it = Some o 
237
    val_to_loc v2 = Some l 
238
    heap_state_loc_in_bounds (l offset{ly} -o) 0 σ.(st_heap) 
239
240
    (* 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))
241
| EqOpPNull v1 v2 σ l v:
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
242
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
Michael Sammler's avatar
Michael Sammler committed
243
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
244
    v2 = NULL 
Michael Sammler's avatar
Michael Sammler committed
245
246
    (* TODO ( see below ): Should we really hard code i32 here because of C? *)
    i2v (Z_of_bool false) i32 = v 
247
248
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
249
    heap_state_loc_in_bounds l 0%nat σ.(st_heap) 
Michael Sammler's avatar
Michael Sammler committed
250
    val_to_loc v1 = Some l 
Michael Sammler's avatar
Michael Sammler committed
251
    v2 = NULL 
Michael Sammler's avatar
Michael Sammler committed
252
    i2v (Z_of_bool true) i32 = v 
253
254
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
255
256
    v1 = NULL 
    v2 = NULL 
Michael Sammler's avatar
Michael Sammler committed
257
    i2v (Z_of_bool true) i32 = v 
258
259
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
260
261
    v1 = NULL 
    v2 = NULL 
Michael Sammler's avatar
Michael Sammler committed
262
    i2v (Z_of_bool false) i32 = v 
263
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
264
| RelOpPP v1 v2 σ l1 l2 v b op:
Michael Sammler's avatar
Michael Sammler committed
265
266
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
267
    valid_ptr l1 σ.(st_heap)  valid_ptr l2 σ.(st_heap) 
268
269
270
271
272
273
274
275
276
    match op with
    | EqOp => Some (bool_decide (l1.2 = l2.2))
    | NeOp => Some (bool_decide (l1.2  l2.2))
    | LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
    | GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
    | LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
    | GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
    | _ => None
    end = Some b 
Michael Sammler's avatar
Michael Sammler committed
277
    i2v (Z_of_bool b) i32 = v 
278
    eval_bin_op op PtrOp PtrOp σ v1 v2 v
279
| RelOpII op v1 v2 σ n1 n2 it b:
Michael Sammler's avatar
Michael Sammler committed
280
281
282
283
284
285
286
287
288
    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 
289
290
    val_to_Z_weak v1 it = Some n1 
    val_to_Z_weak v2 it = Some n2 
Michael Sammler's avatar
Michael Sammler committed
291
292
    (* 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. *)
293
294
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
| ArithOpII op v1 v2 σ n1 n2 it n v:
Michael Sammler's avatar
Michael Sammler committed
295
296
297
298
299
300
301
    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
302
303
    | 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
304
305
306
    | 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
307
308
309
310
311
312
313
314
315
    (* 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
316
317
    | _ => None
    end = Some n 
318
319
    val_to_Z_weak v1 it = Some n1 
    val_to_Z_weak v2 it = Some n2 
320
    val_of_Z (if it_signed it then n else n `mod` int_modulus it) it = Some v 
321
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
322
323
| CommaOp ot1 ot2 σ v1 v2:
    eval_bin_op Comma ot1 ot2 σ v1 v2 v2
Michael Sammler's avatar
Michael Sammler committed
324
325
.

326
Inductive eval_un_op : un_op  op_type  state  val  val  Prop :=
327
328
329
| CastOpII itt its σ vs vt i:
    val_to_int_repr vs its = Some i 
    val_of_int_repr i itt = Some vt 
330
331
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
332
333
    val_to_loc vs = Some l 
    val_of_loc l = vt 
334
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
335
336
| CastOpPI it σ vs vt l:
    val_to_loc vs = Some l 
337
    val_of_int_repr (IRLoc l) it = Some vt 
338
    block_alive l σ.(st_heap) 
339
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
340
341
342
343
| CastOpPINull it σ vs vt:
    vs = NULL 
    val_of_Z 0 it = Some vt 
    eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
344
| CastOpIP it σ vs vt l l':
345
    val_to_loc_weak vs it = Some l 
346
347
348
349
    val_of_loc l' = vt 
    (** This is using that the address 0 is never alive. *)
    l' = (if bool_decide (block_alive l σ.(st_heap)) then l else
           (if bool_decide (l.2 = 0) then NULL_loc else (ProvAlloc None, l.2))) 
350
    eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
351
| NegOpI it σ vs vt n:
352
    val_to_Z_weak vs it = Some n 
353
    val_of_Z (-n) it = Some vt 
354
    eval_un_op NegOp (IntOp it) σ vs vt
355
| NotIntOpI it σ vs vt n:
356
    val_to_Z_weak vs it = Some n 
357
    val_of_Z (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it = Some vt 
358
    eval_un_op NotIntOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
359
360
361
362
.

(*** Evaluation of Expressions *)

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

452
453
454
455
456
457
458
459
460
(*** Evaluation of statements *)
Inductive stmt_step : stmt  runtime_function  state  list Empty_set  runtime_expr  state  list runtime_expr  Prop :=
| AssignS (o : order) rf σ s v1 v2 l v' ly:
    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
    let end_stmt := if o is Na1Ord then Assign Na2Ord ly (Val v1) (Val v2) s else s in
    val_to_loc v1 = Some l 
    v2 `has_layout_val` ly 
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
461
    heap_at l ly v' start_st σ.(st_heap).(hs_heap) 
462
463
    stmt_step (Assign o ly (Val v1) (Val v2) s) rf σ [] (to_rtstmt rf end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
| SwitchS rf σ v n m bs s def it :
464
    val_to_Z_weak v it = Some n 
465
466
467
468
469
    ( 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) σ []
470
471
472
| 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 |} []
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
| 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 σ [].

492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
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
513
    match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
514
515
516
517
518
519
520
521
522
523
524
525
526
527
    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
528
529
(*** evaluation contexts *)
(** for expressions*)
530
Inductive expr_ectx :=
Michael Sammler's avatar
Michael Sammler committed
531
| UnOpCtx (op : un_op) (ot : op_type)
532
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
533
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
534
535
| CopyAllocIdLCtx (ot1 : op_type) (e2 : runtime_expr)
| CopyAllocIdRCtx (ot1 : op_type) (v1 : val)
Michael Sammler's avatar
Michael Sammler committed
536
| DerefCtx (o : order) (l : layout)
537
538
539
540
| 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
541
| CASRCtx (ot : op_type) (v1 v2 : val)
542
| ConcatCtx (vs : list val) (es : list runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
543
| IfECtx (ot : op_type) (e2 e3 : runtime_expr)
Michael Sammler's avatar
Michael Sammler committed
544
545
546
| SkipECtx
.

547
Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
Michael Sammler's avatar
Michael Sammler committed
548
  match Ki with
549
550
551
  | 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
552
553
  | CopyAllocIdLCtx ot1 e2 => RTCopyAllocId ot1 e e2
  | CopyAllocIdRCtx ot1 v1 => RTCopyAllocId ot1 (Val v1) e
554
555
556
557
558
559
560
  | 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
561
  | IfECtx ot e2 e3 => RTIfE ot e e2 e3
562
  | SkipECtx => RTSkipE e
Michael Sammler's avatar
Michael Sammler committed
563
564
565
566
567
568
569
570
571
572
573
574
  end.

(** Statements *)
Inductive stmt_ectx :=
(* Assignment is evalutated right to left, otherwise we need to split contexts *)
| AssignRCtx (o : order) (ly : layout) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ly : layout) (v2 : val) (s : stmt)
| ReturnCtx
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
.

575
Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
Michael Sammler's avatar
Michael Sammler committed
576
  match Ki with
577
578
579
580
581
582
583
584
585
586
  | AssignRCtx o ly e1 s => RTAssign o ly e1 e s
  | AssignLCtx o ly v2 s => RTAssign o ly e (Val v2) s
  | ReturnCtx => RTReturn e
  | 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
587
588
  end.

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

591
592
593
Inductive lang_ectx :=
| ExprCtx (E : expr_ectx)
| StmtCtx (E : stmt_ectx) (rf : runtime_function).
Michael Sammler's avatar
Michael Sammler committed
594

595
596
597
598
599
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
600

601
Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
Michael Sammler's avatar
Michael Sammler committed
602
  to_val e1 = None  to_val e2 = None 
603
604
  (Expr <$> (RTVal <$> vl1)) ++ e1 :: el1 = (Expr <$> (RTVal <$> vl2)) ++ e2 :: el2 
  vl1 = vl2  e1 = e2  el1 = el2.
Michael Sammler's avatar
Michael Sammler committed
605
Proof.
606
607
608
609
610
  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
611
612
Qed.

613
614
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
615
Proof.
616
  move => He. elim: vl2 vl1 => [[]//=*|v vl2 IH [|??]?]; csimpl in *; simplify_eq; eauto.
Michael Sammler's avatar
Michael Sammler committed
617
618
Qed.

619
620
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
621

622
623
624
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.
625

626
627
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.
628

629
630
631
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
632

633
634
635
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
636
Proof.
637
638
639
  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
640
641
Qed.

642
643
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
644
Proof.
645
646
647
648
649
  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
650
651
Qed.

652
Lemma c_lang_mixin : EctxiLanguageMixin of_val to_val lang_fill_item runtime_step.
Michael Sammler's avatar
Michael Sammler committed
653
Proof.
654
  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
655
Qed.
656
657
658
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
659

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

662
Instance mbyte_inhabited : Inhabited mbyte := populate (MPoison).
Michael Sammler's avatar
Michael Sammler committed
663
664
665
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
666
667
668
669
670
671
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
672
673
674
675

Canonical Structure mbyteO := leibnizO mbyte.
Canonical Structure functionO := leibnizO function.
Canonical Structure locO := leibnizO loc.
676
Canonical Structure alloc_idO := leibnizO alloc_id.
Michael Sammler's avatar
Michael Sammler committed
677
678
679
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
680
Canonical Structure allocationO := leibnizO allocation.