In Clight, revised handling of comparisons between pointers and 0

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

cfrontend/Csem.v

@@ -266,35 +266,30 @@ Function sem_cmp (c:comparison)
   match classify_cmp t1 t2 with
   | cmp_case_I32unsi =>
       match v1,v2 with
-      | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmpu c n1 n2))
+      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | _,  _ => None
       end
-  | cmp_case_ii =>
-      match v1,v2 with
-      | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmp c n1 n2))
-      | _,  _ => None
-      end
-  | cmp_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 =>Some (Val.of_bool (Float.cmp c f1 f2))  
-      | _,  _ => None
-      end
-  | cmp_case_pi =>
-      match v1,v2 with
-      | Vptr b ofs, Vint n2 =>
-          if Int.eq n2 Int.zero then sem_cmp_mismatch c else None
-      | _,  _ => None
-      end
-  | cmp_case_pp =>
+  | cmp_case_ipip =>
       match v1,v2 with
+      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b2 (Int.signed ofs2) then
+          if valid_pointer m b1 (Int.signed ofs1)
+          && valid_pointer m b2 (Int.signed ofs2) then
             if zeq b1 b2
             then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
             else None
           else None
+      | Vptr b ofs, Vint n =>
+          if Int.eq n Int.zero then sem_cmp_mismatch c else None
+      | Vint n, Vptr b ofs =>
+          if Int.eq n Int.zero then sem_cmp_mismatch c else None
       | _,  _ => None
-      end 
+      end
+  | cmp_case_ff =>
+      match v1,v2 with
+      | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))  
+      | _,  _ => None
+      end
   | cmp_default => None
   end.
 

cfrontend/Cshmgen.v

@@ -174,10 +174,8 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
   | cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2)
-  | cmp_case_ii => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_case_ipip => OK (Ebinop (Ocmp c) e1 e2)
   | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
-  | cmp_case_pi => OK (Ebinop (Ocmp c) e1 e2)
-  | cmp_case_pp => OK (Ebinop (Ocmp c) e1 e2)
   | cmp_default => Error (msg "Cshmgen.make_shr")
   end.
 

cfrontend/Cshmgenproof2.v

@@ -285,15 +285,24 @@ Lemma make_cmp_correct:
   eval_expr tprog e m c v.
 Proof.
   intros until m. intro SEM. unfold make_cmp.
-  functional inversion SEM; rewrite H0; intros. 
-  inversion H8. eauto with cshm.
+  functional inversion SEM; rewrite H0; intros.
+  (* I32unsi *) 
   inversion H8. eauto with cshm.
+  (* ipip int int *)
   inversion H8. eauto with cshm.
-  inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. functional inversion H; subst; unfold eval_compare_null;
-  rewrite H8; auto.
+  (* ipip ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. rewrite H3. unfold eq_block; rewrite H9. auto.
+  simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
+  (* ipip ptr int *)
+  inversion H9. eapply eval_Ebinop; eauto with cshm.
+  simpl. unfold eval_compare_null. rewrite H8. 
+  functional inversion H; subst; auto.
+  (* ipip int ptr *)
+  inversion H9. eapply eval_Ebinop; eauto with cshm.
+  simpl. unfold eval_compare_null. rewrite H8. 
+  functional inversion H; subst; auto.
+  (* ff *)
+  inversion H8. eauto with cshm.
 Qed.
 
 Lemma transl_unop_correct:

cfrontend/Csyntax.v

@@ -466,24 +466,22 @@ Definition classify_shr (ty1: type) (ty2: type) :=
 
 Inductive classify_cmp_cases : Set:=
   | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
-  | cmp_case_ii: classify_cmp_cases  (**r int , int*)
+  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
   | cmp_case_ff: classify_cmp_cases  (**r float , float *)
-  | cmp_case_pi: classify_cmp_cases  (**r ptr or array , int *)
-  | cmp_case_pp:classify_cmp_cases   (**r ptr or array , ptr or array *)
   | cmp_default: classify_cmp_cases . (**r other *)
 
 Definition classify_cmp (ty1: type) (ty2: type) :=
   match ty1,ty2 with 
   | Tint I32 Unsigned , Tint _ _ => cmp_case_I32unsi 
   | Tint _ _ , Tint I32 Unsigned => cmp_case_I32unsi 
-  | Tint _ _ , Tint _ _ => cmp_case_ii 
+  | Tint _ _ , Tint _ _ => cmp_case_ipip
   | Tfloat _ , Tfloat _ => cmp_case_ff
-  | Tpointer _ , Tint _ _ => cmp_case_pi 
-  | Tarray _ _ , Tint _ _ => cmp_case_pi 
-  | Tpointer _ , Tpointer _ => cmp_case_pp
-  | Tpointer _ , Tarray _ _ => cmp_case_pp
-  | Tarray _ _ ,Tpointer _ => cmp_case_pp
-  | Tarray _ _ ,Tarray _ _ => cmp_case_pp
+  | Tpointer _ , Tint _ _ => cmp_case_ipip
+  | Tarray _ _ , Tint _ _ => cmp_case_ipip
+  | Tpointer _ , Tpointer _ => cmp_case_ipip
+  | Tpointer _ , Tarray _ _ => cmp_case_ipip
+  | Tarray _ _ ,Tpointer _ => cmp_case_ipip
+  | Tarray _ _ ,Tarray _ _ => cmp_case_ipip
   | _ , _ => cmp_default
   end.