From 25e3a0643d99248e479b7d18f3dfcbb9bbc35d83 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Sep 2019 09:30:53 +0200 Subject: CSEproof for non trapping loads --- backend/CSEdomain.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'backend/CSEdomain.v') 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 := -- cgit