GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 23:32:15 +03:00
Code Issues Projects Releases Wiki Activity

Minor fixes.

Browse Source
This commit is contained in:
Andrei Stefanescu 2018-09-18 21:43:52 -07:00
parent 32961d20cb
commit 1c002f160b
3 changed files with 3 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs
View File

@ -25,8 +25,6 @@ import qualified Data.IORef as IO
import qualified Data.Map.Strict as M
import Data.Parameterized.Classes ( (:~:)( Refl ), testEquality )
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.NatRepr as NR
import qualified Data.Text as Text
import Text.Printf ( printf )
import qualified Lang.Crucible.Backend as C
@ -277,7 +275,6 @@ funcSemantics sf pf s =
return (ptrVal, s)
MP.FP2 name v1 v2 fpscr -> do
let sym = s ^. C.stateSymInterface
name' <- C.stringLit sym $ Text.pack ("fp_" ++ name)
v1' <- toValBV sym v1
v2' <- toValBV sym v2
fpscr' <- toValBV sym fpscr
@ -287,7 +284,6 @@ funcSemantics sf pf s =
return (ptrVal, s)
MP.FP3 name v1 v2 v3 fpscr -> do
let sym = s ^. C.stateSymInterface
name' <- C.stringLit sym $ Text.pack name
v1' <- toValBV sym v1
v2' <- toValBV sym v2
v3' <- toValBV sym v3
@ -298,7 +294,6 @@ funcSemantics sf pf s =
return (ptrVal, s)
MP.Vec1 name v fpscr -> do
let sym = s ^. C.stateSymInterface
name' <- C.stringLit sym $ Text.pack name
v' <- toValBV sym v
fpscr' <- toValBV sym fpscr
let args = Ctx.extend (Ctx.extend Ctx.empty v') fpscr'
@ -307,7 +302,6 @@ funcSemantics sf pf s =
return (ptrVal, s)
MP.Vec2 name v1 v2 fpscr -> do
let sym = s ^. C.stateSymInterface
name' <- C.stringLit sym $ Text.pack name
v1' <- toValBV sym v1
v2' <- toValBV sym v2
fpscr' <- toValBV sym fpscr
@ -317,7 +311,6 @@ funcSemantics sf pf s =
return (ptrVal, s)
MP.Vec3 name v1 v2 v3 fpscr -> do
let sym = s ^. C.stateSymInterface
name' <- C.stringLit sym $ Text.pack name
v1' <- toValBV sym v1
v2' <- toValBV sym v2
v3' <- toValBV sym v3

2
macaw-ppc/src/Data/Macaw/PPC/Arch.hs
View File

@ -416,7 +416,7 @@ instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc v)
FPFMA fi _ _ _ _ -> MT.FloatTypeRepr fi
FPLt{} -> knownRepr
FPEq{} -> knownRepr
FPLt{} -> knownRepr
FPLe{} -> knownRepr
FPIsNaN{} -> knownRepr
FPCast fi _ _ -> MT.FloatTypeRepr fi
FPRound fi _ _ -> MT.FloatTypeRepr fi

2
macaw-ppc/src/Data/Macaw/PPC/Eval.hs
View File

@ -110,8 +110,10 @@ absEvalArchFn _ _r = \case
FPFMA{} -> MA.TopV
FPLt{} -> MA.TopV
FPEq{} -> MA.TopV
FPLe{} -> MA.TopV
FPIsNaN{} -> MA.TopV
FPCast{} -> MA.TopV
FPRound{} -> MA.TopV
FPToBinary{} -> MA.TopV
FPFromBinary{} -> MA.TopV
FPToSBV{} -> MA.TopV