GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-29 00:59:09 +03:00
Code Issues Projects Releases Wiki Activity

adding two finsets, get a finset

Browse Source
This commit is contained in:
Daniel Wagner 2018-05-24 11:52:30 -04:00
parent d0d30f038d
commit fa96a062e1
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
base/src/Data/Macaw/AbsDomain/AbsState.hs
View File

@ -614,6 +614,15 @@ bvadc w (FinSet t) (StackOffset a s) c
, BoolConst b <- c , BoolConst b <- c
, o <- if b then o0 + 1 else o0 = , o <- if b then o0 + 1 else o0 =
StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s
-- Two finite sets
bvadc w (FinSet l) (FinSet r) (BoolConst b)
| ls <- Set.toList l
, rs <- Set.toList r
= case Set.fromList [bottomBits $ lval+rval+if b then 1 else 0 | lval <- ls, rval <- rs] of
s | Set.size s <= maxSetSize -> FinSet s
_ -> TopV
where
bottomBits v = v .&. (bit (fromInteger (natValue w)) - 1)
-- Strided intervals -- Strided intervals
bvadc w v v' c bvadc w v v' c
| StridedInterval si1 <- v, StridedInterval si2 <- v' = go si1 si2 | StridedInterval si1 <- v, StridedInterval si2 <- v' = go si1 si2