From f448a4ae9f32f2fec52941fe5ee757b3f84dcfa0 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Mon, 27 Aug 2018 13:34:46 -0700 Subject: [PATCH] Add symbolic semantics to PPC floats. --- .../src/Data/Macaw/PPC/Symbolic/Functions.hs | 187 +++++++++++++++++- 1 file changed, 184 insertions(+), 3 deletions(-) diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs index d81c4ee7..794d3fc1 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} @@ -34,6 +35,7 @@ import qualified Lang.Crucible.Simulator.RegMap as C import qualified Lang.Crucible.Simulator.SimError as C import qualified Lang.Crucible.Types as C import qualified What4.Interface as C +import qualified What4.InterpretedFloatingPoint as C import qualified What4.Symbol as C import qualified Data.Macaw.CFG as MC @@ -131,6 +133,136 @@ funcSemantics sf pf s = -- FIXME: Make sure that the semantics when rhs == 0 exactly match PowerPC. v <- LL.llvmPointer_bv sym =<< C.bvSdiv sym lhs' rhs' return (v, s) + MP.FPNeg (_ :: MT.FloatInfoRepr fi) x -> withSymFPUnOp s x $ \sym x' -> + C.iFloatNeg @_ @(MS.ToCrucibleFloatInfo fi) sym x' + MP.FPAbs (_ :: MT.FloatInfoRepr fi) x -> withSymFPUnOp s x $ \sym x' -> + C.iFloatAbs @_ @(MS.ToCrucibleFloatInfo fi) sym x' + MP.FPSqrt (_ :: MT.FloatInfoRepr fi) x -> withSymFPUnOp s x $ \sym x' -> + C.iFloatSqrt @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' + MP.FPAdd (_ :: MT.FloatInfoRepr fi) x y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatAdd @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' y' + MP.FPSub (_ :: MT.FloatInfoRepr fi) x y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatSub @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' y' + MP.FPMul (_ :: MT.FloatInfoRepr fi) x y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatMul @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' y' + MP.FPDiv (_ :: MT.FloatInfoRepr fi) x y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatDiv @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' y' + MP.FPFMA (_ :: MT.FloatInfoRepr fi) x y z -> withSym s $ \sym -> do + let x' = toValFloat sym x + let y' = toValFloat sym y + let z' = toValFloat sym z + C.iFloatFMA @_ @(MS.ToCrucibleFloatInfo fi) sym C.RNE x' y' z' + MP.FPLt (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi)) y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatLt @_ @(MS.ToCrucibleFloatInfo fi) sym x' y' + MP.FPEq (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi)) y -> + withSymFPBinOp s x y $ \sym x' y' -> + C.iFloatFpEq @_ @(MS.ToCrucibleFloatInfo fi) sym x' y' + MP.FPIsNaN (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi)) -> + withSymFPUnOp s x $ \sym x' -> + C.iFloatIsNaN @_ @(MS.ToCrucibleFloatInfo fi) sym x' + MP.FPCast fi (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi')) -> + withSymFPUnOp s x $ \sym x' -> + C.iFloatCast @_ @_ @(MS.ToCrucibleFloatInfo fi') + sym + (MS.floatInfoToCrucible fi) + C.RNE + x' + MP.FPToBinary fi x -> withSymFPUnOp s x $ \sym x' -> case fi of + MT.HalfFloatRepr -> + LL.llvmPointer_bv sym + =<< C.iFloatToBinary sym (MS.floatInfoToCrucible fi) x' + MT.SingleFloatRepr -> + LL.llvmPointer_bv sym + =<< C.iFloatToBinary sym (MS.floatInfoToCrucible fi) x' + MT.DoubleFloatRepr -> + LL.llvmPointer_bv sym + =<< C.iFloatToBinary sym (MS.floatInfoToCrucible fi) x' + MT.QuadFloatRepr -> + LL.llvmPointer_bv sym + =<< C.iFloatToBinary sym (MS.floatInfoToCrucible fi) x' + MT.X86_80FloatRepr -> + LL.llvmPointer_bv sym + =<< C.iFloatToBinary sym (MS.floatInfoToCrucible fi) x' + MP.FPFromBinary fi x -> withSymBVUnOp s x $ \sym x' -> case fi of + MT.HalfFloatRepr -> + C.iFloatFromBinary sym (MS.floatInfoToCrucible fi) x' + MT.SingleFloatRepr -> + C.iFloatFromBinary sym (MS.floatInfoToCrucible fi) x' + MT.DoubleFloatRepr -> + C.iFloatFromBinary sym (MS.floatInfoToCrucible fi) x' + MT.QuadFloatRepr -> + C.iFloatFromBinary sym (MS.floatInfoToCrucible fi) x' + MT.X86_80FloatRepr -> + C.iFloatFromBinary sym (MS.floatInfoToCrucible fi) x' + MP.FPToSBV w (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi)) -> + withSymFPUnOp s x $ \sym x' -> + LL.llvmPointer_bv sym + =<< C.iFloatToSBV @_ @_ @(MS.ToCrucibleFloatInfo fi) sym w C.RNE x' + MP.FPToUBV w (x :: A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi)) -> + withSymFPUnOp s x $ \sym x' -> + LL.llvmPointer_bv sym + =<< C.iFloatToBV @_ @_ @(MS.ToCrucibleFloatInfo fi) sym w C.RNE x' + MP.FPFromSBV fi x -> withSymBVUnOp s x $ \sym x' -> + C.iSBVToFloat sym (MS.floatInfoToCrucible fi) C.RNE x' + MP.FPFromUBV fi x -> withSymBVUnOp s x $ \sym x' -> + C.iBVToFloat sym (MS.floatInfoToCrucible fi) C.RNE x' + MP.FPCoerce (fi :: MT.FloatInfoRepr fi) (fi' :: MT.FloatInfoRepr fi') x -> + withSymFPUnOp s x $ \sym x' -> do + res <- C.iFloatCast @_ @_ @(MS.ToCrucibleFloatInfo fi') + sym + (MS.floatInfoToCrucible fi) + C.RNE + x' + cond <- C.iFloatEq @_ @(MS.ToCrucibleFloatInfo fi') sym x' + =<< C.iFloatCast @_ @_ @(MS.ToCrucibleFloatInfo fi) + sym + (MS.floatInfoToCrucible fi') + C.RNE + res + C.assert sym cond $ C.GenericSimError $ + "float precision loss: coercing from " + ++ show (MS.floatInfoToCrucible fi') + ++ " to " + ++ show (MS.floatInfoToCrucible fi) + return res + MP.FPSCR1 name x fpscr -> withSym s $ \sym -> do + x' <- toValBV sym x + fpscr' <- toValBV sym fpscr + LL.llvmPointer_bv sym =<< lookupApplySymFun sym sf name + (Ctx.empty + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @32)) + (Ctx.empty Ctx.:> x' Ctx.:> fpscr') + (C.BaseBVRepr (NR.knownNat @32)) + MP.FPSCR2 name x y fpscr -> withSym s $ \sym -> do + x' <- toValBV sym x + y' <- toValBV sym y + fpscr' <- toValBV sym fpscr + LL.llvmPointer_bv sym =<< lookupApplySymFun sym sf name + (Ctx.empty + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @32)) + (Ctx.empty Ctx.:> x' Ctx.:> y' Ctx.:> fpscr') + (C.BaseBVRepr (NR.knownNat @32)) + MP.FPSCR3 name x y z fpscr -> withSym s $ \sym -> do + x' <- toValBV sym x + y' <- toValBV sym y + z' <- toValBV sym z + fpscr' <- toValBV sym fpscr + LL.llvmPointer_bv sym =<< lookupApplySymFun sym sf name + (Ctx.empty + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @128) + Ctx.:> C.BaseBVRepr (NR.knownNat @32)) + (Ctx.empty Ctx.:> x' Ctx.:> y' Ctx.:> z' Ctx.:> fpscr') + (C.BaseBVRepr (NR.knownNat @32)) MP.FP1 name v fpscr -> do let sym = s ^. C.stateSymInterface v' <- toValBV sym v @@ -197,9 +329,6 @@ funcSemantics sf pf s = fval <- lookupApplySymFun sym sf name argTypes args rType ptrVal <- LL.llvmPointer_bv sym fval return (ptrVal, s) - MP.FPIsQNaN {} -> error "FPIsQNaN is not supported yet (unused?)" - MP.FPIsSNaN {} -> error "FPIsSNaN is not supported yet (unused?)" - MP.FPCvt {} -> error "FPCvt is not supported yet (unused?)" lookupApplySymFun :: (C.IsSymInterface sym) @@ -231,4 +360,56 @@ toValBV :: (C.IsSymInterface sym) -> IO (C.RegValue sym (C.BVType w)) toValBV sym (A.AtomWrapper x) = LL.projectLLVM_bv sym (C.regValue x) +toValFloat + :: (C.IsSymInterface sym) + => sym + -> A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi) + -> C.RegValue sym (MS.ToCrucibleType (MT.FloatType fi)) +toValFloat _ (A.AtomWrapper x) = C.regValue x + +withSym + :: (C.IsSymInterface sym) + => S ppc sym rtp bs r ctx + -> (sym -> IO a) + -> IO (a, S ppc sym rtp bs r ctx) +withSym s action = do + let sym = s ^. C.stateSymInterface + val <- action sym + return (val, s) + +withSymBVUnOp + :: (C.IsSymInterface sym) + => S ppc sym rtp bs r ctx + -> A.AtomWrapper (C.RegEntry sym) (MT.BVType w) + -> (sym -> C.RegValue sym (C.BVType w) -> IO a) + -> IO (a, S ppc sym rtp bs r ctx) +withSymBVUnOp s x action = withSym s $ \sym -> action sym =<< toValBV sym x + +withSymFPUnOp + :: (C.IsSymInterface sym) + => S ppc sym rtp bs r ctx + -> A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi) + -> ( sym + -> C.RegValue sym (MS.ToCrucibleType (MT.FloatType fi)) + -> IO a + ) + -> IO (a, S ppc sym rtp bs r ctx) +withSymFPUnOp s x action = withSym s $ \sym -> action sym $ toValFloat sym x + +withSymFPBinOp + :: (C.IsSymInterface sym) + => S ppc sym rtp bs r ctx + -> A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi) + -> A.AtomWrapper (C.RegEntry sym) (MT.FloatType fi) + -> ( sym + -> C.RegValue sym (MS.ToCrucibleType (MT.FloatType fi)) + -> C.RegValue sym (MS.ToCrucibleType (MT.FloatType fi)) + -> IO a + ) + -> IO (a, S ppc sym rtp bs r ctx) +withSymFPBinOp s x y action = withSym s $ \sym -> do + let x' = toValFloat sym x + let y' = toValFloat sym y + action sym x' y' + type S ppc sym rtp bs r ctx = C.CrucibleState (MS.MacawSimulatorState sym) sym (MS.MacawExt ppc) rtp bs r ctx