diff options
| -rw-r--r-- | caml/Cil2Csyntax.ml | 13 | ||||
| -rw-r--r-- | caml/PrintCsyntax.ml | 60 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 8 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 19 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 26 | ||||
| -rw-r--r-- | cfrontend/Csyntax.v | 20 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 13 |
7 files changed, 82 insertions, 77 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 779929c..de0b616 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -345,7 +345,7 @@ and convertLval lv = | NoOffset -> e | Field (f, ofs) -> begin match t with - | Tstruct fList -> + | Tstruct(_, fList) -> begin try let idf = intern_string f.fname in let t' = getFieldType idf fList in @@ -353,7 +353,7 @@ and convertLval lv = with Not_found -> internal_error "processOffset: no such struct field" end - | Tunion fList -> + | Tunion(_, fList) -> begin try let idf = intern_string f.fname in let t' = getFieldType idf fList in @@ -399,6 +399,8 @@ and convertTypGen env = function | TVoid _ -> Tvoid | TInt (k, _) -> let (x, y) = convertIkind k in Tint (x, y) | TFloat (k, _) -> Tfloat (convertFkind k) + | TPtr (TComp(c, _), _) when List.mem c.ckey env -> + Tcomp_ptr (intern_string (Cil.compFullName c)) | TPtr (t, _) -> Tpointer (convertTypGen env t) | TArray (t, eOpt, _) -> begin match eOpt with @@ -423,7 +425,9 @@ and convertTypGen env = function end | TNamed (tinfo, _) -> convertTypGen env tinfo.ttype | TComp (c, _) -> - if List.mem c.ckey env then Tvoid else begin + if List.mem c.ckey env then + unsupported "ill-formed recursive structure or union" + else begin let rec convertFieldList = function | [] -> Fnil | {fname=str; ftype=t} :: rem -> @@ -431,7 +435,8 @@ and convertTypGen env = function let t' = convertTypGen (c.ckey :: env) t in Fcons(idf, t', convertFieldList rem) in let fList = convertFieldList c.cfields in - if c.cstruct then Tstruct fList else Tunion fList + let id = intern_string (Cil.compFullName c) in + if c.cstruct then Tstruct(id, fList) else Tunion(id, fList) end | TEnum _ -> constInt32 (* enum constants are integers *) | TBuiltin_va_list _ -> unsupported "GCC `builtin va_list' type" diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml index da257bd..f837099 100644 --- a/caml/PrintCsyntax.ml +++ b/caml/PrintCsyntax.ml @@ -45,25 +45,17 @@ let name_floattype sz = | F32 -> "float" | F64 -> "double" -(* Naming of structs and unions *) - -type su_kind = Struct | Union - -let struct_union_names = ref [] -let struct_union_name_counter = ref 0 - -let register_struct_union kind fld = - if not (List.mem_assoc (kind, fld) !struct_union_names) then begin - incr struct_union_name_counter; - let s = - match kind with - | Struct -> sprintf "s%d" !struct_union_name_counter - | Union -> sprintf "u%d" !struct_union_name_counter in - struct_union_names := ((kind, fld), s) :: !struct_union_names - end - -let struct_union_name kind fld = - try List.assoc (kind, fld) !struct_union_names with Not_found -> "<unknown>" +(* Collecting the names and fields of structs and unions *) + +module StructUnionSet = Set.Make(struct + type t = string * fieldlist + let compare = (compare: t -> t -> int) +end) + +let struct_unions = ref StructUnionSet.empty + +let register_struct_union id fld = + struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions (* Declarator (identifier + type) *) @@ -107,10 +99,12 @@ let rec name_cdecl id ty = end; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res - | Tstruct fld -> - "struct " ^ struct_union_name Struct fld ^ name_optid id - | Tunion fld -> - "union " ^ struct_union_name Union fld ^ name_optid id + | Tstruct(name, fld) -> + extern_atom name ^ name_optid id + | Tunion(name, fld) -> + extern_atom name ^ name_optid id + | Tcomp_ptr name -> + extern_atom name ^ " *" ^ id (* Type *) @@ -346,8 +340,9 @@ let rec collect_type = function | Tpointer t -> collect_type t | Tarray(t, n) -> collect_type t | Tfunction(args, res) -> collect_type_list args; collect_type res - | Tstruct fld -> register_struct_union Struct fld; collect_fields fld - | Tunion fld -> register_struct_union Union fld; collect_fields fld + | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld + | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld + | Tcomp_ptr _ -> () and collect_type_list = function | Tnil -> () @@ -417,10 +412,11 @@ let collect_program p = coqlist_iter collect_globvar p.prog_vars; coqlist_iter collect_fundef p.prog_funct -let print_struct_or_union p ((kind, fld), name) = - fprintf p "@[<v 2>%s %s {" - (match kind with Struct -> "struct" | Union -> "union") - name; +let declare_struct_or_union p (name, fld) = + fprintf p "%s;@ @ " name + +let print_struct_or_union p (name, fld) = + fprintf p "@[<v 2>%s {" name; let rec print_fields = function | Fnil -> () | Fcons(id, ty, rem) -> @@ -430,11 +426,11 @@ let print_struct_or_union p ((kind, fld), name) = fprintf p "@;<0 -2>}@]@ " let print_program p prog = - struct_union_names := []; - struct_union_name_counter := 0; + struct_unions := StructUnionSet.empty; collect_program prog; fprintf p "@[<v 0>"; - List.iter (print_struct_or_union p) !struct_union_names; + StructUnionSet.iter (declare_struct_or_union p) !struct_unions; + StructUnionSet.iter (print_struct_or_union p) !struct_unions; coqlist_iter (print_globvar p) prog.prog_vars; coqlist_iter (print_fundef p) prog.prog_funct; fprintf p "@]@." diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5431697..4cc8555 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -556,15 +556,15 @@ with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop := sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> eval_lvalue e m (Expr (Eindex a1 a2) ty) (t1 ** t2) m2 l ofs - | eval_Efield_struct: forall e m a t m1 l ofs fList i ty delta, + | eval_Efield_struct: forall e m a t m1 l ofs id fList i ty delta, eval_lvalue e m a t m1 l ofs -> - typeof a = Tstruct fList -> + typeof a = Tstruct id fList -> field_offset i fList = Some delta -> eval_lvalue e m (Expr (Efield a i) ty) t m1 l (Int.add ofs (Int.repr delta)) - | eval_Efield_union: forall e m a t m1 l ofs fList i ty, + | eval_Efield_union: forall e m a t m1 l ofs id fList i ty, eval_lvalue e m a t m1 l ofs -> - typeof a = Tunion fList -> + typeof a = Tunion id fList -> eval_lvalue e m (Expr (Efield a i) ty) t m1 l ofs diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 5585416..aaec07d 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -41,8 +41,9 @@ Definition var_kind_of_type (ty: type): option var_kind := | Tpointer _ => Some(Vscalar Mint32) | Tarray _ _ => Some(Varray (Csyntax.sizeof ty)) | Tfunction _ _ => None - | Tstruct fList => Some(Varray (Csyntax.sizeof ty)) - | Tunion fList => Some(Varray (Csyntax.sizeof ty)) + | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty)) + | Tunion _ fList => Some(Varray (Csyntax.sizeof ty)) + | Tcomp_ptr _ => Some(Vscalar Mint32) end. (** ** Csharpminor constructors *) @@ -359,13 +360,13 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := Some(make_intconst (Int.repr (Csyntax.sizeof ty))) | Expr (Csyntax.Efield b i) ty => match typeof b with - | Tstruct fld => + | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; make_load (make_binop Oadd tb (make_intconst (Int.repr ofs))) ty - | Tunion fld => + | Tunion _ fld => do tb <- transl_lvalue b; make_load tb ty | _ => None @@ -389,11 +390,11 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := make_add tb (typeof b) tc (typeof c) | Expr (Csyntax.Efield b i) ty => match typeof b with - | Tstruct fld => + | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; Some (make_binop Oadd tb (make_intconst (Int.repr ofs))) - | Tunion fld => + | Tunion _ fld => transl_lvalue b | _ => None end @@ -430,9 +431,9 @@ Definition is_variable (e: Csyntax.expr) : option ident := Definition exit_if_false (e: Csyntax.expr) : option stmt := do te <- transl_expr e; Some(Sifthenelse - (make_notbool te (typeof e)) - (Sexit 0%nat) - Sskip). + (make_boolean te (typeof e)) + Sskip + (Sexit 0%nat)). (* [transl_statement nbrk ncnt s] returns a Csharpminor statement that performs the same computations as the CabsCoq statement [s]. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 5b4146b..497286b 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -725,11 +725,11 @@ Qed. Lemma transl_Efield_struct_correct: (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident) + (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) (ty : type) (delta : Z), eval_lvalue ge e m a t m1 l ofs -> eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tstruct fList -> + typeof a = Tstruct id fList -> field_offset i fList = Some delta -> eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l (Int.add ofs (Int.repr delta))). @@ -743,11 +743,11 @@ Qed. Lemma transl_Efield_union_correct: (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (fList : fieldlist) (i : ident) + (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) (ty : type), eval_lvalue ge e m a t m1 l ofs -> eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tunion fList -> + typeof a = Tunion id fList -> eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l ofs). Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -925,13 +925,9 @@ Lemma exit_if_false_true: exec_stmt tprog te m1 ts t m2 Out_normal. Proof. intros. monadInv H. rewrite <- H5. - eapply exec_Sifthenelse_false with (v1 := Vfalse). - eapply make_notbool_correct with (va := v); eauto. - inversion H3; subst; simpl; auto. - rewrite Int.eq_false; auto. - rewrite Int.eq_false; auto. - rewrite Float.eq_zero_false; auto. - simpl; auto. + exploit make_boolean_correct_true. eapply H0; eauto. eauto. + intros [vb [EVAL ISTRUE]]. + eapply exec_Sifthenelse_true with (v1 := vb); eauto. constructor. traceEq. Qed. @@ -945,11 +941,9 @@ Lemma exit_if_false_false: exec_stmt tprog te m1 ts t m2 (Out_exit 0). Proof. intros. monadInv H. rewrite <- H5. - eapply exec_Sifthenelse_true with (v1 := Vtrue). - eapply make_notbool_correct with (va := v); eauto. - inversion H3; subst; simpl; auto. - rewrite Float.eq_zero_true; auto. - simpl; apply Int.one_not_zero. + exploit make_boolean_correct_false. eapply H0; eauto. eauto. + intros [vb [EVAL ISFALSE]]. + eapply exec_Sifthenelse_false with (v1 := vb); eauto. constructor. traceEq. Qed. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 979d0bc..f9463e6 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -29,8 +29,9 @@ Inductive type : Set := | Tpointer: type -> type | Tarray: type -> Z -> type | Tfunction: typelist -> type -> type - | Tstruct: fieldlist -> type - | Tunion: fieldlist -> type + | Tstruct: ident -> fieldlist -> type + | Tunion: ident ->fieldlist -> type + | Tcomp_ptr: ident -> type with typelist : Set := | Tnil: typelist @@ -164,8 +165,9 @@ Fixpoint alignof (t: type) : Z := | Tpointer _ => 4 | Tarray t' n => alignof t' | Tfunction _ _ => 1 - | Tstruct fld => alignof_fields fld - | Tunion fld => alignof_fields fld + | Tstruct _ fld => alignof_fields fld + | Tunion _ fld => alignof_fields fld + | Tcomp_ptr _ => 4 end with alignof_fields (f: fieldlist) : Z := @@ -208,8 +210,9 @@ Fixpoint sizeof (t: type) : Z := | Tpointer _ => 4 | Tarray t' n => sizeof t' * Zmax 1 n | Tfunction _ _ => 1 - | Tstruct fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) - | Tunion fld => align (Zmax 1 (sizeof_union fld)) (alignof t) + | Tstruct _ fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) + | Tunion _ fld => align (Zmax 1 (sizeof_union fld)) (alignof t) + | Tcomp_ptr _ => 4 end with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := @@ -285,8 +288,9 @@ Definition access_mode (ty: type) : mode := | Tpointer _ => By_value Mint32 | Tarray _ _ => By_reference | Tfunction _ _ => By_reference - | Tstruct fList => By_nothing - | Tunion fList => By_nothing + | Tstruct _ fList => By_nothing + | Tunion _ fList => By_nothing + | Tcomp_ptr _ => By_value Mint32 end. (** Classification of arithmetic operations and comparisons *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 797033d..0795e1b 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -190,8 +190,12 @@ Fixpoint eq_type (t1 t2: type) {struct t1}: bool := eq_type u1 u2 && if zeq sz1 sz2 then true else false | Tfunction args1 res1, Tfunction args2 res2 => eq_typelist args1 args2 && eq_type res1 res2 - | Tstruct f1, Tstruct f2 => eq_fieldlist f1 f2 - | Tunion f1, Tunion f2 => eq_fieldlist f1 f2 + | Tstruct id1 f1, Tstruct id2 f2 => + if ident_eq id1 id2 then eq_fieldlist f1 f2 else false + | Tunion id1 f1, Tunion id2 f2 => + if ident_eq id1 id2 then eq_fieldlist f1 f2 else false + | Tcomp_ptr id1, Tcomp_ptr id2 => + if ident_eq id1 id2 then true else false | _, _ => false end @@ -239,8 +243,9 @@ Proof. decEq; auto. TrueInv. decEq; auto. TrueInv. decEq; auto. - decEq; auto. - decEq; auto. + TrueInv. subst i0. decEq; auto. + TrueInv. subst i0. decEq; auto. + TrueInv. congruence. auto. TrueInv. decEq; auto. auto. |