From 849cf541d32fffcbf21e950e0a01f86d062d0d91 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Thu, 20 Aug 2020 16:26:11 -0400 Subject: [PATCH 1/7] WIP: Temporarily add RAX to callee-saved registers --- deps/macaw | 2 +- src/SAWScript/Crucible/LLVM/X86.hs | 12 +++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/deps/macaw b/deps/macaw index 6a83d23989..bb68256484 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 6a83d23989a44eb7b57b411e7fb2c425d2d95565 +Subproject commit bb682564846fbb6b738c2f11b49f30d6f21f76dc diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 66bcdb10c9..ba456d6e6e 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -360,10 +360,16 @@ buildCFG opts halloc path nm = do _ -> fail $ mconcat ["Could not find symbol \"", nm, "\""] printOutLn opts Info $ mconcat ["Found symbol at address ", show addr, ", building CFG"] let + preservedRegs = Set.insert (Some Macaw.RAX) Macaw.x86CalleeSavedRegs + preserveFn r = Set.member (Some r) preservedRegs + macawCallParams = Macaw.x86_64CallParams { Macaw.preserveReg = preserveFn } + macawArchInfo = (Macaw.x86_64_info preserveFn) + { Macaw.archCallParams = macawCallParams + } initialDiscoveryState = - Macaw.emptyDiscoveryState (memory relf) (funSymMap relf) Macaw.x86_64_linux_info + Macaw.emptyDiscoveryState (memory relf) (funSymMap relf) macawArchInfo + -- "inline" any function addresses that we happen to jump to & Macaw.trustedFunctionEntryPoints .~ Set.empty - let finalState = Macaw.cfgFromAddrsAndState initialDiscoveryState [addr] [] finfos = finalState ^. Macaw.funInfo cfgs <- forM finfos $ \(Some finfo) -> @@ -470,7 +476,7 @@ initialState sym opts sc cc elf relf ms globs maxAddr = do , globalEnd . fst <$> globs , allocGlobalEnd <$> ms ^. MS.csGlobalAllocs ] - (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Immutable + (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Mutable "globals" emptyMem sz align pure $ X86State { _x86Sym = sym From 568349492fe774f415db86595c15360665869987 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 31 Aug 2020 23:10:20 -0400 Subject: [PATCH 2/7] WIP: Bump Flexdis and Macaw, support more uninterpreted instructions --- deps/flexdis86 | 2 +- src/SAWScript/Crucible/LLVM/X86.hs | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/deps/flexdis86 b/deps/flexdis86 index 1d88cb56f6..640e4c870a 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 1d88cb56f611713605f4c236beaebbcd80a3efa0 +Subproject commit 640e4c870a1edcedabda4a5ef8cb89be281e06fb diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index ba456d6e6e..844eab7b50 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -220,8 +220,12 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl cenv <- rwCryptol <$> getTopLevelRW liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesEnc sfs) $ cryptolUninterpreted cenv "aesenc" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted cenv "aesenclast" + liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDec sfs) $ cryptolUninterpreted cenv "aesdec" + liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDecLast sfs) $ cryptolUninterpreted cenv "aesdeclast" + liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnClMul sfs) $ cryptolUninterpreted cenv "clmul" (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc path nm + liftIO $ print cfg addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] From 3be1f3b0dc47d6543597fedd3458f9f7df4fc3f9 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Tue, 8 Sep 2020 15:42:45 -0400 Subject: [PATCH 3/7] WIP --- src/SAWScript/Crucible/LLVM/X86.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 844eab7b50..e143389e09 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -222,10 +222,10 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted cenv "aesenclast" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDec sfs) $ cryptolUninterpreted cenv "aesdec" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDecLast sfs) $ cryptolUninterpreted cenv "aesdeclast" + liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesKeyGenAssist sfs) $ cryptolUninterpreted cenv "aeskeygenassist" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnClMul sfs) $ cryptolUninterpreted cenv "clmul" (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc path nm - liftIO $ print cfg addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] @@ -800,6 +800,7 @@ assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptexpected) = do ptr <- resolvePtrSetupValue env tyenv tptr memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected storTy <- liftIO $ C.LLVM.toStorableType memTy + actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment pure $ LO.matchArg opts sc cc ms MS.PostState actual memTy texpected From 9a6f9488eecc1dbaa089abebad683c4b46dd43b2 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Sun, 11 Oct 2020 12:54:39 -0400 Subject: [PATCH 4/7] x86: Allow user to specify additional preserved registers --- src/SAWScript/Crucible/LLVM/X86.hs | 35 ++++++++++++++++++++++++++---- src/SAWScript/Interpreter.hs | 21 ++++++++++++++++++ src/SAWScript/Value.hs | 1 + 3 files changed, 53 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index e143389e09..a357b86885 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -39,8 +39,10 @@ import Data.Foldable (foldlM) import qualified Data.List.NonEmpty as NE import qualified Data.Vector as Vector import qualified Data.Text as Text +import Data.Text (Text) import Data.Text.Encoding (decodeUtf8, encodeUtf8) import qualified Data.Set as Set +import Data.Set (Set) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe @@ -170,6 +172,27 @@ getReg reg regs = case Macaw.lookupX86Reg reg regs of Just (C.RV val) -> pure val Nothing -> throwX86 $ mconcat ["Invalid register: ", show reg] +-- TODO: extend to more than general purpose registers +stringToReg :: Text -> Maybe (Some Macaw.X86Reg) +stringToReg s = case s of + "rax" -> Just $ Some Macaw.RAX + "rbx" -> Just $ Some Macaw.RBX + "rcx" -> Just $ Some Macaw.RCX + "rdx" -> Just $ Some Macaw.RDX + "rsp" -> Just $ Some Macaw.RSP + "rbp" -> Just $ Some Macaw.RBP + "rsi" -> Just $ Some Macaw.RSI + "rdi" -> Just $ Some Macaw.RDI + "r8" -> Just $ Some Macaw.R8 + "r9" -> Just $ Some Macaw.R9 + "r10" -> Just $ Some Macaw.R10 + "r11" -> Just $ Some Macaw.R11 + "r12" -> Just $ Some Macaw.R12 + "r13" -> Just $ Some Macaw.R13 + "r14" -> Just $ Some Macaw.R14 + "r15" -> Just $ Some Macaw.R15 + _ -> Nothing + cryptolUninterpreted :: (MonadIO m, MonadThrow m) => CryptolEnv -> @@ -217,7 +240,8 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule sfs <- liftIO $ Macaw.newSymFuns sym - cenv <- rwCryptol <$> getTopLevelRW + rw <- getTopLevelRW + let cenv = rwCryptol rw liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesEnc sfs) $ cryptolUninterpreted cenv "aesenc" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted cenv "aesenclast" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDec sfs) $ cryptolUninterpreted cenv "aesdec" @@ -225,7 +249,8 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesKeyGenAssist sfs) $ cryptolUninterpreted cenv "aeskeygenassist" liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnClMul sfs) $ cryptolUninterpreted cenv "clmul" - (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc path nm + let preserved = Set.fromList . catMaybes $ stringToReg . Text.toLower . Text.pack <$> rwPreservedRegs rw + (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc preserved path nm addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] @@ -338,6 +363,7 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl buildCFG :: Options -> C.HandleAllocator -> + Set (Some Macaw.X86Reg) {- ^ Registers to treat as callee-saved -} -> String {- ^ Path to ELF file -} -> String {- ^ Function's symbol in ELF file -} -> IO ( C.SomeCFG @@ -354,7 +380,7 @@ buildCFG :: (EmptyCtx ::> Macaw.ArchRegStruct Macaw.X86_64) (Macaw.ArchRegStruct Macaw.X86_64)) ) -buildCFG opts halloc path nm = do +buildCFG opts halloc preserved path nm = do printOutLn opts Info $ mconcat ["Finding symbol for \"", nm, "\""] elf <- getElf path relf <- getRelevant elf @@ -364,7 +390,8 @@ buildCFG opts halloc path nm = do _ -> fail $ mconcat ["Could not find symbol \"", nm, "\""] printOutLn opts Info $ mconcat ["Found symbol at address ", show addr, ", building CFG"] let - preservedRegs = Set.insert (Some Macaw.RAX) Macaw.x86CalleeSavedRegs + preservedRegs = Set.union preserved Macaw.x86CalleeSavedRegs + preserveFn :: forall t. Macaw.X86Reg t -> Bool preserveFn r = Set.member (Some r) preservedRegs macawCallParams = Macaw.x86_64CallParams { Macaw.preserveReg = preserveFn } macawArchInfo = (Macaw.x86_64_info preserveFn) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index ddd7f9d671..0db2d1e145 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -434,6 +434,7 @@ buildTopLevelEnv proxy opts = , rwProfilingFile = Nothing , rwLaxArith = False , rwWhat4HashConsing = False + , rwPreservedRegs = [] } return (bic, ro0, rw0) @@ -508,6 +509,16 @@ disable_what4_hash_consing = do rw <- getTopLevelRW putTopLevelRW rw { rwWhat4HashConsing = False } +add_x86_preserved_reg :: String -> TopLevel () +add_x86_preserved_reg r = do + rw <- getTopLevelRW + putTopLevelRW rw { rwPreservedRegs = r:rwPreservedRegs rw } + +default_x86_preserved_reg :: TopLevel () +default_x86_preserved_reg = do + rw <- getTopLevelRW + putTopLevelRW rw { rwPreservedRegs = [] } + include_value :: FilePath -> TopLevel () include_value file = do oldpath <- io $ getCurrentDirectory @@ -2203,6 +2214,16 @@ primitives = Map.fromList , "that can be used as an override when verifying other LLVM functions." ] + , prim "add_x86_preserved_reg" "String -> TopLevel ()" + (pureVal add_x86_preserved_reg) + Current + [ "Treat the given register as callee-saved during x86 verification." ] + + , prim "default_x86_preserved_reg" "TopLevel ()" + (pureVal default_x86_preserved_reg) + Current + [ "Use the default set of callee-saved registers during x86 verification.." ] + , prim "crucible_array" "[SetupValue] -> SetupValue" (pureVal CIR.anySetupArray) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index c4ef2ec22a..de846bb81e 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -409,6 +409,7 @@ data TopLevelRW = , rwProfilingFile :: Maybe FilePath , rwLaxArith :: Bool , rwWhat4HashConsing :: Bool + , rwPreservedRegs :: [String] } newtype TopLevel a = From 487ed2a3e51c430bd7eebc0fdb10485e8f12b005 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Sun, 11 Oct 2020 13:10:12 -0400 Subject: [PATCH 5/7] x86: Ensure global memory is immutable --- src/SAWScript/Crucible/LLVM/X86.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index a357b86885..7b5389a9b8 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -507,7 +507,7 @@ initialState sym opts sc cc elf relf ms globs maxAddr = do , globalEnd . fst <$> globs , allocGlobalEnd <$> ms ^. MS.csGlobalAllocs ] - (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Mutable + (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Immutable "globals" emptyMem sz align pure $ X86State { _x86Sym = sym From a89a21a2b41e809e6411903dcad677317ca98390 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 12 Oct 2020 14:35:01 -0400 Subject: [PATCH 6/7] Update deps --- deps/flexdis86 | 2 +- deps/macaw | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/flexdis86 b/deps/flexdis86 index 640e4c870a..e8b6c38a65 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 640e4c870a1edcedabda4a5ef8cb89be281e06fb +Subproject commit e8b6c38a6590e65efa0255124993a61f9f68c3ec diff --git a/deps/macaw b/deps/macaw index bb68256484..3a071e317b 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit bb682564846fbb6b738c2f11b49f30d6f21f76dc +Subproject commit 3a071e317b456515a1d193bd5180a9127700c408 From beafc24885ddf9324b07cf90160c8f4449bf4510 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 12 Oct 2020 17:02:07 -0400 Subject: [PATCH 7/7] Add integration test --- intTests/test_llvm_x86_06/test.S | 14 ++++++++++++++ intTests/test_llvm_x86_06/test.c | 8 ++++++++ intTests/test_llvm_x86_06/test.saw | 13 +++++++++++++ intTests/test_llvm_x86_06/test.sh | 7 +++++++ 4 files changed, 42 insertions(+) create mode 100644 intTests/test_llvm_x86_06/test.S create mode 100644 intTests/test_llvm_x86_06/test.c create mode 100644 intTests/test_llvm_x86_06/test.saw create mode 100755 intTests/test_llvm_x86_06/test.sh diff --git a/intTests/test_llvm_x86_06/test.S b/intTests/test_llvm_x86_06/test.S new file mode 100644 index 0000000000..b84a3ffeef --- /dev/null +++ b/intTests/test_llvm_x86_06/test.S @@ -0,0 +1,14 @@ +section .bss +section .text +foo: + ret +global discoverytest +discoverytest: + lea rax, [rsp] + call foo + lea rsp, [rax] + ret +global _start +_start: + mov rax, 60 + syscall diff --git a/intTests/test_llvm_x86_06/test.c b/intTests/test_llvm_x86_06/test.c new file mode 100644 index 0000000000..c53d0d4e9c --- /dev/null +++ b/intTests/test_llvm_x86_06/test.c @@ -0,0 +1,8 @@ +#include +#include + +extern void discoverytest(); + +void test() { + discoverytest(); +}; diff --git a/intTests/test_llvm_x86_06/test.saw b/intTests/test_llvm_x86_06/test.saw new file mode 100644 index 0000000000..e3c64e334d --- /dev/null +++ b/intTests/test_llvm_x86_06/test.saw @@ -0,0 +1,13 @@ +enable_experimental; + +m <- llvm_load_module "test.bc"; + +let discoverytest_setup = do { + crucible_execute_func []; +}; + +fails (crucible_llvm_verify_x86 m "./test" "discoverytest" [] false discoverytest_setup w4); + +add_x86_preserved_reg "rax"; +crucible_llvm_verify_x86 m "./test" "discoverytest" [] false discoverytest_setup w4; +default_x86_preserved_reg; \ No newline at end of file diff --git a/intTests/test_llvm_x86_06/test.sh b/intTests/test_llvm_x86_06/test.sh new file mode 100755 index 0000000000..79a0867031 --- /dev/null +++ b/intTests/test_llvm_x86_06/test.sh @@ -0,0 +1,7 @@ +#!/bin/sh +set -e + +yasm -felf64 test.S +ld test.o -o test +clang -c -emit-llvm test.c +$SAW test.saw