From 78f1b6a57c95ecc68c104d4764fc8d5851d7dd54 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 19 Jul 2015 12:11:37 +0200 Subject: 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. --- arm/ConstpropOp.vp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'arm/ConstpropOp.vp') 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) := -- cgit