Value analysis: keep track of pointer values that leak through small integers with Uns or Sgn abstract values.

This is a follow-up to commit 2932b53.  It adds provenance tracking to the Uns and Sgn abstract values.

2 files changed, 21 insertions, 21 deletions

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 4f4bf5aa..872493a6 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -96,12 +96,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
 Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
   match c, args, vl with
   | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
-      if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
-      else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
       else make_cmp_base c args vl
   | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
-      if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
-      else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+      if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+      else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
       else make_cmp_base c args vl
   | _, _, _ =>
       make_cmp_base c args vl
@@ -164,7 +164,7 @@ Definition make_divuimm (n: int) (r1 r2: reg) :=
 Definition make_andimm (n: int) (r: reg) (a: aval) :=
   if Int.eq n Int.zero then (Ointconst Int.zero, nil)
   else if Int.eq n Int.mone then (Omove, r :: nil)
-  else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero
+  else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero
                      | _ => false end
   then (Omove, r :: nil)
   else (Oandimm n, r :: nil).
@@ -190,9 +190,9 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) :=
   else (Omulfs, r1 :: r2 :: nil).
 
 Definition make_cast8signed (r: reg) (a: aval) :=
-  if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil).
+  if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil).
 Definition make_cast16signed (r: reg) (a: aval) :=
-  if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
+  if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
 
 Nondetfunction op_strength_reduction 
               (op: operation) (args: list reg) (vl: list aval) :=
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 597c9602..fa20d17e 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -163,24 +163,24 @@ Lemma make_cmp_correct:
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros c args vl.
-  assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+  assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true ->
              rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
-  { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+  { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
   unfold make_cmp. case (make_cmp_match c args vl); intros.
-- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
   simpl in H; inv H. InvBooleans. subst n. 
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
-  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
   simpl in H; inv H. InvBooleans. subst n. 
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
-- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
   simpl in H; inv H. InvBooleans. subst n. 
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
-  destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+  destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
   simpl in H; inv H. InvBooleans. subst n. 
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
@@ -302,7 +302,7 @@ Proof.
   subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
-  destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
+  destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                        | _ => false end) eqn:UNS.
   destruct x; try congruence. 
   exists (rs#r); split; auto.
@@ -313,7 +313,7 @@ Proof.
   rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
   rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
   rewrite Int.bits_not by auto. apply negb_involutive. 
-  rewrite H5 by auto. auto. 
+  rewrite H6 by auto. auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
@@ -404,11 +404,11 @@ Lemma make_cast8signed_correct:
   let (op, args) := make_cast8signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
 Proof.
-  intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. 
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. 
   exists rs#r; split; auto. 
-  assert (V: vmatch bc rs#r (Sgn 8)).
+  assert (V: vmatch bc rs#r (Sgn Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
-  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
   econstructor; split; simpl; eauto.
 Qed.
 
@@ -418,11 +418,11 @@ Lemma make_cast16signed_correct:
   let (op, args) := make_cast16signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
 Proof.
-  intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. 
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. 
   exists rs#r; split; auto. 
-  assert (V: vmatch bc rs#r (Sgn 16)).
+  assert (V: vmatch bc rs#r (Sgn Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
-  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
   econstructor; split; simpl; eauto.
 Qed.