From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- cfrontend/Cexec.v | 80 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 38 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 5c062158..952d148d 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -284,31 +284,31 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o end. Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop := - (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\ + (alignof_blockcopy ge ty | Int.unsigned ofs') /\ (alignof_blockcopy ge ty | Int.unsigned ofs) /\ (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'). + \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs + \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'). Remark check_assign_copy: forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. Proof with try (right; intuition omega). intros. unfold assign_copy_ok. - assert (alignof_blockcopy ty > 0) by apply alignof_blockcopy_pos. - destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto... - destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto... + assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos. + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto... + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto... assert (Y: {b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'} + + Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'} + {~(b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ty <= Int.unsigned ofs')}). + Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs')}). destruct (eq_block b' b); auto. destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs' + sizeof ty) (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto. + destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto. + destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto. right; intuition omega. destruct Y... left; intuition omega. Defined. @@ -324,7 +324,7 @@ Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v match v with | Vptr b' ofs' => if check_assign_copy ty b ofs b' ofs' then - do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty); + do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty); do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes; Some(w, E0, m') else None @@ -746,12 +746,14 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r with | Some(Vptr b ofs, ty') => match ty' with - | Tstruct id fList _ => - match field_offset f fList with + | Tstruct id _ => + do co <- ge.(genv_cenv)!id; + match field_offset ge f (co_members co) with | Error _ => stuck | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) end - | Tunion id fList _ => + | Tunion id _ => + do co <- ge.(genv_cenv)!id; topred (Lred (Eloc b ofs ty) m) | _ => stuck end @@ -787,7 +789,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ebinop op r1 r2 ty => match is_val r1, is_val r2 with | Some(v1, ty1), Some(v2, ty2) => - do v <- sem_binary_operation op v1 ty1 v2 ty2 m; + do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m; topred (Rred (Eval v ty) m E0) | _, _ => incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) @@ -828,9 +830,9 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end | RV, Esizeof ty' ty => - topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0) + topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) | RV, Ealignof ty' ty => - topred (Rred (Eval (Vint (Int.repr (alignof ty'))) ty) m E0) + topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) | RV, Eassign l1 r2 ty => match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => @@ -988,8 +990,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Efield (Eval v ty1) f ty => exists b, exists ofs, v = Vptr b ofs /\ match ty1 with - | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta - | Tunion _ _ _ => True + | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = OK delta + | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co | _ => False end | Eval v ty => False @@ -998,7 +1000,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Eunop op (Eval v1 ty1) ty => exists v, sem_unary_operation op v1 ty1 = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => - exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v + exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => @@ -1043,8 +1045,8 @@ Proof. exists b; auto. exists b; auto. exists b; exists ofs; auto. - exists b; exists ofs; split; auto. exists delta; auto. - exists b; exists ofs; auto. + exists b; exists ofs; split; auto. exists co, delta; auto. + exists b; exists ofs; split; auto. exists co; auto. Qed. Lemma rred_invert: @@ -1385,10 +1387,12 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct v... destruct ty'... (* top struct *) - destruct (field_offset f f0) as [delta|] eqn:?... - apply topred_ok; auto. apply red_field_struct; auto. + destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... + destruct (field_offset ge f (co_members co)) as [delta|] eqn:?... + apply topred_ok; auto. eapply red_field_struct; eauto. (* top union *) - apply topred_ok; auto. apply red_field_union; auto. + destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... + apply topred_ok; auto. eapply red_field_union; eauto. (* in depth *) eapply incontext_ok; eauto. (* Evalof *) @@ -1425,7 +1429,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val a2) as [[v2 ty2] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) - destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|] eqn:?... + destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?... apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor. (* depth *) eapply incontext2_ok; eauto. @@ -1589,9 +1593,9 @@ Proof. (* deref *) auto. (* field struct *) - rewrite H; auto. + rewrite H, H0; auto. (* field union *) - auto. + rewrite H; auto. Qed. Lemma rred_topred: @@ -1895,21 +1899,21 @@ Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l match l with | nil => (e,m) | (id, ty) :: l' => - let (m1,b1) := Mem.alloc m 0 (sizeof ty) in + let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in do_alloc_variables (PTree.set id (b1, ty) e) m1 l' end. Lemma do_alloc_variables_sound: - forall l e m, alloc_variables e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). + forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). Proof. induction l; intros; simpl. constructor. - destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1] eqn:?; simpl. + destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl. econstructor; eauto. Qed. Lemma do_alloc_variables_complete: - forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 -> + forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 -> do_alloc_variables e1 m1 l = (e2, m2). Proof. induction 1; simpl. @@ -1985,7 +1989,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m) | Kreturn k => do v' <- sem_cast v ty f.(fn_return); - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate v' (call_cont k) m') | Kswitch1 sl k => do n <- sem_switch_arg v ty; @@ -2024,11 +2028,11 @@ Definition do_step (w: world) (s: state) : list (trace * state) := | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m) | State f (Sreturn None) k e m => - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate Vundef (call_cont k) m') | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate Vundef k m') | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) @@ -2209,7 +2213,7 @@ End EXEC. Local Open Scope option_monad_scope. Definition do_initial_state (p: program): option (genv * state) := - let ge := Genv.globalenv p in + let ge := globalenv p in do m0 <- Genv.init_mem p; do b <- Genv.find_symbol ge p.(prog_main); do f <- Genv.find_funct_ptr ge b; -- cgit