GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-12-01 20:23:10 +03:00
Code Issues Projects Releases Wiki Activity

Fix some cases where domain values could overflow their bitwidth.

Browse Source
This commit is contained in:
Rob Dockins 2020-04-16 10:06:58 -07:00 committed by robdockins
parent fcd94ded6e
commit 2037458461
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
what4/src/What4/Utils/BVDomain/Arith.hs
View File

@ -595,7 +595,7 @@ not a =
case a of
BVDAny _ -> a
BVDInterval mask al aw ->
BVDInterval mask (ah `Bits.xor` mask) aw
BVDInterval mask (complement ah .&. mask) aw
where ah = al + aw
-- | Return bitwise bounds for domain (i.e. logical AND of all
@ -617,7 +617,7 @@ bitbounds a =
-- @lo..hi@.
unknowns :: Domain w -> Integer
unknowns (BVDAny mask) = mask
unknowns (BVDInterval _mask al aw) = fillright 1 (al `Bits.xor` (al+aw))
unknowns (BVDInterval mask al aw) = mask .&. (fillright 1 (al `Bits.xor` (al+aw)))
where
-- @fillright 1 x@ rounds up @x@ to the nearest 2^n-1.
fillright :: Int -> Integer -> Integer