From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 45 +++++++++++++-------------------------------- 1 file changed, 13 insertions(+), 32 deletions(-) (limited to 'backend/Cminor.v') diff --git a/backend/Cminor.v b/backend/Cminor.v index 16f7c3df..35bf3916 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -103,7 +103,6 @@ Inductive stmt : Set := | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt | Stailcall: signature -> expr -> list expr -> stmt - | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -251,8 +250,11 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := Definition eval_compare_mismatch (c: comparison) : option val := match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end. +Definition eval_compare_null (c: comparison) (n: int) : option val := + if Int.eq n Int.zero then eval_compare_mismatch c else None. + Definition eval_binop - (op: binary_operation) (arg1 arg2: val) (m: mem): option val := + (op: binary_operation) (arg1 arg2: val): option val := match op, arg1, arg2 with | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1)) @@ -286,17 +288,13 @@ Definition eval_binop | Ocmp c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmp c n1 n2)) | Ocmp c, Vptr b1 n1, Vptr b2 n2 => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 - then Some(Val.of_bool(Int.cmp c n1 n2)) - else eval_compare_mismatch c - else - None + if eq_block b1 b2 + then Some(Val.of_bool(Int.cmp c n1 n2)) + else eval_compare_mismatch c | Ocmp c, Vptr b1 n1, Vint n2 => - if Int.eq n2 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n2 | Ocmp c, Vint n1, Vptr b2 n2 => - if Int.eq n1 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n1 | Ocmpu c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmpu c n1 n2)) | Ocmpf c, Vfloat f1, Vfloat f2 => @@ -332,7 +330,7 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Ebinop: forall op a1 a2 v1 v2 v, eval_expr a1 v1 -> eval_expr a2 v2 -> - eval_binop op v1 v2 m = Some v -> + eval_binop op v1 v2 = Some v -> eval_expr (Ebinop op a1 a2) v | eval_Eload: forall chunk addr vaddr v, eval_expr addr vaddr -> @@ -438,12 +436,6 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) - | step_alloc: forall f id a k sp e m n m' b, - eval_expr sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - step (State f (Salloc id a) k sp e m) - E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m') - | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) @@ -633,12 +625,6 @@ with exec_stmt: eval_funcall m f vargs t m' vres -> e' = set_optvar optid vres e -> exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal - | exec_Salloc: - forall sp e m id a n m' b, - eval_expr ge sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - exec_stmt sp e m (Salloc id a) - E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal | exec_Sifthenelse: forall sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> @@ -805,10 +791,10 @@ Definition eval_funcall_exec_stmt_ind2 (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) (P2: val -> env -> mem -> stmt -> trace -> env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q r => + fun a b c d e f g h i j k l m n o p q => conj - (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) - (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ). + (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) + (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). Inductive outcome_state_match (sp: val) (e: env) (m: mem) (f: function) (k: cont): @@ -918,11 +904,6 @@ Proof. constructor. reflexivity. traceEq. subst e'. constructor. -(* alloc *) - exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split. - apply star_one. econstructor; eauto. - constructor. - (* ifthenelse *) destruct (H2 f k) as [S [A B]]. exists S; split. -- cgit