diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 09:30:53 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 09:30:53 +0200 |
| commit | 25e3a0643d99248e479b7d18f3dfcbb9bbc35d83 (patch) | |
| tree | 168c0018da1ca0461841c56929cf884b54806b9e /backend/CSEdomain.v | |
| parent | e188b6c4a1c43fb83157670e1c28db5798f50f0b (diff) | |
| download | compcert-kvx-25e3a0643d99248e479b7d18f3dfcbb9bbc35d83.tar.gz compcert-kvx-25e3a0643d99248e479b7d18f3dfcbb9bbc35d83.zip | |
CSEproof for non trapping loads
Diffstat (limited to 'backend/CSEdomain.v')
| -rw-r--r-- | backend/CSEdomain.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index 26d9c481..34ec0118 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -32,7 +32,7 @@ Definition valnum := positive. Inductive rhs : Type := | Op: operation -> list valnum -> rhs - | Load: trapping_mode -> memory_chunk -> addressing -> list valnum -> rhs. + | Load: memory_chunk -> addressing -> list valnum -> rhs. Inductive equation : Type := | Eq (v: valnum) (strict: bool) (r: rhs). @@ -74,7 +74,7 @@ Definition empty_numbering := Definition valnums_rhs (r: rhs): list valnum := match r with | Op op vl => vl - | Load trap chunk addr vl => vl + | Load chunk addr vl => vl end. Definition wf_rhs (next: valnum) (r: rhs) : Prop := @@ -106,11 +106,11 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): | op_eval_to: forall op vl v, eval_operation ge sp op (map valu vl) m = Some v -> rhs_eval_to valu ge sp m (Op op vl) v - | load_eval_to: forall trap chunk addr vl a v, + | load_eval_to: forall chunk addr vl a v, eval_addressing ge sp addr (map valu vl) = Some a -> Mem.loadv chunk m a = Some v -> - rhs_eval_to valu ge sp m (Load trap chunk addr vl) v - | load_notrap1_eval_to: forall chunk addr vl, + rhs_eval_to valu ge sp m (Load chunk addr vl) v +(* | load_notrap1_eval_to: forall chunk addr vl, eval_addressing ge sp addr (map valu vl) = None -> rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) (default_notrap_load_value chunk) @@ -118,7 +118,7 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem): eval_addressing ge sp addr (map valu vl) = Some a -> Mem.loadv chunk m a = None -> rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl) - (default_notrap_load_value chunk). + (default_notrap_load_value chunk) *). Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem): equation -> Prop := |