GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-24 14:42:23 +03:00
Code Issues Projects Releases Wiki Activity

Add a translation for the undefined value from semmc

Browse Source
This commit is contained in:
Tristan Ravitch 2017-11-21 23:37:17 -08:00
parent 3b763bf347
commit 18d5ac3fe4
2 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -36,6 +36,7 @@ import qualified Data.Parameterized.ShapedList as SL
import Data.Parameterized.Some ( Some(..) )
import qualified Data.Parameterized.TraversableFC as FC
import Data.Parameterized.Witness ( Witness(..) )
import qualified Lang.Crucible.BaseTypes as CT
import qualified Lang.Crucible.Solver.Interface as SI
import qualified Lang.Crucible.Solver.SimpleBuilder as S
import qualified Lang.Crucible.Solver.SimpleBackend as S
@ -472,6 +473,11 @@ evalNonceAppTH bvi nonceApp =
locExp <- addEltTH bvi loc
liftQ [| addExpr (AppExpr (M.PopCount (NR.knownNat @64) $(return locExp))) |]
_ -> fail ("Unsupported argument list for popcnt: " ++ showF args)
"undefined" -> do
case S.nonceAppType nonceApp of
CT.BaseBVRepr n ->
liftQ [| M.AssignedValue <$> addAssignment (M.SetUndefined (M.BVTypeRepr $(natReprTH n))) |]
nt -> fail ("Invalid type for undefined: " ++ show nt)
_ | Just nBytes <- readMemBytes fnName -> do
case FC.toListFC Some args of
[_, Some addrElt] -> do

2
submodules/semmc

@ -1 +1 @@
Subproject commit 6a48bfafe3a1c3992904a4c2b782af32f5672bb9
Subproject commit 44e45f2e58b47c171e31c8ccc272c8b9dbd7fdd9