diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 12:11:37 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-19 12:11:37 +0200 |
| commit | 78f1b6a57c95ecc68c104d4764fc8d5851d7dd54 (patch) | |
| tree | 0c39dadd44f196baa0835ba525e7fb4246ebee3d /powerpc/ConstpropOp.vp | |
| parent | 2932b531ceff2cd4573714aeaeb9b4e537d36af8 (diff) | |
| download | compcert-kvx-78f1b6a57c95ecc68c104d4764fc8d5851d7dd54.tar.gz compcert-kvx-78f1b6a57c95ecc68c104d4764fc8d5851d7dd54.zip | |
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.
Diffstat (limited to 'powerpc/ConstpropOp.vp')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index bba0fad4..7265337d 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -52,12 +52,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 @@ -120,7 +120,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). @@ -146,9 +146,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) := |