diff options
43 files changed, 1349 insertions, 276 deletions
@@ -203,6 +203,8 @@ compcert.ini: Makefile.config VERSION echo "system=$(SYSTEM)"; \ echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ + echo "struct_passing_style=$(STRUCT_PASSING)"; \ + echo "struct_return_style=$(STRUCT_RETURN)"; \ version=`cat VERSION`; \ echo version=$$version) \ > compcert.ini diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 392959d4..d7b1e675 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -135,7 +135,7 @@ Proof. inv H. econstructor; eauto. (* default *) econstructor. constructor. eauto. constructor. - simpl. inv H0. auto. auto. + simpl. inv H0. auto. Qed. Lemma eval_load: diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 92004a2f..ff3ccfa1 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2121,12 +2121,14 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } unfold cmpu_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_different_blocks_none, pcmp_none, diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 47e876f7..fd10efb4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -199,6 +199,10 @@ let builtins_generic = { (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__compcert_va_composite", + (TPtr(TVoid [], []), + [TPtr(TVoid [], []); TInt(IUInt, [])], + false); (* Helper functions for int64 arithmetic *) "__i64_dtos", (TInt(ILongLong, []), @@ -381,26 +385,46 @@ let va_list_ptr e = | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr)) | _ -> error "bad use of a va_list object"; e -let make_builtin_va_arg env ty e = - let (helper, ty_ret) = - match ty with - | Tint _ | Tpointer _ -> - ("__compcert_va_int32", Tint(I32, Unsigned, noattr)) - | Tlong _ -> - ("__compcert_va_int64", Tlong(Unsigned, noattr)) - | Tfloat _ -> - ("__compcert_va_float64", Tfloat(F64, noattr)) - | _ -> - unsupported "va_arg at this type"; - ("", Tvoid) in +let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr e, Enil), + Econs(va_list_ptr arg, Enil), ty_ret), ty) +let make_builtin_va_arg_by_ref helper ty arg = + let ty_fun = + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tpointer(Tvoid, noattr), cc_default) in + let ty_ptr = + Tpointer(ty, noattr) in + let call = + Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), + Econs(va_list_ptr arg, + Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), + Tpointer(Tvoid, noattr)) in + Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) + +let make_builtin_va_arg env ty e = + match ty with + | Tint _ | Tpointer _ -> + make_builtin_va_arg_by_val + "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e + | Tlong _ -> + make_builtin_va_arg_by_val + "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e + | Tfloat _ -> + make_builtin_va_arg_by_val + "__compcert_va_float64" ty (Tfloat(F64, noattr)) e + | Tstruct _ | Tunion _ -> + make_builtin_va_arg_by_ref + "__compcert_va_composite" ty e + | _ -> + unsupported "va_arg at this type"; + Eval(Vint(coqint_of_camlint 0l), type_int32s) + (** ** Translation functions *) (** Constants *) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 66427b76..7c00ab47 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -785,7 +785,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eunop op r1 ty => match is_val r1 with | Some(v1, ty1) => - do v <- sem_unary_operation op v1 ty1; + do v <- sem_unary_operation op v1 ty1 m; topred (Rred "red_unop" (Eval v ty) m E0) | None => incontext (fun x => Eunop op x ty) (step_expr RV r1 m) @@ -810,7 +810,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqand r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0) else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0) | None => @@ -819,7 +819,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqor r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0) else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0) | None => @@ -828,7 +828,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Econdition r1 r2 r3 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) @@ -987,17 +987,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, exists w', deref_loc ge ty m b ofs t v /\ possible_trace w t w' | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => 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 => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, exists w', ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' @@ -1409,7 +1409,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* unop *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_unary_operation op v ty') as [v'|] eqn:?... + destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1433,7 +1433,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqand *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor. (* depth *) @@ -1441,7 +1441,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqor *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor. (* depth *) @@ -1449,7 +1449,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* condition *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... + destruct (bool_val v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1973,20 +1973,20 @@ Definition do_step (w: world) (s: state) : list transition := match k with | Kdo k => ret "step_do_2" (State f Sskip k e m ) | Kifthenelse s1 s2 k => - do b <- bool_val v ty; + do b <- bool_val v ty m; ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_while_true" (State f s (Kwhile2 x s k) e m) else ret "step_while_false" (State f Sskip k e m) | Kdowhile2 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_dowhile_true" (State f (Sdowhile x s) k e m) else ret "step_dowhile_false" (State f Sskip k e m) | Kfor2 a2 a3 s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) else ret "step_for_false" (State f Sskip k e m) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 7a45b453..77511b2c 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -403,7 +403,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Eaddrof a ty) (Vptr loc ofs) | eval_Eunop: forall op a ty v1 v, eval_expr a v1 -> - sem_unary_operation op v1 (typeof a) = Some v -> + sem_unary_operation op v1 (typeof a) m = Some v -> eval_expr (Eunop op a ty) v | eval_Ebinop: forall op a1 a2 ty v1 v2 v, eval_expr a1 v1 -> @@ -620,7 +620,7 @@ Inductive step: state -> trace -> state -> Prop := | step_ifthenelse: forall f a s1 s2 k e le m v1 b, eval_expr e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> step (State f (Sifthenelse a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 5b092db7..ac8931e5 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -115,7 +115,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> t1 le1 m1 out | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> exec_stmt e le m (if b then s1 else s2) t le' m' out -> exec_stmt e le m (Sifthenelse a s1 s2) t le' m' out @@ -204,7 +204,7 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2) | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> execinf_stmt e le m (if b then s1 else s2) t -> execinf_stmt e le m (Sifthenelse a s1 s2) t | execinf_Sloop_body1: forall e le m s1 s2 t, diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4e572277..2a5d17bc 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) | _ => None end | cast_case_l2l => @@ -371,7 +370,7 @@ Definition classify_bool (ty: type) : classify_bool_cases := considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Definition bool_val (v: val) (t: type) : option bool := +Definition bool_val (v: val) (t: type) (m: mem) : option bool := match classify_bool t with | bool_case_i => match v with @@ -391,7 +390,7 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => Some true + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None | _ => None end | bool_case_l => @@ -406,7 +405,7 @@ Definition bool_val (v: val) (t: type) : option bool := (** *** Boolean negation *) -Definition sem_notbool (v: val) (ty: type) : option val := +Definition sem_notbool (v: val) (ty: type) (m: mem): option val := match classify_bool ty with | bool_case_i => match v with @@ -426,7 +425,7 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr _ _ => Some Vfalse + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None | _ => None end | bool_case_l => @@ -973,9 +972,9 @@ Definition sem_switch_arg (v: val) (ty: type): option Z := (** * Combined semantics of unary and binary operators *) Definition sem_unary_operation - (op: unary_operation) (v: val) (ty: type): option val := + (op: unary_operation) (v: val) (ty: type) (m: mem): option val := match op with - | Onotbool => sem_notbool v ty + | Onotbool => sem_notbool v ty m | Onotint => sem_notint v ty | Oneg => sem_neg v ty | Oabsfloat => sem_absfloat v ty @@ -1091,15 +1090,17 @@ Proof. - econstructor; eauto. Qed. -Lemma sem_unary_operation_inject: +Lemma sem_unary_operation_inj: forall op v1 ty v tv1, - sem_unary_operation op v1 ty = Some v -> + sem_unary_operation op v1 ty m = Some v -> val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. (* neg *) @@ -1265,18 +1266,31 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma bool_val_inject: +Lemma bool_val_inj: forall v ty b tv, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> val_inject f v tv -> - bool_val tv ty = Some b. + bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. - destruct (classify_bool ty); inv H0; congruence. + destruct (classify_bool ty); inv H0; try congruence. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. Qed. End GENERIC_INJECTION. +Lemma sem_unary_operation_inject: + forall f m m' op v1 ty1 v tv1, + sem_unary_operation op v1 ty1 m = Some v -> + val_inject f v1 tv1 -> + Mem.inject f m m' -> + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. +Proof. + intros. eapply sem_unary_operation_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> @@ -1291,6 +1305,17 @@ Proof. intros; eapply Mem.different_pointers_inject; eauto. Qed. +Lemma bool_val_inject: + forall f m m' v ty b tv, + bool_val v ty m = Some b -> + val_inject f v tv -> + Mem.inject f m m' -> + bool_val tv ty m' = Some b. +Proof. + intros. eapply bool_val_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + (** * Some properties of operator semantics *) (** This section collects some common-sense properties about the type @@ -1301,9 +1326,12 @@ Qed. (** Relation between Boolean value and casting to [_Bool] type. *) Lemma cast_bool_bool_val: - forall v t, - sem_cast v t (Tint IBool Signed noattr) = - match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. + forall v t m, + match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with + | Some v', Some b => v' = Val.of_bool b + | Some v', None => False + | None, _ => True + end. Proof. intros. assert (A: classify_bool t = @@ -1337,12 +1365,13 @@ Qed. (** Relation between Boolean value and Boolean negation. *) Lemma notbool_bool_val: - forall v t, - sem_notbool v t = - match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. + forall v t m, + sem_notbool v t m = + match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. + destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index fafbf29f..3e9017c9 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -241,7 +241,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Eaddrof (Eloc b ofs ty1) ty) m E0 (Eval (Vptr b ofs) ty) m | red_unop: forall op v1 ty1 ty m v, - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> rred (Eunop op (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_binop: forall op v1 ty1 v2 ty2 ty m v, @@ -253,23 +253,23 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ecast (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_seqand_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_seqand_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.zero) ty) m | red_seqor_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.one) ty) m | red_seqor_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_condition: forall v1 ty1 r1 r2 ty b m, - bool_val v1 ty1 = Some b -> + bool_val v1 ty1 m = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, @@ -633,7 +633,7 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sifthenelse a s1 s2) k e m) E0 (ExprState f a (Kifthenelse s1 s2 k) e m) | step_ifthenelse_2: forall f v ty s1 s2 k e m b, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m) E0 (State f (if b then s1 else s2) k e m) @@ -641,11 +641,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Swhile x s) k e m) E0 (ExprState f x (Kwhile1 x s k) e m) | step_while_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f Sskip k e m) | step_while_true: forall f v ty x s k e m , - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f s (Kwhile2 x s k) e m) | step_skip_or_continue_while: forall f s0 x s k e m, @@ -664,11 +664,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f s0 (Kdowhile1 x s k) e m) E0 (ExprState f x (Kdowhile2 x s k) e m) | step_dowhile_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f Sskip k e m) | step_dowhile_true: forall f v ty x s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f (Sdowhile x s) k e m) | step_break_dowhile: forall f a s k e m, @@ -683,11 +683,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sfor Sskip a2 a3 s) k e m) E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m) | step_for_false: forall f v ty a2 a3 s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f Sskip k e m) | step_for_true: forall f v ty a2 a3 s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f s (Kfor3 a2 a3 s k) e m) | step_skip_or_continue_for3: forall f x a2 a3 s k e m, diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..025d7b66 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -311,7 +311,7 @@ Qed. Lemma make_boolean_correct: forall e le m a v ty b, eval_expr ge e le m a v -> - bool_val v ty = Some b -> + bool_val v ty m = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. @@ -333,7 +333,10 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. + unfold Val.cmpu, Val.cmpu_bool. simpl. + unfold Mem.weak_valid_pointer in V; rewrite V. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. @@ -366,13 +369,16 @@ Qed. Lemma make_notbool_correct: forall a tya c va v e le m, - sem_notbool va tya = Some v -> + sem_notbool va tya m = Some v -> make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V; rewrite V. auto. Qed. Lemma make_notint_correct: @@ -633,7 +639,7 @@ Qed. Lemma transl_unop_correct: forall op a tya c va v e le m, transl_unop op a tya = OK c -> - sem_unary_operation op va tya = Some v -> + sem_unary_operation op va tya m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3b0eb84f..b082ea56 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -122,7 +122,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -249,33 +249,33 @@ Inductive estep: state -> trace -> state -> Prop := | step_seqand_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_seqand_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m) | step_seqor_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m) | step_seqor_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some b -> + bool_val v (typeof r1) m = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m) @@ -536,17 +536,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => 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 => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' @@ -1695,27 +1695,27 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m RV (Eseqor a1 a2 ty) t1 m' (Eval (Vint Int.one) ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) @@ -1801,7 +1801,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := t1 m1 out | exec_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 m2 b out, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> exec_stmt e m1 (if b then s1 else s2) t2 m2 out -> exec_stmt e m (Sifthenelse a s1 s2) (t1**t2) m2 out @@ -1820,19 +1820,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := E0 m Out_continue | exec_Swhile_false: forall e m a s t m' v, eval_expression e m a t m' v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m' = Some false -> exec_stmt e m (Swhile a s) t m' Out_normal | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) (t1**t2) m2 out | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 (Swhile a s) t3 m3 out -> @@ -1842,7 +1842,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m2 = Some false -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, @@ -1854,7 +1854,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out @@ -1865,19 +1865,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> - bool_val v (typeof a2) = Some false -> + bool_val v (typeof a2) m' = Some false -> exec_stmt e m (Sfor Sskip a2 a3 s) t m' Out_normal | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1952,7 +1952,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqand a1 a2 ty) t1 | evalinf_seqand_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqand a1 a2 ty) (t1***t2) | evalinf_seqor: forall e m a1 a2 ty t1, @@ -1960,7 +1960,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqor a1 a2 ty) t1 | evalinf_seqor_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqor a1 a2 ty) (t1***t2) | evalinf_condition: forall e m a1 a2 a3 ty t1, @@ -1968,7 +1968,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) | evalinf_assign_left: forall e m a1 t1 a2 ty, @@ -2039,7 +2039,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sifthenelse a s1 s2) t1 | execinf_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 b, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> execinf_stmt e m1 (if b then s1 else s2) t2 -> execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) | execinf_Sreturn_some: forall e m a t, @@ -2050,12 +2050,12 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Swhile a s) t1 | execinf_Swhile_body: forall e m a s t1 m1 v t2, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Swhile a s) (t1***t2) | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 (Swhile a s) t3 -> @@ -2072,7 +2072,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> execinf_stmt e m2 (Sdowhile a s) t3 -> execinf_stmt e m (Sdowhile a s) (t1***t2***t3) | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, @@ -2087,19 +2087,19 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 a3 t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 43d34007..2582fff8 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1376,9 +1376,9 @@ Proof. Qed. Lemma pres_sem_unop: - forall op ty1 ty v1 v, + forall op ty1 ty v1 m v, type_unop op ty1 = OK ty -> - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> wt_val v1 ty1 -> wt_val v ty. Proof. @@ -1390,7 +1390,7 @@ Proof. destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. destruct (Int.eq i Int.zero); constructor; auto with ty. - constructor; auto with ty. + constructor. constructor. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 025960d7..7af4792a 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -74,7 +74,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := constval ce l | Eunop op r1 ty => do v1 <- constval ce r1; - match sem_unary_operation op v1 (typeof r1) with + match sem_unary_operation op v1 (typeof r1) Mem.empty with | Some v => OK v | None => Error(msg "undefined unary operation") end @@ -94,7 +94,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqand r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") @@ -102,7 +102,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqor r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") @@ -111,7 +111,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do v1 <- constval ce r1; do v2 <- constval ce r2; do v3 <- constval ce r3; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) ty | Some false => do_cast v3 (typeof r3) ty | None => Error(msg "condition is undefined") diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 02a453cf..e0fcb210 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -112,7 +112,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -127,23 +127,23 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_alignof: forall ty1 ty, eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero) | esr_seqor_false: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) | esr_condition: forall r1 r2 r3 ty v v1 b v', - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some b -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v @@ -366,6 +366,15 @@ Proof. intros [v' [A B]]. congruence. Qed. +Lemma bool_val_match: + forall v ty b v' m, + bool_val v ty Mem.empty = Some b -> + val_inject inj v v' -> + bool_val v' ty m = Some b. +Proof. + intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. +Qed. + (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -390,8 +399,10 @@ Proof. (* addrof *) eauto. (* unop *) - destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0. - exploit sem_unary_operation_inject. eexact E. eauto. + destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0. + exploit (sem_unary_operation_inj inj Mem.empty m). + intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. + eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. @@ -409,24 +420,24 @@ Proof. (* alignof *) constructor. (* seqand *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) - destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b' = b) by congruence. subst b'. destruct b; eapply sem_cast_match; eauto. (* comma *) diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ebd06c54..f1c3ef18 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -206,7 +206,7 @@ and print_cases p cases = and print_case_label p = function | None -> fprintf p "default" - | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + | Some lbl -> fprintf p "case %s" (Z.to_string lbl) and print_stmt_for p s = match s with diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 8a4d60a5..882272b8 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -346,7 +346,7 @@ and print_cases p cases = and print_case_label p = function | None -> fprintf p "default" - | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + | Some lbl -> fprintf p "case %s" (Z.to_string lbl) and print_stmt_for p s = match s with diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 36fe07ae..097dc589 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -18,6 +18,7 @@ Require Import Errors. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Memory. Require Import AST. Require Import Ctypes. Require Import Cop. @@ -129,7 +130,7 @@ Function eval_simpl_expr (a: expr) : option val := Function makeif (a: expr) (s1 s2: statement) : statement := match eval_simpl_expr a with | Some v => - match bool_val v (typeof a) with + match bool_val v (typeof a) Mem.empty with | Some b => if b then s1 else s2 | None => Sifthenelse a s1 s2 end diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 74019061..7ef1cbe2 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -761,20 +761,30 @@ Proof. inv H; simpl; auto. Qed. +Lemma static_bool_val_sound: + forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b. +Proof. + intros until b; unfold bool_val. destruct (classify_bool t); destruct v; auto. + intros E. unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool in E. + rewrite ! pred_dec_false in E by (apply Mem.perm_empty). discriminate. +Qed. + Lemma step_makeif: forall f a s1 s2 k e le m v1 b, eval_expr tge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> star step1 tge (State f (makeif a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m). Proof. intros. functional induction (makeif a s1 s2). - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - apply star_one. eapply step_ifthenelse; eauto. - apply star_one. eapply step_ifthenelse; eauto. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some true) by (apply static_bool_val_sound; auto). + replace b with true by congruence. constructor. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some false) by (apply static_bool_val_sound; auto). + replace b with false by congruence. constructor. +- apply star_one. eapply step_ifthenelse; eauto. +- apply star_one. eapply step_ifthenelse; eauto. Qed. Lemma step_make_set: diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 5cf59d94..3364ec6a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -267,11 +267,8 @@ Proof. constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. diff --git a/common/Values.v b/common/Values.v index 984da4ed..12b380b7 100644 --- a/common/Values.v +++ b/common/Values.v @@ -111,15 +111,13 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. -(** Truth values. Pointers and non-zero integers are treated as [True]. +(** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. - [Vundef] and floats are neither true nor false. *) + Other values are neither true nor false. *) Inductive bool_of_val: val -> bool -> Prop := | bool_of_val_int: - forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)) - | bool_of_val_ptr: - forall b ofs, bool_of_val (Vptr b ofs) true. + forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)). (** Arithmetic operations *) @@ -695,7 +693,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2) | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero then cmp_different_blocks c else None + if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2) + then cmp_different_blocks c + else None | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then if weak_valid_ptr b1 (Int.unsigned ofs1) @@ -708,7 +708,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := then cmp_different_blocks c else None | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero then cmp_different_blocks c else None + if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1) + then cmp_different_blocks c + else None | _, _ => None end. @@ -1175,8 +1177,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.negate_cmpu. auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0). destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). @@ -1222,8 +1224,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.swap_cmpu. auto. - case (Int.eq i Int.zero); auto. - case (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0); subst. rewrite dec_eq_true. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); @@ -1429,19 +1431,23 @@ Lemma cmpu_bool_lessdef: cmpu_bool valid_ptr' c v1' v2' = Some b. Proof. intros. + assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> + valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). + { intros until ofs. rewrite ! orb_true_iff. intuition. } destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. + destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. destruct (eq_block b0 b1). - assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> - valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). - intros until ofs. rewrite ! orb_true_iff. intuition. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate. - erewrite !H0 by eauto. auto. + erewrite ! A by eauto. auto. destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. - erewrite !H by eauto. auto. + erewrite ! H by eauto. auto. Qed. Lemma of_optbool_lessdef: @@ -1605,7 +1611,17 @@ Lemma val_cmpu_bool_inject: Proof. Local Opaque Int.add. intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). @@ -64,9 +64,9 @@ while : ; do -toolprefix|--toolprefix) toolprefix="$2"; shift;; -no-runtime-lib) - has_runtime_lib=false; shift;; + has_runtime_lib=false;; -no-checklink) - build_checklink=false; shift;; + build_checklink=false;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -79,12 +79,19 @@ done cchecklink=false casmruntime="" asm_supports_cfi="" +struct_passing="" +struct_return="" case "$target" in powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi) arch="powerpc" model="standard" abi="eabi" + struct_passing="ref-caller" + case "$target" in + *-linux) struct_return="ref";; + *-eabi) struct_return="int1-8";; + esac system="linux" cc="${toolprefix}gcc" cprepro="${toolprefix}gcc -U__GNUC__ -E" @@ -97,6 +104,8 @@ case "$target" in arch="powerpc" model="standard" abi="eabi" + struct_passing="ref-caller" + struct_return="int1-8" system="diab" cc="${toolprefix}dcc" cprepro="${toolprefix}dcc -E" @@ -125,6 +134,8 @@ case "$target" in echo "$usage" 1>&2 exit 2;; esac + struct_passing="ints" + struct_return="int1-4" system="linux" cc="${toolprefix}gcc" cprepro="${toolprefix}gcc -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" @@ -135,6 +146,8 @@ case "$target" in arch="ia32" model="sse2" abi="standard" + struct_passing="ints" + struct_return="ref" system="linux" cc="${toolprefix}gcc -m32" cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" @@ -145,6 +158,8 @@ case "$target" in arch="ia32" model="sse2" abi="standard" + struct_passing="ints" + struct_return="int1248" # to check! system="bsd" cc="${toolprefix}gcc -m32" cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" @@ -154,7 +169,9 @@ case "$target" in ia32-macosx) arch="ia32" model="sse2" - abi="standard" + abi="macosx" + struct_passing="ints" + struct_return="int1248" system="macosx" cc="${toolprefix}gcc -arch i386" cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" @@ -170,6 +187,8 @@ case "$target" in arch="ia32" model="sse2" abi="standard" + struct_passing="ints" + struct_return="ref" system="cygwin" cc="${toolprefix}gcc -m32" cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" @@ -326,6 +345,8 @@ cat >> Makefile.config <<EOF ARCH=$arch MODEL=$model ABI=$abi +STRUCT_PASSING=$struct_passing +STRUCT_RETURN=$struct_return SYSTEM=$system CC=$cc CPREPRO=$cprepro @@ -362,9 +383,19 @@ MODEL= # ABI=standard # for IA32 ABI= +# Default calling conventions for passing structs and unions by value +# See options -fstruct-passing=<style> and -fstruct-return=<style> +# in the CompCert user's manual +STRUCT_PASSING=ref_callee +# STRUCT_PASSING=ref_caller +# STRUCT_PASSING=ints +STRUCT_RETURN=ref +# STRUCT_RETURN=int1248 +# STRUCT_RETURN=int1-4 +# STRUCT_RETURN=int1-8 + # Target operating system and development environment # Possible choices for PowerPC: -# SYSTEM=macosx # SYSTEM=linux # SYSTEM=diab # Possible choices for ARM: @@ -425,6 +456,7 @@ CompCert configuration: Target architecture........... $arch Hardware model................ $model Application binary interface.. $abi + Composite passing conventions. arguments: $struct_passing, return values: $struct_return OS and development env........ $system C compiler.................... $cc C preprocessor................ $cprepro diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 9e7f102e..4d6d2137 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -834,9 +834,23 @@ let nullconst = ecast (TPtr(TVoid [], [])) (intconst 0L IInt) let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp } -(* Construct a "," expression *) +(* Construct a "," expression. Reassociate to the left so that + it prints more nicely. *) -let ecomma e1 e2 = { edesc = EBinop(Ocomma, e1, e2, e2.etyp); etyp = e2.etyp } +let rec ecomma e1 e2 = + match e2.edesc with + | EBinop(Ocomma, e2', e2'', _) -> + ecomma (ecomma e1 e2') e2'' + | _ -> + { edesc = EBinop(Ocomma, e1, e2, e2.etyp); etyp = e2.etyp } + +(* Construct a cascade of "," expressions. + Associate to the left so that it prints more nicely. *) + +let ecommalist el e = + match el with + | [] -> e + | e1 :: el -> ecomma (List.fold_left ecomma e1 el) e (* Construct an address-of expression. Can be applied not just to an l-value but also to a sequence or a conditional of l-values. *) @@ -910,3 +924,65 @@ let rec default_init env ty = end | _ -> assert false + +(* Substitution of variables by expressions *) + +let rec subst_expr phi e = + match e.edesc with + | EConst _ | ESizeof _ | EAlignof _ -> e + | EVar x -> + begin try IdentMap.find x phi with Not_found -> e end + | EUnop(op, e1) -> + { e with edesc = EUnop(op, subst_expr phi e1) } + | EBinop(op, e1, e2, ty) -> + { e with edesc = EBinop(op, subst_expr phi e1, subst_expr phi e2, ty) } + | EConditional(e1, e2, e3) -> + { e with edesc = + EConditional(subst_expr phi e1, subst_expr phi e2, subst_expr phi e3) } + | ECast(ty, e1) -> + { e with edesc = ECast(ty, subst_expr phi e1) } + | ECompound(ty, i) -> + { e with edesc = ECompound(ty, subst_init phi i) } + | ECall(e1, el) -> + { e with edesc = ECall(subst_expr phi e1, List.map (subst_expr phi) el) } + +and subst_init phi = function + | Init_single e -> Init_single (subst_expr phi e) + | Init_array il -> Init_array (List.map (subst_init phi) il) + | Init_struct(name, fl) -> + Init_struct(name, List.map (fun (f,i) -> (f, subst_init phi i)) fl) + | Init_union(name, f, i) -> + Init_union(name, f, subst_init phi i) + +let subst_decl phi (sto, name, ty, optinit) = + (sto, name, ty, + match optinit with None -> None | Some i -> Some (subst_init phi i)) + +let rec subst_stmt phi s = + { s with sdesc = + match s.sdesc with + | Sskip + | Sbreak + | Scontinue + | Sgoto _ + | Sasm _ -> s.sdesc + | Sdo e -> Sdo (subst_expr phi e) + | Sseq(s1, s2) -> Sseq (subst_stmt phi s1, subst_stmt phi s2) + | Sif(e, s1, s2) -> + Sif (subst_expr phi e, subst_stmt phi s1, subst_stmt phi s2) + | Swhile(e, s1) -> Swhile (subst_expr phi e, subst_stmt phi s1) + | Sdowhile(s1, e) -> Sdowhile (subst_stmt phi s1, subst_expr phi e) + | Sfor(s1, e, s2, s3) -> + Sfor (subst_stmt phi s1, subst_expr phi e, + subst_stmt phi s2, subst_stmt phi s3) + | Sswitch(e, s1) -> Sswitch (subst_expr phi e, subst_stmt phi s1) + | Slabeled(l, s1) -> Slabeled (l, subst_stmt phi s1) + | Sreturn None -> s.sdesc + | Sreturn (Some e) -> Sreturn (Some (subst_expr phi e)) + | Sblock sl -> Sblock (List.map (subst_stmt phi) sl) + | Sdecl d -> Sdecl (subst_decl phi d) + } + + + + diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b90dc897..deee9f08 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -210,6 +210,8 @@ val eassign : exp -> exp -> exp (* Expression for [e1 = e2] *) val ecomma : exp -> exp -> exp (* Expression for [e1, e2] *) +val ecommalist : exp list -> exp -> exp + (* Expression for [e1, ..., eN, e] *) val sskip: stmt (* The [skip] statement. No location. *) val sseq : location -> stmt -> stmt -> stmt @@ -232,3 +234,10 @@ val formatloc: Format.formatter -> location -> unit val default_init: Env.t -> typ -> init (* Return a default initializer for the given type (with zero numbers, null pointers, etc). *) + +(* Substitution of variables by expressions *) + +val subst_expr: exp IdentMap.t -> exp -> exp +val subst_init: exp IdentMap.t -> init -> init +val subst_decl: exp IdentMap.t -> decl -> decl +val subst_stmt: exp IdentMap.t -> stmt -> stmt diff --git a/cparser/Machine.ml b/cparser/Machine.ml index b215505b..bd6489fd 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -44,7 +44,7 @@ type t = { alignof_fun: int option; bigendian: bool; bitfields_msb_first: bool; - struct_return_as_int: int + supports_unaligned_accesses: bool } let ilp32ll64 = { @@ -76,7 +76,7 @@ let ilp32ll64 = { alignof_fun = None; bigendian = false; bitfields_msb_first = false; - struct_return_as_int = 0 + supports_unaligned_accesses = false } let i32lpll64 = { @@ -108,7 +108,7 @@ let i32lpll64 = { alignof_fun = None; bigendian = false; bitfields_msb_first = false; - struct_return_as_int = 0 + supports_unaligned_accesses = false } let il32pll64 = { @@ -140,7 +140,7 @@ let il32pll64 = { alignof_fun = None; bigendian = false; bitfields_msb_first = false; - struct_return_as_int = 0 + supports_unaligned_accesses = false } (* Canned configurations for some ABIs *) @@ -149,9 +149,15 @@ let x86_32 = { ilp32ll64 with name = "x86_32"; char_signed = true; alignof_longlong = 4; alignof_double = 4; - sizeof_longdouble = 12; alignof_longdouble = 4 } + sizeof_longdouble = 12; alignof_longdouble = 4; + supports_unaligned_accesses = true } + +let x86_32_macosx = + { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16 } + let x86_64 = { i32lpll64 with name = "x86_64"; char_signed = true } + let win32 = { ilp32ll64 with name = "win32"; char_signed = true; sizeof_wchar = 2; wchar_signed = false } @@ -162,10 +168,10 @@ let ppc_32_bigendian = { ilp32ll64 with name = "powerpc"; bigendian = true; bitfields_msb_first = true; - struct_return_as_int = 8 } + supports_unaligned_accesses = true } + let arm_littleendian = - { ilp32ll64 with name = "arm"; - struct_return_as_int = 4 } + { ilp32ll64 with name = "arm" } (* Add GCC extensions re: sizeof and alignof *) @@ -173,6 +179,12 @@ let gcc_extensions c = { c with sizeof_void = Some 1; sizeof_fun = Some 1; alignof_void = Some 1; alignof_fun = Some 1 } +(* Normalize configuration for use with the CompCert reference interpreter *) + +let compcert_interpreter c = + { c with sizeof_longdouble = 8; alignof_longdouble = 8; + supports_unaligned_accesses = false } + (* Undefined configuration *) let undef = { @@ -204,7 +216,7 @@ let undef = { alignof_fun = None; bigendian = false; bitfields_msb_first = false; - struct_return_as_int = 0 + supports_unaligned_accesses = false } (* The current configuration. Must be initialized before use. *) diff --git a/cparser/Machine.mli b/cparser/Machine.mli index b544711f..fb7321f9 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -44,13 +44,20 @@ type t = { alignof_fun: int option; bigendian: bool; bitfields_msb_first: bool; - struct_return_as_int: int + supports_unaligned_accesses: bool } +(* The current configuration *) + +val config : t ref + +(* Canned configurations *) + val ilp32ll64 : t val i32lpll64 : t val il32pll64 : t val x86_32 : t +val x86_32_macosx : t val x86_64 : t val win32 : t val win64 : t @@ -58,5 +65,4 @@ val ppc_32_bigendian : t val arm_littleendian : t val gcc_extensions : t -> t - -val config : t ref +val compcert_interpreter : t -> t diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 228cc530..8bfc6954 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -13,37 +13,198 @@ (* *) (* *********************************************************************) -(* Eliminate structs and unions being returned by value as function results *) +(* Eliminate structs and unions that are + - returned by value as function results + - passed by value as function parameters. *) open Machine +open Configuration open C open Cutil open Transform +let struct_return_style = ref SR_ref +let struct_passing_style = ref SP_ref_callee + (* Classification of function return types. *) type return_kind = | Ret_scalar (**r a scalar type, returned as usual *) | Ret_ref (**r a composite type, returned by reference *) - | Ret_value of typ (**r a small composite type, returned as an integer *) + | Ret_value of typ * int * int + (**r a small composite type, returned as an integer + (type, size, alignment) *) let classify_return env ty = if is_composite_type env ty then begin - match sizeof env ty with - | None -> Ret_ref (* should not happen *) - | Some sz -> - if (!config).struct_return_as_int >= 4 && sz <= 4 then - Ret_value (TInt(IUInt, [])) - else if (!config).struct_return_as_int >= 8 && sz <= 8 then - Ret_value (TInt(IULongLong, [])) - else Ret_ref + match sizeof env ty, alignof env ty with + | Some sz, Some al -> + begin match !struct_return_style with + | SR_int1248 when sz = 1 || sz = 2 || sz = 4 -> + Ret_value (TInt(IUInt, []), sz, al) + | SR_int1248 when sz = 8 -> + Ret_value (TInt(IULongLong, []), sz, al) + | (SR_int1to4 | SR_int1to8) when sz <= 4 -> + Ret_value (TInt(IUInt, []), sz, al) + | SR_int1to8 when sz > 4 && sz <= 8 -> + Ret_value (TInt(IULongLong, []), sz, al) + | _ -> + Ret_ref + end + | _, _ -> + Ret_ref (* should not happen *) end else Ret_scalar -(* Rewriting of function types. +(* Classification of function parameter types. *) + +type param_kind = + | Param_unchanged (**r passed as is *) + | Param_ref_caller (**r passed by reference to a copy taken by the caller *) + | Param_flattened of int * int * int (**r passed as N integer arguments *) + (**r (N, size, alignment) *) + +let classify_param env ty = + if is_composite_type env ty then begin + match !struct_passing_style with + | SP_ref_callee -> Param_unchanged + | SP_ref_caller -> Param_ref_caller + | _ -> + match sizeof env ty, alignof env ty with + | Some sz, Some al -> + Param_flattened ((sz + 3) / 4, sz, al) + | _, _ -> + Param_unchanged (* should not happen *) + end else + Param_unchanged + +(* Return the list [f 0; f 1; ...; f (n-1)] *) + +let list_map_n f n = + let rec map i = if i >= n then [] else f i :: map (i + 1) + in map 0 + +(* Declaring and accessing buffers (arrays of int) *) + +let uchar = TInt(IUChar, []) +let ushort = TInt(IUShort, []) +let uint = TInt(IUInt, []) +let ulonglong = TInt(IULongLong, []) +let ucharptr = TPtr(uchar, []) +let ushortptr = TPtr(ushort, []) +let uintptr = TPtr(uint, []) +let ulonglongptr = TPtr(ulonglong, []) + +let ty_buffer n = + TArray(uint, Some (Int64.of_int n), []) + +let ebuffer_index base idx = + { edesc = EBinop(Oindex, base, intconst (Int64.of_int idx) IInt, uintptr); + etyp = uint } + +let attr_structret = [Attr("__structreturn", [])] + +(* Expression constructor functions *) + +let ereinterpret ty e = + { edesc = EUnop(Oderef, ecast (TPtr(ty, [])) (eaddrof e)); etyp = ty } + +let or2 a b = { edesc = EBinop(Oor, a, b, uint); etyp = uint } +let or3 a b c = or2 (or2 a b) c +let or4 a b c d = or2 (or2 (or2 a b) c) d + +let lshift a nbytes = + if nbytes = 0 then a else + { edesc = EBinop(Oshl, a, intconst (Int64.of_int (nbytes * 8)) IInt, uint); + etyp = uint } + +let offsetptr base ofs = + if ofs = 0 then base else + { edesc = EBinop(Oadd, base, intconst (Int64.of_int ofs) IInt, ucharptr); + etyp = ucharptr } + +let load1 base ofs shift_le shift_be = + let shift = if (!config).bigendian then shift_be else shift_le in + let a = offsetptr base ofs in + lshift { edesc = EUnop(Oderef, a); etyp = uchar } shift + +let load2 base ofs shift_le shift_be = + let shift = if (!config).bigendian then shift_be else shift_le in + let a = ecast ushortptr (offsetptr base ofs) in + lshift { edesc = EUnop(Oderef, a); etyp = ushort } shift + +let load4 base ofs = + let a = ecast uintptr (offsetptr base ofs) in + { edesc = EUnop(Oderef, a); etyp = uint } + +let load8 base ofs = + let a = ecast ulonglongptr (offsetptr base ofs) in + { edesc = EUnop(Oderef, a); etyp = ulonglong } + +let lshift_ll a nbytes = + let a = ecast ulonglong a in + if nbytes = 0 then a else + { edesc = EBinop(Oshl, a, intconst (Int64.of_int (nbytes * 8)) IInt, ulonglong); + etyp = ulonglong } + +let or2_ll a b = { edesc = EBinop(Oor, a, b, uint); etyp = ulonglong } + +(* Loading a memory area as one or several integers. *) + +let load_word base ofs sz al = + match sz with + | 0 -> intconst 0L IInt + | 1 -> load1 base ofs 0 3 + | 2 -> if al >= 2 || (!config).supports_unaligned_accesses then + load2 base ofs 0 2 + else + or2 (load1 base ofs 0 3) + (load1 base (ofs + 1) 1 2) + | 3 -> if al >= 2 || (!config).supports_unaligned_accesses then + or2 (load2 base ofs 0 2) + (load1 base (ofs + 2) 2 1) + else + or3 (load1 base ofs 0 3) + (load1 base (ofs + 1) 1 2) + (load1 base (ofs + 2) 2 1) + | 4 -> if al >= 4 || (!config).supports_unaligned_accesses then + load4 base ofs + else if al >= 2 then + or2 (load2 base ofs 0 2) + (load2 base (ofs + 2) 2 0) + else + or4 (load1 base ofs 0 3) + (load1 base (ofs + 1) 1 2) + (load1 base (ofs + 2) 2 1) + (load1 base (ofs + 3) 3 0) + | _ -> assert false + + +let rec load_words base ofs sz al = + if ofs >= sz then [] + else if ofs + 4 >= sz then [load_word base ofs (sz - ofs) al] + else load_word base ofs 4 al :: load_words base (ofs + 4) sz al + +let load_result base sz al = + assert (sz <= 8); + if sz <= 4 then + load_word base 0 sz al + else if sz = 8 && (al >= 8 || (!config).supports_unaligned_accesses) then + load8 base 0 + else begin + let (shift1, shift2) = if (!config).bigendian then (4, 0) else (0, 4) in + or2_ll (lshift_ll (load_word base 0 4 al) shift1) + (lshift_ll (load_word base 4 (sz - 4) al) shift2) + end + +(* Rewriting of function types. For the return type: return kind scalar -> no change return kind ref -> return type void + add 1st parameter struct s * return kind value(t) -> return type t. + For the parameters: + param unchanged -> no change + param_ref_caller -> turn into a pointer + param_flattened N -> turn into N parameters of type "int" Try to preserve original typedef names when no change. *) @@ -51,22 +212,25 @@ let rec transf_type env t = match unroll env t with | TFun(tres, None, vararg, attr) -> let tres' = transf_type env tres in - let tres'' = - match classify_return env tres with - | Ret_scalar -> tres' - | Ret_ref -> TVoid [] - | Ret_value ty -> ty in - TFun(tres'', None, vararg, attr) + begin match classify_return env tres with + | Ret_scalar -> + TFun(tres', None, vararg, attr) + | Ret_ref -> + TFun(TVoid [], None, vararg, add_attributes attr attr_structret) + | Ret_value(ty, sz, al) -> + TFun(ty, None, vararg, attr) + end | TFun(tres, Some args, vararg, attr) -> - let args' = List.map (transf_funarg env) args in + let args' = transf_funargs env args in let tres' = transf_type env tres in begin match classify_return env tres with | Ret_scalar -> TFun(tres', Some args', vararg, attr) | Ret_ref -> let res = Env.fresh_ident "_res" in - TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr) - | Ret_value ty -> + TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, + add_attributes attr attr_structret) + | Ret_value(ty, sz, al) -> TFun(ty, Some args', vararg, attr) end | TPtr(t1, attr) -> @@ -77,12 +241,28 @@ let rec transf_type env t = if t1' = t1 then t else TArray(transf_type env t1, sz, attr) | _ -> t -and transf_funarg env (id, t) = (id, transf_type env t) +and transf_funargs env = function + | [] -> [] + | (id, t) :: args -> + let t' = transf_type env t in + let args' = transf_funargs env args in + match classify_param env t with + | Param_unchanged -> + (id, t') :: args' + | Param_ref_caller -> + (id, TPtr(t', [])) :: args' + | Param_flattened(n, sz, al) -> + list_map_n (fun _ -> (Env.fresh_ident id.name, uint)) n + @ args' (* Expressions: transform calls + rewrite the types *) -let ereinterpret ty e = - { edesc = EUnop(Oderef, ecast (TPtr(ty, [])) (eaddrof e)); etyp = ty } +let rec translates_to_extended_lvalue arg = + is_lvalue arg || + (match arg.edesc with + | ECall _ -> true + | EBinop(Ocomma, a, b, _) -> translates_to_extended_lvalue b + | _ -> false) let rec transf_expr env ctx e = let newty = transf_type env e.etyp in @@ -98,7 +278,7 @@ let rec transf_expr env ctx e = | EUnop(op, e1) -> {edesc = EUnop(op, transf_expr env Val e1); etyp = newty} | EBinop(Oassign, lhs, {edesc = ECall(fn, args); etyp = ty}, _) -> - transf_call env ctx (Some lhs) fn args ty + transf_call env ctx (Some (transf_expr env Val lhs)) fn args ty | EBinop(Ocomma, e1, e2, ty) -> ecomma (transf_expr env Effects e1) (transf_expr env ctx e2) | EBinop(op, e1, e2, ty) -> @@ -133,48 +313,92 @@ let rec transf_expr env ctx e = and transf_call env ctx opt_lhs fn args ty = let ty' = transf_type env ty in let fn' = transf_expr env Val fn in - let args' = List.map (transf_expr env Val) args in + let (assignments, args') = transf_arguments env args in let opt_eassign e = match opt_lhs with | None -> e - | Some lhs -> eassign (transf_expr env Val lhs) e in + | Some lhs -> eassign lhs e in match fn with | {edesc = EVar {name = "__builtin_va_arg"}} -> (* Do not transform the call in this case *) opt_eassign {edesc = ECall(fn, args'); etyp = ty} | _ -> - match classify_return env ty with - | Ret_scalar -> - opt_eassign {edesc = ECall(fn', args'); etyp = ty'} - | Ret_ref -> - begin match ctx, opt_lhs with - | Effects, None -> - let tmp = new_temp ~name:"_res" ty in - {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} - | Effects, Some lhs -> - let lhs' = transf_expr env Val lhs in - {edesc = ECall(fn', eaddrof lhs' :: args'); etyp = TVoid []} - | Val, None -> - let tmp = new_temp ~name:"_res" ty in - ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} - tmp - | Val, Some lhs -> - let lhs' = transf_expr env Val lhs in - let tmp = new_temp ~name:"_res" ty in - ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} - (eassign lhs' tmp) - end - | Ret_value ty_ret -> - let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in - begin match ctx, opt_lhs with - | Effects, None -> - ecall - | _, _ -> - let tmp = new_temp ~name:"_res" ty_ret in - opt_eassign - (ecomma (eassign tmp ecall) - (ereinterpret ty' tmp)) - end + let call = + match classify_return env ty with + | Ret_scalar -> + opt_eassign {edesc = ECall(fn', args'); etyp = ty'} + | Ret_ref -> + begin match ctx, opt_lhs with + | Effects, None -> + let tmp = new_temp ~name:"_res" ty in + {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} + | Effects, Some lhs -> + {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} + | Val, None -> + let tmp = new_temp ~name:"_res" ty in + ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} + tmp + | Val, Some lhs -> + let tmp = new_temp ~name:"_res" ty in + ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} + (eassign lhs tmp) + end + | Ret_value(ty_ret, sz, al) -> + let ecall = {edesc = ECall(fn', args'); etyp = ty_ret} in + begin match ctx, opt_lhs with + | Effects, None -> + ecall + | _, _ -> + let tmp = new_temp ~name:"_res" ty_ret in + opt_eassign + (ecomma (eassign tmp ecall) + (ereinterpret ty' tmp)) + end + in ecommalist assignments call + +(* Function argument of ref_caller kind: take a copy and pass pointer to copy + arg ---> newtemp = arg ... &newtemp + Function argument of flattened(N) kind: load and pass as integers + either using an intermediate array + arg ---> ( * ((ty * ) temparray) = arg ... + temparray[0], ...,, temparray[N-1] + or by using loadwords: + arg ---> addr = &(arg) ... loadwords addr ... +*) + +and transf_arguments env args = + match args with + | [] -> ([], []) + | arg :: args -> + let (assignments, args') = transf_arguments env args in + match classify_param env arg.etyp with + | Param_unchanged -> + let arg' = transf_expr env Val arg in + (assignments, arg' :: args') + | Param_ref_caller -> + let ty' = transf_type env arg.etyp in + let tmp = new_temp ~name:"_arg" ty' in + (transf_assign env tmp arg :: assignments, + eaddrof tmp :: args') + | Param_flattened(n, sz, al) -> + let ty' = transf_type env arg.etyp in + if translates_to_extended_lvalue arg then begin + let tmp = new_temp ~name:"_arg" ucharptr in + (eassign tmp (ecast ucharptr (eaddrof (transf_expr env Val arg))) + :: assignments, + load_words tmp 0 sz al @ args') + end else begin + let tmp = new_temp ~name:"_arg" (ty_buffer n) in + (transf_assign env (ereinterpret ty' tmp) arg :: assignments, + list_map_n (ebuffer_index tmp) n @ args') + end + +and transf_assign env lhs e = + match e.edesc with + | ECall(fn, args) -> + transf_call env Effects (Some lhs) fn args e.etyp + | _ -> + eassign lhs (transf_expr env Val e) (* Initializers *) @@ -204,6 +428,7 @@ let transf_expr ctx e = transf_expr env ctx e in return kind scalar -> return e return kind ref -> _res = x; return return kind value ty -> *((struct s * )_res) = x; return _res + or addr = &x; return loadresult(addr) *) let rec transf_stmt s = @@ -240,10 +465,18 @@ let rec transf_stmt s = sseq s.sloc (sassign s.sloc dst e') {sdesc = Sreturn None; sloc = s.sloc} - | Ret_value ty, Some dst -> - sseq s.sloc - (sassign s.sloc (ereinterpret e'.etyp dst) e') - {sdesc = Sreturn (Some dst); sloc = s.sloc} + | Ret_value(ty, sz, al), None -> + if translates_to_extended_lvalue e then begin + let tmp = new_temp ~name:"_res" ucharptr in + sseq s.sloc + (sassign s.sloc tmp (ecast ucharptr (eaddrof e'))) + {sdesc = Sreturn (Some (load_result tmp sz al)); sloc = s.sloc} + end else begin + let dst = new_temp ~name:"_res" ty in + sseq s.sloc + (sassign s.sloc (ereinterpret e'.etyp dst) e') + {sdesc = Sreturn (Some dst); sloc = s.sloc} + end | _, _ -> assert false end @@ -256,29 +489,77 @@ let rec transf_stmt s = in transf_stmt body +(* Binding arguments to parameters. Returns a triple: + - parameter list + - actions to perform at the beginning of the function + - substitution to apply to the function body +*) + +let rec transf_funparams loc env params = + match params with + | [] -> + ([], sskip, IdentMap.empty) + | (x, tx) :: params -> + let tx' = transf_type env tx in + let (params', actions, subst) = transf_funparams loc env params in + match classify_param env tx with + | Param_unchanged -> + ((x, tx') :: params', + actions, + subst) + | Param_ref_caller -> + let tpx = TPtr(tx', []) in + let ex = { edesc = EVar x; etyp = tpx } in + let estarx = { edesc = EUnop(Oderef, ex); etyp = tx' } in + ((x, tpx) :: params', + actions, + IdentMap.add x estarx subst) + | Param_flattened(n, sz, al) -> + let y = new_temp ~name:x.name (ty_buffer n) in + let yparts = list_map_n (fun _ -> Env.fresh_ident x.name) n in + let assign_part e p act = + sseq loc (sassign loc e {edesc = EVar p; etyp = uint}) act in + (List.map (fun p -> (p, uint)) yparts @ params', + List.fold_right2 assign_part + (list_map_n (ebuffer_index y) n) + yparts + actions, + IdentMap.add x (ereinterpret tx' y) subst) + let transf_fundef env f = reset_temps(); let ret = transf_type env f.fd_ret in - let params = - List.map (fun (id, ty) -> (id, transf_type env ty)) f.fd_params in - let (ret1, params1, body1) = + let (params, actions, subst) = + transf_funparams f.fd_body.sloc env f.fd_params in + let locals = + List.map (fun d -> transf_decl env (subst_decl subst d)) f.fd_locals in + let (attr1, ret1, params1, body1) = match classify_return env f.fd_ret with | Ret_scalar -> - (ret, params, transf_funbody env f.fd_body None) + (f.fd_attrib, + ret, + params, + transf_funbody env (subst_stmt subst f.fd_body) None) | Ret_ref -> let vres = Env.fresh_ident "_res" in let tres = TPtr(ret, []) in let eres = {edesc = EVar vres; etyp = tres} in let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in - (TVoid [], + (add_attributes f.fd_attrib attr_structret, + TVoid [], (vres, tres) :: params, - transf_funbody env f.fd_body (Some eeres)) - | Ret_value ty -> - let eres = new_temp ~name:"_res" ty in - (ty, params, transf_funbody env f.fd_body (Some eres)) in + transf_funbody env (subst_stmt subst f.fd_body) (Some eeres)) + | Ret_value(ty, sz, al) -> + (f.fd_attrib, + ty, + params, + transf_funbody env (subst_stmt subst f.fd_body) None) in let temps = get_temps() in - {f with fd_ret = ret1; fd_params = params1; - fd_locals = f.fd_locals @ temps; fd_body = body1} + {f with fd_attrib = attr1; + fd_ret = ret1; + fd_params = params1; + fd_locals = locals @ temps; + fd_body = sseq f.fd_body.sloc actions body1} (* Composites *) @@ -288,6 +569,14 @@ let transf_composite env su id attr fl = (* Entry point *) let program p = + struct_passing_style := + if !Clflags.option_interp + then SP_ref_callee + else !Clflags.option_fstruct_passing_style; + struct_return_style := + if !Clflags.option_interp + then SR_ref + else !Clflags.option_fstruct_return_style; Transform.program ~decl:transf_decl ~fundef:transf_fundef diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 405986f3..4013db9b 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -149,7 +149,7 @@ let rec expand_expr islocal env e = | ECall(e1, el) -> {edesc = ECall(expand e1, List.map expand el); etyp = e.etyp} in - let e' = expand e in add_inits_expr !inits e' + let e' = expand e in ecommalist !inits e' (* Elimination of compound literals within an initializer. *) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ead27b36..8899c2b0 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -17,6 +17,8 @@ let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) let option_flongdouble = ref false let option_fstruct_return = ref false +let option_fstruct_return_style = ref Configuration.struct_return_style +let option_fstruct_passing_style = ref Configuration.struct_passing_style let option_fbitfields = ref false let option_fvararg_calls = ref true let option_funprototyped = ref true diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 0012dc0c..237085de 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -94,3 +94,30 @@ let asm_supports_cfi = | v -> bad_config "asm_supports_cfi" [v] let version = get_config_string "version" + +type struct_passing_style = + | SP_ref_callee (* by reference, callee takes copy *) + | SP_ref_caller (* by reference, caller takes copy *) + | SP_split_args (* by value, as a sequence of ints *) + +type struct_return_style = + | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) + | SR_int1to4 (* return by content if size is <= 4 *) + | SR_int1to8 (* return by content if size is <= 8 *) + | SR_ref (* always return by assignment to a reference + given as extra argument *) + +let struct_passing_style = + match get_config_string "struct_passing_style" with + | "ref-callee" -> SP_ref_callee + | "ref-caller" -> SP_ref_caller + | "ints" -> SP_split_args + | v -> bad_config "struct_passing_style" [v] + +let struct_return_style = + match get_config_string "struct_return_style" with + | "int1248" -> SR_int1248 + | "int1-4" -> SR_int1to4 + | "int1-8" -> SR_int1to8 + | "ref" -> SR_ref + | v -> bad_config "struct_return_style" [v] diff --git a/driver/Configuration.mli b/driver/Configuration.mli new file mode 100644 index 00000000..875bd692 --- /dev/null +++ b/driver/Configuration.mli @@ -0,0 +1,55 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +val arch: string + (** Target architecture *) +val model: string + (** Sub-model for this architecture *) +val abi: string + (** ABI to use *) +val system: string + (** Flavor of operating system that runs CompCert *) + +val prepro: string list + (** How to invoke the external preprocessor *) +val asm: string list + (** How to invoke the external assembler *) +val linker: string list + (** How to invoke the external linker *) +val asm_supports_cfi: bool + (** True if the assembler supports Call Frame Information *) +val stdlib_path: string + (** Path to CompCert's library *) +val has_runtime_lib: bool + (** True if CompCert's library is available. *) + +val version: string + (** CompCert version string *) + +type struct_passing_style = + | SP_ref_callee (* by reference, callee takes copy *) + | SP_ref_caller (* by reference, caller takes copy *) + | SP_split_args (* by value, as a sequence of ints *) + +type struct_return_style = + | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) + | SR_int1to4 (* return by content if size is <= 4 *) + | SR_int1to8 (* return by content if size is <= 8 *) + | SR_ref (* always return by assignment to a reference + given as extra argument *) + +val struct_passing_style: struct_passing_style + (** Calling conventions to use for passing structs and unions as + first-class values *) +val struct_return_style: struct_return_style + (** Calling conventions to use for returning structs and unions as + first-class values *) diff --git a/driver/Driver.ml b/driver/Driver.ml index d22dd77c..ad7cf61e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -265,6 +265,7 @@ let process_c_file sourcename = let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin + Machine.config := Machine.compcert_interpreter !Machine.config; let csyntax = parse_c_file sourcename preproname in safe_remove preproname; Interp.execute csyntax; @@ -409,6 +410,10 @@ Language support options (use -fno-<opt> to turn off -f<opt>) : -fbitfields Emulate bit fields in structs [off] -flongdouble Treat 'long double' as 'double' [off] -fstruct-return Emulate returning structs and unions by value [off] + -fstruct-return=<convention> + Set the calling conventions used to return structs by value + -fstruct-passing=<convention> + Set the calling conventions used to pass structs by value -fvararg-calls Support calls to variable-argument functions [on] -funprototyped Support calls to old-style functions without prototypes [on] -fpacked-structs Emulate packed structs [off] @@ -550,7 +555,28 @@ let cmdline_actions = Exact "-quiet", Self (fun _ -> Interp.trace := 0); Exact "-trace", Self (fun _ -> Interp.trace := 2); Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All) + Exact "-all", Self (fun _ -> Interp.mode := Interp.All); +(* Special -f options *) + Exact "-fstruct-passing=ref-callee", + Self (fun _ -> option_fstruct_passing_style := Configuration.SP_ref_callee); + Exact "-fstruct-passing=ref-caller", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Configuration.SP_ref_caller); + Exact "-fstruct-passing=ints", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_passing_style := Configuration.SP_split_args); + Exact "-fstruct-return=ref", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_ref); + Exact "-fstruct-return=int1248", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_int1248); + Exact "-fstruct-return=int1-4", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_int1to4); + Exact "-fstruct-return=int1-8", + Self (fun _ -> option_fstruct_return := true; + option_fstruct_return_style := Configuration.SR_int1to8) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @@ -607,7 +633,9 @@ let _ = begin match Configuration.arch with | "powerpc" -> Machine.ppc_32_bigendian | "arm" -> Machine.arm_littleendian - | "ia32" -> Machine.x86_32 + | "ia32" -> if Configuration.abi = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 | _ -> assert false end; Builtins.set C2C.builtins; diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 7d71d1a2..0ca343fb 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -462,12 +462,14 @@ Proof. rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. destruct (Int.ltu i i0); reflexivity. (* int ptr *) - destruct (Int.eq i Int.zero) eqn:?; try discriminate. + destruct (Int.eq i Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr int *) - destruct (Int.eq i0 Int.zero) eqn:?; try discriminate. + destruct (Int.eq i0 Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. @@ -647,6 +647,7 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true + | Ocmp (Ccompuimm _ _) => true | _ => false end. @@ -656,7 +657,7 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; try congruence. reflexivity. + destruct c; simpl; auto; congruence. Qed. (** Global variables mentioned in an operation or addressing mode *) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 0de38471..cb4905ef 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -801,8 +801,10 @@ module Target(System: SYSTEM):TARGET = | Pjmp_l(l) -> fprintf oc " jmp %a\n" label (transl_label l) | Pjmp_s(f, sg) -> + assert (not sg.sig_cc.cc_structret); fprintf oc " jmp %a\n" symbol f | Pjmp_r(r, sg) -> + assert (not sg.sig_cc.cc_structret); fprintf oc " jmp *%a\n" ireg r | Pjcc(c, l) -> let l = transl_label l in @@ -818,12 +820,21 @@ module Target(System: SYSTEM):TARGET = fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; jumptables := (l, tbl) :: !jumptables | Pcall_s(f, sg) -> - fprintf oc " call %a\n" symbol f + fprintf oc " call %a\n" symbol f; + if sg.sig_cc.cc_structret then + fprintf oc " pushl %%eax\n" | Pcall_r(r, sg) -> - fprintf oc " call *%a\n" ireg r + fprintf oc " call *%a\n" ireg r; + if sg.sig_cc.cc_structret then + fprintf oc " pushl %%eax\n" | Pret -> - fprintf oc " ret\n" - (** Pseudo-instructions *) + if (!current_function_sig).sig_cc.cc_structret then begin + fprintf oc " movl 0(%%esp), %%eax\n"; + fprintf oc " ret $4\n" + end else begin + fprintf oc " ret\n" + end + (** Pseudo-instructions *) | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) | Pallocframe(sz, ofs_ra, ofs_link) -> @@ -64,13 +64,13 @@ Module Type TREE. Hypothesis gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then Some x else get i m. + (* We could implement the following, but it's not needed for the moment. Hypothesis gsident: forall (A: Type) (i: elt) (m: t A) (v: A), get i m = Some v -> set i v m = m. - (* We could implement the following, but it's not needed for the moment. - Hypothesis grident: - forall (A: Type) (i: elt) (m: t A) (v: A), - get i m = None -> remove i m = m. + Hypothesis grident: + forall (A: Type) (i: elt) (m: t A) (v: A), + get i m = None -> remove i m = m. *) Hypothesis grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. @@ -115,11 +115,6 @@ Module Type TREE. f None None = None -> forall (m1: t A) (m2: t B) (i: elt), get i (combine f m1 m2) = f (get i m1) (get i m2). - Hypothesis combine_commut: - forall (A B: Type) (f g: option A -> option A -> option B), - (forall (i j: option A), f i j = g j i) -> - forall (m1 m2: t A), - combine f m1 m2 = combine g m2 m1. (** Enumerating the bindings of a tree. *) Variable elements: diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S index ae06e361..5e319b8b 100644 --- a/runtime/arm/vararg.S +++ b/runtime/arm/vararg.S @@ -75,3 +75,15 @@ FUNCTION(__compcert_va_float64) #endif bx lr ENDFUNCTION(__compcert_va_float64) + +FUNCTION(__compcert_va_composite) + @ r0 = ap parameter + @ r1 = size of the composite, in bytes + ldr r2, [r0, #0] @ r2 = pointer to next argument + ADD r3, r2, r1 @ advance by size + ADD r3, r3, #3 @ 4-align + BIC r3, r3, #3 + str r3, [r0, #0] @ update ap + mov r0, r2 @ result is pointer to composite in stack + bx lr +ENDFUNCTION(__compcert_va_composite) diff --git a/runtime/ia32/vararg.S b/runtime/ia32/vararg.S index ec55a454..78666c70 100644 --- a/runtime/ia32/vararg.S +++ b/runtime/ia32/vararg.S @@ -67,3 +67,15 @@ FUNCTION(__compcert_va_float64) movl %edx, 0(%ecx) ret ENDFUNCTION(__compcert_va_float64) + +FUNCTION(__compcert_va_composite) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 8(%esp), %edx // %edx = size of composite in bytes + movl 0(%ecx), %eax // %eax = current argument pointer + leal 3(%eax, %edx), %edx // advance by size + andl $0xfffffffc, %edx // and round up to multiple of 4 + movl %edx, 0(%ecx) // update argument pointer + ret +ENDFUNCTION(__compcert_va_composite) + + diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s index 16681c1c..8d7e62c8 100644 --- a/runtime/powerpc/vararg.s +++ b/runtime/powerpc/vararg.s @@ -128,6 +128,13 @@ __compcert_va_float64: .type __compcert_va_float64, @function .size __compcert_va_float64, .-__compcert_va_int64 + .balign 16 + .globl __compcert_va_composite +__compcert_va_composite: + b __compcert_va_int32 + .type __compcert_va_composite, @function + .size __compcert_va_composite, .-__compcert_va_composite + # Save integer and FP registers at beginning of vararg function .balign 16 diff --git a/test/regression/Makefile b/test/regression/Makefile index 5c601211..206670b5 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \ volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 switch switch2 compound \ - decl1 + decl1 interop1 # Can run, but only in compiled mode, and have reference output in Results @@ -45,6 +45,13 @@ all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(TESTS_DIFF:%=%.compcert) all_s: $(TESTS:%=%.s) $(TESTS_COMP:%=%.s) $(TESTS_DIFF:%=%.s) $(EXTRAS:%=%.s) +interop1.compcert: interop1.c $(CCOMP) + $(CC) -DCC_SIDE -c -o interop1n.o interop1.c + $(CCOMP) $(CCOMPFLAGS) -DCOMPCERT_SIDE -o interop1.compcert interop1.c interop1n.o $(LIBS) + +interop1.s: interop1.c $(CCOMP) + $(CCOMP) $(CCOMPFLAGS) -S interop1.c + %.compcert: %.c $(CCOMP) $(CCOMP) $(CCOMPFLAGS) -o $*.compcert $*.c $(LIBS) diff --git a/test/regression/Results/interop1 b/test/regression/Results/interop1 new file mode 100644 index 00000000..990dfe9d --- /dev/null +++ b/test/regression/Results/interop1 @@ -0,0 +1,90 @@ +--- CompCert calling native: +s1: { a = 'a' } +s2: { a = 'a', b = 'b' } +s3: { a = 'a', b = 'b', c = ' c' } +s4: { a = 'a', b = 'b', c = ' c', d = 'd' } +s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' } +s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' } +s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' } +s8: "Hello world!" +t1: { a = 123 } +t2: { a = 123, b = 456 } +t3: { a = 123, b = 456, c = 789 } +t4: { a = 123, b = 456, c = 789, d = -111 } +t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' } +u1: { a = 12 } +u2: { a = 12, b = -34 } +u3: { a = 12, b = 34, c = -56 } +u4: { a = 12, b = 34, c = 56, d = -78 } +u5: { a = 1234, b = 'u' } +u6: { a = 55555, b = 666 } +u7: { a = -10001, b = -789, c = 'z' } +u8: { a = 'x', b = 12345 } +after ms4, x = { 's', 'a', 'm', 'e' } +after mu4, x = { a = { 11, 22, 33, 44 } } +rs1: { a = 'a' } +rs2: { a = 'a', b = 'b' } +rs3: { a = 'a', b = 'b', c = ' c' } +rs4: { a = 'a', b = 'b', c = ' c', d = 'd' } +rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' } +rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' } +rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' } +rs8: "Hello world!" +rt1: { a = 123 } +rt2: { a = 123, b = 456 } +rt3: { a = 123, b = 456, c = 789 } +rt4: { a = 123, b = 456, c = 789, d = -111 } +rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' } +ru1: { a = 12 } +ru2: { a = 12, b = -34 } +ru3: { a = 12, b = 34, c = -56 } +ru4: { a = 12, b = 34, c = 56, d = -78 } +ru5: { a = 1234, b = 'u' } +ru6: { a = 55555, b = 666 } +ru7: { a = -10001, b = -789, c = 'z' } +ru8: { a = 'x', b = 12345 } +--- native calling CompCert: +s1: { a = 'a' } +s2: { a = 'a', b = 'b' } +s3: { a = 'a', b = 'b', c = ' c' } +s4: { a = 'a', b = 'b', c = ' c', d = 'd' } +s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' } +s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' } +s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' } +s8: "Hello world!" +t1: { a = 123 } +t2: { a = 123, b = 456 } +t3: { a = 123, b = 456, c = 789 } +t4: { a = 123, b = 456, c = 789, d = -111 } +t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' } +u1: { a = 12 } +u2: { a = 12, b = -34 } +u3: { a = 12, b = 34, c = -56 } +u4: { a = 12, b = 34, c = 56, d = -78 } +u5: { a = 1234, b = 'u' } +u6: { a = 55555, b = 666 } +u7: { a = -10001, b = -789, c = 'z' } +u8: { a = 'x', b = 12345 } +after ms4, x = { 's', 'a', 'm', 'e' } +after mu4, x = { a = { 11, 22, 33, 44 } } +rs1: { a = 'a' } +rs2: { a = 'a', b = 'b' } +rs3: { a = 'a', b = 'b', c = ' c' } +rs4: { a = 'a', b = 'b', c = ' c', d = 'd' } +rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' } +rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' } +rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' } +rs8: "Hello world!" +rt1: { a = 123 } +rt2: { a = 123, b = 456 } +rt3: { a = 123, b = 456, c = 789 } +rt4: { a = 123, b = 456, c = 789, d = -111 } +rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' } +ru1: { a = 12 } +ru2: { a = 12, b = -34 } +ru3: { a = 12, b = 34, c = -56 } +ru4: { a = 12, b = 34, c = 56, d = -78 } +ru5: { a = 1234, b = 'u' } +ru6: { a = 55555, b = 666 } +ru7: { a = -10001, b = -789, c = 'z' } +ru8: { a = 'x', b = 12345 } diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2 index f954927e..96ee9d63 100644 --- a/test/regression/Results/varargs2 +++ b/test/regression/Results/varargs2 @@ -2,7 +2,9 @@ An int: 42 A long long: 123456789012345 A string: Hello world A double: 3.141592654 -A mixture: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746 +A small struct: x12 +A bigger struct: (123,456,789) +A mixture: x & Hello, world! & y2 & 42 & 123456789012345 & 3.141592654 & 2.718281746 Twice: -1 1.23 Twice: -1 1.23 With va_copy: -1 1.23 diff --git a/test/regression/interop1.c b/test/regression/interop1.c new file mode 100644 index 00000000..a39f449c --- /dev/null +++ b/test/regression/interop1.c @@ -0,0 +1,286 @@ +#if defined(COMPCERT_SIDE) +#define US(x) compcert_##x +#define THEM(x) native_##x +#elif defined(CC_SIDE) +#define US(x) native_##x +#define THEM(x) compcert_##x +#else +#define US(x) x +#define THEM(x) x +#endif + +#include <stdio.h> + +/* Alignment 1 */ + +struct S1 { char a; }; +static struct S1 init_S1 = { 'a' }; +#define print_S1(x) printf("{ a = '%c' }\n", x.a) + +struct S2 { char a, b; }; +static struct S2 init_S2 = { 'a', 'b' }; +#define print_S2(x) printf("{ a = '%c', b = '%c' }\n", x.a, x.b) + +struct S3 { char a, b, c; }; +static struct S3 init_S3 = { 'a', 'b', 'c' }; +#define print_S3(x) \ + printf("{ a = '%c', b = '%c', c = ' %c' }\n", x.a, x.b, x.c) + +struct S4 { char a, b, c, d; }; +static struct S4 init_S4 = { 'a', 'b', 'c', 'd' }; +#define print_S4(x) \ + printf("{ a = '%c', b = '%c', c = ' %c', d = '%c' }\n", \ + x.a, x.b, x.c, x.d); + +struct S5 { char a, b, c, d, e; }; +static struct S5 init_S5 = { 'a', 'b', 'c', 'd', 'e' }; +#define print_S5(x) \ + printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c' }\n", \ + x.a, x.b, x.c, x.d, x.e) + +struct S6 { char a, b, c, d, e, f; }; +static struct S6 init_S6 = { 'a', 'b', 'c', 'd', 'e', 'f' }; +#define print_S6(x) \ + printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c' }\n", \ + x.a, x.b, x.c, x.d, x.e, x.f) + +struct S7 { char a, b, c, d, e, f, g; }; +static struct S7 init_S7 = { 'a', 'b', 'c', 'd', 'e', 'f', 'g' }; +#define print_S7(x) \ + printf("{ a = '%c', b = '%c', c = ' %c', d = '%c', e = '%c', f = '%c', g = '%c' }\n", \ + x.a, x.b, x.c, x.d, x.e, x.f, x.g) + +struct S8 { char a[32]; }; +static struct S8 init_S8 = { "Hello world!" }; +/* Do not use printf("%s") to avoid undefined behavior in the + reference interpreter */ +#define print_S8(x) \ + { char * p; \ + printf("\""); \ + for (p = x.a; *p != 0; p++) printf("%c", *p); \ + printf("\"\n"); \ + } + +/* Alignment 2 */ + +struct T1 { short a; }; +static struct T1 init_T1 = { 123 }; +#define print_T1(x) printf("{ a = %d }\n", x.a) + +struct T2 { short a, b; }; +static struct T2 init_T2 = { 123, 456 }; +#define print_T2(x) printf("{ a = %d, b = %d }\n", x.a, x.b) + +struct T3 { short a, b, c; }; +static struct T3 init_T3 = { 123, 456, 789 }; +#define print_T3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c) + +struct T4 { short a, b, c, d; }; +static struct T4 init_T4 = { 123, 456, 789, -111 }; +#define print_T4(x) \ + printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d) + +struct T5 { short a, b, c, d; char e; }; +static struct T5 init_T5 = { 123, 456, 789, -999, 'x' }; +#define print_T5(x) \ + printf("{ a = %d, b = %d, c = %d, d = %d, e = '%c' }\n", \ + x.a, x.b, x.c, x.d, x.e) + +/* Alignment >= 4 */ + +struct U1 { int a; }; +static struct U1 init_U1 = { 12 }; +#define print_U1(x) printf("{ a = %d }\n", x.a) + +struct U2 { int a, b; }; +static struct U2 init_U2 = { 12, -34 }; +#define print_U2(x) printf("{ a = %d, b = %d }\n", x.a, x.b) + +struct U3 { int a, b, c; }; +static struct U3 init_U3 = { 12, 34, -56}; +#define print_U3(x) printf("{ a = %d, b = %d, c = %d }\n", x.a, x.b, x.c) + +struct U4 { int a, b, c, d; }; +static struct U4 init_U4 = { 12, 34, 56, -78 }; +#define print_U4(x) \ + printf("{ a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d) + +struct U5 { int a; char b; }; +static struct U5 init_U5 = { 1234, 'u' }; +#define print_U5(x) \ + printf("{ a = %d, b = '%c' }\n", x.a, x.b) + +struct U6 { int a; short b; }; +static struct U6 init_U6 = { 55555, 666 }; +#define print_U6(x) \ + printf("{ a = %d, b = %d }\n", x.a, x.b) + +struct U7 { int a; short b; char c; }; +static struct U7 init_U7 = { -10001, -789, 'z' }; +#define print_U7(x) \ + printf("{ a = %d, b = %d, c = '%c' }\n", x.a, x.b, x.c) + +struct U8 { char a; int b; }; +static struct U8 init_U8 = { 'x', 12345 }; +#define print_U8(x) \ + printf("{ a = '%c', b = %d }\n", x.a, x.b) + +/* Struct passing */ + +#define PRINT(name,ty,print) \ +extern void THEM(name) (struct ty x); \ +void US(name) (struct ty x) { print(x); } + +PRINT(s1,S1,print_S1) +PRINT(s2,S2,print_S2) +PRINT(s3,S3,print_S3) +PRINT(s4,S4,print_S4) +PRINT(s5,S5,print_S5) +PRINT(s6,S6,print_S6) +PRINT(s7,S7,print_S7) +PRINT(s8,S8,print_S8) +PRINT(t1,T1,print_T1) +PRINT(t2,T2,print_T2) +PRINT(t3,T3,print_T3) +PRINT(t4,T4,print_T4) +PRINT(t5,T5,print_T5) +PRINT(u1,U1,print_U1) +PRINT(u2,U2,print_U2) +PRINT(u3,U3,print_U3) +PRINT(u4,U4,print_U4) +PRINT(u5,U5,print_U5) +PRINT(u6,U6,print_U6) +PRINT(u7,U7,print_U7) +PRINT(u8,U8,print_U8) + +/* Struct passing with modification in the callee */ + +extern void THEM (ms4) (struct S4 x); +void US (ms4) (struct S4 x) +{ + x.a += 1; x.d -= 1; +} + +extern void THEM (mu4) (struct U4 x); +void US (mu4) (struct U4 x) +{ + x.a = 1; x.b = 2; +} + +/* Struct return */ + +#define RETURN(name,ty,init) \ +extern struct ty THEM(name)(void); \ +struct ty US(name)(void) { return init; } + +RETURN(rs1,S1,init_S1) +RETURN(rs2,S2,init_S2) +RETURN(rs3,S3,init_S3) +RETURN(rs4,S4,init_S4) +RETURN(rs5,S5,init_S5) +RETURN(rs6,S6,init_S6) +RETURN(rs7,S7,init_S7) +RETURN(rs8,S8,init_S8) +RETURN(rt1,T1,init_T1) +RETURN(rt2,T2,init_T2) +RETURN(rt3,T3,init_T3) +RETURN(rt4,T4,init_T4) +RETURN(rt5,T5,init_T5) +RETURN(ru1,U1,init_U1) +RETURN(ru2,U2,init_U2) +RETURN(ru3,U3,init_U3) +RETURN(ru4,U4,init_U4) +RETURN(ru5,U5,init_U5) +RETURN(ru6,U6,init_U6) +RETURN(ru7,U7,init_U7) +RETURN(ru8,U8,init_U8) + +/* Test function, calling the functions compiled by the other compiler */ + +#define CALLPRINT(name,ty,init) \ + printf(#name": "); THEM(name)(init); + +#define CALLRETURN(name,ty,print) \ + { struct ty x = THEM(name)(); \ + printf(#name": "); print(x); } + +extern void THEM(test) (void); +void US(test) (void) +{ + CALLPRINT(s1,S1,init_S1) + CALLPRINT(s2,S2,init_S2) + CALLPRINT(s3,S3,init_S3) + CALLPRINT(s4,S4,init_S4) + CALLPRINT(s5,S5,init_S5) + CALLPRINT(s6,S6,init_S6) + CALLPRINT(s7,S7,init_S7) + CALLPRINT(s8,S8,init_S8) + CALLPRINT(t1,T1,init_T1) + CALLPRINT(t2,T2,init_T2) + CALLPRINT(t3,T3,init_T3) + CALLPRINT(t4,T4,init_T4) + CALLPRINT(t5,T5,init_T5) + CALLPRINT(u1,U1,init_U1) + CALLPRINT(u2,U2,init_U2) + CALLPRINT(u3,U3,init_U3) + CALLPRINT(u4,U4,init_U4) + CALLPRINT(u5,U5,init_U5) + CALLPRINT(u6,U6,init_U6) + CALLPRINT(u7,U7,init_U7) + CALLPRINT(u8,U8,init_U8) + + { struct S4 x = { 's', 'a', 'm', 'e' }; + THEM(ms4)(x); + printf("after ms4, x = { '%c', '%c', '%c', '%c' }\n", x.a, x.b, x.c, x.d); } + { struct U4 x = { 11, 22, 33, 44 }; + THEM(mu4)(x); + printf("after mu4, x = { a = { %d, %d, %d, %d } }\n", x.a, x.b, x.c, x.d); } + + CALLRETURN(rs1,S1,print_S1) + CALLRETURN(rs2,S2,print_S2) + CALLRETURN(rs3,S3,print_S3) + CALLRETURN(rs4,S4,print_S4) + CALLRETURN(rs5,S5,print_S5) + CALLRETURN(rs6,S6,print_S6) + CALLRETURN(rs7,S7,print_S7) + CALLRETURN(rs8,S8,print_S8) + CALLRETURN(rt1,T1,print_T1) + CALLRETURN(rt2,T2,print_T2) + CALLRETURN(rt3,T3,print_T3) + CALLRETURN(rt4,T4,print_T4) + CALLRETURN(rt5,T5,print_T5) + CALLRETURN(ru1,U1,print_U1) + CALLRETURN(ru2,U2,print_U2) + CALLRETURN(ru3,U3,print_U3) + CALLRETURN(ru4,U4,print_U4) + CALLRETURN(ru5,U5,print_U5) + CALLRETURN(ru6,U6,print_U6) + CALLRETURN(ru7,U7,print_U7) + CALLRETURN(ru8,U8,print_U8) +} + +#if defined(COMPCERT_SIDE) + +int main() +{ + printf("--- CompCert calling native:\n"); + compcert_test(); + printf("--- native calling CompCert:\n"); + native_test(); + return 0; +} + +#elif !defined(CC_SIDE) + +int main() +{ + printf("--- CompCert calling native:\n"); + test(); + printf("--- native calling CompCert:\n"); + test(); + return 0; +} + +#endif + + diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c index 6c091d8b..b96d1940 100644 --- a/test/regression/varargs2.c +++ b/test/regression/varargs2.c @@ -1,6 +1,9 @@ #include <stdarg.h> #include <stdio.h> +struct Y { char kind; unsigned char num; }; +struct Z { int x, y, z; }; + void minivprintf(const char * fmt, va_list ap) { char c; @@ -32,6 +35,14 @@ void minivprintf(const char * fmt, va_list ap) case 'f': printf("%.10g", (float) va_arg(ap, double)); break; + case 'y': + { struct Y s = va_arg(ap, struct Y); + printf("%c%d", s.kind, s.num); + break; } + case 'z': + { struct Z s = va_arg(ap, struct Z); + printf("(%d,%d,%d)", s.x, s.y, s.z); + break; } default: puts("<bad format>"); return; @@ -111,9 +122,12 @@ int main() miniprintf("A long long: %l\n", 123456789012345LL); miniprintf("A string: %s\n", "Hello world"); miniprintf("A double: %e\n", 3.141592654); - miniprintf("A mixture: %c & %s & %d & %l & %e & %f\n", + miniprintf("A small struct: %y\n", (struct Y) { 'x', 12 }); + miniprintf("A bigger struct: %z\n", (struct Z) { 123, 456, 789 }); + miniprintf("A mixture: %c & %s & %y & %d & %l & %e & %f\n", 'x', "Hello, world!", + (struct Y) { 'y', 2 }, 42, 123456789012345LL, 3.141592654, |