-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathsemantics.v
142 lines (117 loc) · 4.82 KB
/
semantics.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
Require Import ZArith String.
Require Import List.
Open Scope Z_scope.
Open Scope string_scope.
(* Definitions of ±C expressions *)
Inductive mon_op : Type :=
| M_MINUS | M_NOT | M_POST_INC
| M_POST_DEC | M_PRE_INC | M_PRE_DEC | M_DEREF | M_ADDR.
Inductive bin_op : Type :=
| S_MUL | S_DIV | S_MOD | S_ADD
| S_SUB | S_INDEX | S_SHL | S_SHR | S_AND | S_OR | S_XOR.
Inductive cmp_op : Type := C_LT | C_LE | C_EQ | C_GT | C_GE | C_NE.
Inductive expr : Type :=
| VAR (x:string)
| CST (n:Z)
| STRING (s:string)
| SET_VAR (s:string) (e:expr)
| SET_ARRAY (t:string) (e:expr) (e':expr)
| SET_DEREF (lhs:expr) (rhs:expr)
| OPSET_VAR (op:bin_op) (x:string) (e:expr)
| OPSET_ARRAY (op:bin_op) (x:string) (i:expr) (e:expr)
| OPSET_DEREF (op:bin_op) (a:expr) (e:expr)
| CALL (f:string) (args:list expr)
| OP1 (op:mon_op) (e:expr)
| OP2 (op:bin_op) (lhs:expr) (rhs:expr)
| CMP (op:cmp_op) (lhs:expr) (rhs:expr)
| EIF (cnd:expr) (e1:expr) (e0:expr)
| ESEQ (es:list expr).
Inductive var_decl : Type :=
| VDECL (name:string) (init:option expr).
Inductive code : Type :=
| CBLOCK (cs:list code)
| CLOCAL (vs:list var_decl)
| CEXPR (e:expr)
| CIF (cnd:expr) (c1 c0 : code)
| CWHILE (cnd:expr) (body:code) (fin:option expr) (tst:bool)
| CRETURN (e:option expr)
| CBREAK
| CCONTINUE
| CSWITCH (e:expr) (cases:list (Z * list code)) (default:code)
| CTRY (body:code) (catches:list catch) (fin:option code)
| CTHROW (exc:string) (val:expr)
with catch : Type :=
| CATCH (exc bind : string) (handle:code).
Inductive toplevel_decl : Type :=
| CDECL (name:string) (init:option expr)
| CFUN (name:string) (args:list var_decl) (body:code).
(* A memory model *)
Definition memory : Set := list (Z * Z).
Definition uint_max := Zpower_nat 2 64 - 1.
Definition int_max := Zpower_nat 2 63 - 1.
Definition int_min := - Zpower_nat 2 63.
Definition signed_to_unsigned_64 (n:Z) := if Z.gtb n 0 then n else (Zpower_nat 2 64 + n + 1).
Definition unsigned_to_signed_64 (n:Z) := if Z.gtb n int_max then (n - Zpower_nat 2 64) else n.
Lemma unsigned_inverse : forall n, n >= 0 /\ n <= uint_max -> signed_to_unsigned_64 (unsigned_to_signed_64 n) = n.
Proof.
intros.
destruct (Z.gtb n 0).
- auto.
- auto.
Qed.
Compute (signed_to_unsigned_64 (-1)).
Fixpoint rd_raw (m:memory) (a:Z) :=
match m with
| nil => 0
| (loc,val) :: rest => if Z.eqb loc a then val else (rd_raw rest a)
end.
Fixpoint rd_bytes (m:memory) (a:Z) (i:nat) :=
match i with
| O => 0
| S p => (rd_bytes m (a+1) p) * 256 + (rd_raw m a)
end.
Definition rd_int (m:memory) (a:Z) := unsigned_to_signed_64 (rd_bytes m a 8).
Variable rd_str : memory -> Z -> string.
Definition wr_raw (m:memory) (a:Z) (v:Z) := (a,v) :: m.
(* Write bytes into memory *)
Fixpoint wr_bytes (m:memory) (a:Z) (v:Z) (i:nat) :=
match i with
| O => m
| S p => wr_bytes (wr_raw m a (v mod 256)) (a+1) (v / 256) p
end.
Definition wr_int (m:memory) (a:Z) (v:Z) := wr_bytes m (signed_to_unsigned_64 a) v 8.
Definition scope : Set := string -> Z.
Inductive flag : Type :=
| Xbrk | Xret | Xcnt | Xnil | Exc (e:string).
Definition state : Set := (scope * memory * flag * Z).
(* Evaluation of expressions *)
Inductive eval_expr : state -> expr -> state -> Prop :=
| var : forall rho mu v x, eval_expr (rho,mu,Xnil,v) (VAR x) (rho,mu,Xnil,rd_int mu (rho x))
| var_chi : forall rho mu chi v x, chi <> Xnil
-> eval_expr (rho,mu,chi,v) (VAR x) (rho,mu,chi,v)
| cst : forall rho mu v n, eval_expr (rho,mu,Xnil,v) (CST n) (rho,mu,Xnil,n)
| cst_chi : forall rho mu chi v n, chi <> Xnil
-> eval_expr (rho,mu,chi,v) (CST n) (rho,mu,chi,v)
| str : forall rho mu v s a, rd_str mu a = s
-> eval_expr (rho,mu,Xnil,v) (STRING s) (rho,mu,Xnil,a)
| str_chi : forall rho mu chi v s, chi <> Xnil
-> eval_expr (rho,mu,chi,v) (STRING s) (rho,mu,chi,v)
| idx : forall rho mu chi v i mu_i chi_i v_i a mu' v_a,
eval_expr (rho,mu,chi,v) i (rho,mu_i,chi_i,v_i)
/\ eval_expr (rho,mu_i,chi_i,v_i) a (rho,mu',Xnil,v_a)
-> eval_expr (rho,mu,chi,v) (OP2 S_INDEX a i) (rho,mu',Xnil,rd_int mu' (v_a + v_i * 8))
| neg : forall rho mu chi v e mu_e v_e,
eval_expr (rho,mu,chi,v) e (rho,mu_e,Xnil,v_e)
-> eval_expr (rho,mu,chi,v) (OP1 M_MINUS e) (rho,mu_e,Xnil,-v_e)
| not : forall rho mu chi v e mu_e v_e,
eval_expr (rho,mu,chi,v) (OP1 M_NOT e) (rho,mu_e,Xnil,-v_e-1)
| var_ref : forall rho mu v x, eval_expr (rho,mu,Xnil,v) (OP1 M_ADDR (VAR x)) (rho,mu,Xnil,rho x)
| idx_ref : forall rho mu chi v i mu_i chi_i v_i a mu_a v_a,
eval_expr (rho,mu,chi,v) i (rho,mu_i,chi_i,v_i)
/\ eval_expr (rho,mu_i,chi_i,v_i) a (rho,mu_a,Xnil,v_a)
-> eval_expr (rho,mu,chi,v) (OP1 M_ADDR (OP2 S_INDEX a i)) (rho,mu_a,Xnil,v_a+v_i*8).
Lemma one : forall rho mu v, eval_expr (rho,mu,Xnil,v) (CST 1) (rho,mu,Xnil,1).
Proof.
intros.
apply cst.
Qed.