diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 28 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 8 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 2 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 15 |
4 files changed, 46 insertions, 7 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 71328c71..b919c1d4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -572,6 +572,7 @@ let z_of_str hex str fst = done; !res + let checkFloatOverflow f = match f with | Fappli_IEEE.B754_finite _ -> () @@ -897,6 +898,28 @@ let rec groupSwitch = function let (fst, cases) = groupSwitch rem in (Cutil.sseq s.sloc s fst, cases) +(* Test whether the statement contains case and give an *) +let rec contains_case s = + match s.sdesc with + | C.Sskip + | C.Sdo _ + | C.Sbreak + | C.Scontinue + | C.Sswitch _ (* Stop at a switch *) + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ + | C.Sasm _ -> () + | C.Sseq (s1,s2) + | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 + | C.Swhile (_,s1) + | C.Sdowhile (s1,_) -> contains_case s1 + | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 + | C.Slabeled(C.Scase _, _) -> + unsupported "'case' outside of 'switch'" + | C.Slabeled(_,s) -> contains_case s + | C.Sblock b -> List.iter contains_case b + (** Annotations for line numbers *) let add_lineno prev_loc this_loc s = @@ -953,7 +976,10 @@ let rec convertStmt ploc env s = | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in if init.sdesc <> C.Sskip then - warning "ignored code at beginning of 'switch'"; + begin + warning "ignored code at beginning of 'switch'"; + contains_case init + end; let te = convertExpr env e in add_lineno ploc s.sloc (swrap (Ctyping.sswitch te diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 6284660c..948ccaca 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -709,8 +709,10 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) match v1,v2 with | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then - if Int.eq (Int.repr (sizeof cenv ty)) Int.zero then None - else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof cenv ty)))) + let sz := sizeof cenv ty in + if zlt 0 sz && zle sz Int.max_signed + then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz))) + else None else None | _, _ => None end @@ -1216,7 +1218,7 @@ Proof. + inv H0; inv H1; inv H. TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. - destruct (Int.eq (Int.repr (sizeof cenv ty)) Int.zero); inv H3. + destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cb83731a..a80f4c15 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -260,7 +260,7 @@ Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in - OK (Ebinop Odivu (Ebinop Osub e1 e2) n) + OK (Ebinop Odiv (Ebinop Osub e1 e2) n) | sub_case_pl ty => let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 025d7b66..c69d0c0a 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -490,8 +490,19 @@ Proof. destruct (classify_sub tya tyb); inv MAKE. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM. - destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ce ty)) Int.zero) eqn:E; inv H0. - econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. + destruct (eq_block b0 b1); try discriminate. + set (sz := sizeof ce ty) in *. + destruct (zlt 0 sz); try discriminate. + destruct (zle sz Int.max_signed); simpl in H0; inv H0. + econstructor; eauto with cshm. + rewrite dec_eq_true; simpl. + assert (E: Int.signed (Int.repr sz) = sz). + { apply Int.signed_repr. generalize Int.min_signed_neg; omega. } + predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. + rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. + predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. + rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. + rewrite andb_false_r; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. |