<NME> LLVMBuiltins.hs
<BEF> {- |
Module      : SAWScript.LLVMBuiltins
Description : Implementations of LLVM-related SAW-Script primitives.
License     : BSD3
Maintainer  : atomb
Stability   : provisional
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ConstraintKinds #-}
import Text.PrettyPrint.HughesPJ
import Text.Read (readMaybe)

import Text.LLVM ( modTypes, modGlobals, modDeclares, modDefines, modDataLayout
                 , defName, defRetType, defVarArgs, defArgs, defAttrs
                 , funLinkage, funGC
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative hiding (many)
#endif
import Data.String
import Data.Parameterized.Some
import Control.Monad.State (gets)

import qualified Text.LLVM.AST as LLVM
import qualified Data.LLVM.BitCode as LLVM
import qualified Text.LLVM.Parser as LLVM (parseType)

import SAWScript.Value as SV

import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (LLVMModule, loadLLVMModule)

llvm_load_module :: FilePath -> TopLevel (Some CMS.LLVMModule)
llvm_load_module file =
  do laxArith <- gets rwLaxArith
     debugIntrinsics <- gets rwDebugIntrinsics
     let ?transOpts = CL.defaultTranslationOptions
                        { CL.laxArith = laxArith
                        , CL.debugIntrinsics = debugIntrinsics
                        }
     halloc <- getHandleAlloc
     io (CMS.loadLLVMModule file halloc) >>= \case
       Left err -> fail (LLVM.formatError err)
       Right llvm_mod -> return llvm_mod

llvm_type :: String -> TopLevel LLVM.Type
llvm_type str =
  case LLVM.parseType str of
    Left e -> fail (show e)
    Right t -> return t

llvm_int :: Int -> LLVM.Type
llvm_int n = LLVM.PrimType (LLVM.Integer (fromIntegral n))

llvm_float :: LLVM.Type
llvm_float = LLVM.PrimType (LLVM.FloatType LLVM.Float)

llvm_double :: LLVM.Type
llvm_double = LLVM.PrimType (LLVM.FloatType LLVM.Double)

llvm_array :: Int -> LLVM.Type -> LLVM.Type
llvm_array n t = LLVM.Array (fromIntegral n) t

llvm_alias :: String -> LLVM.Type
llvm_alias n = LLVM.Alias (fromString n)

llvm_packed_struct_type :: [LLVM.Type] -> LLVM.Type
llvm_packed_struct_type = LLVM.PackedStruct

llvm_pointer :: LLVM.Type -> LLVM.Type
llvm_pointer = LLVM.PtrTo

llvm_struct_type :: [LLVM.Type] -> LLVM.Type
llvm_struct_type = LLVM.Struct
  let dl = parseDataLayout $ modDataLayout mdl
      sym = Symbol func
  withBE $ \be -> do
    (sbe, mem, scLLVM) <- createSAWBackend' be dl
    (_warnings, cb) <- mkCodebase sbe dl mdl
    -- TODO: Print warnings from codebase.
    case lookupDefine sym cb of
  let pos = fixPos -- TODO
      dl = parseDataLayout $ modDataLayout mdl
  withBE $ \be -> do
    (sbe, mem, scLLVM) <- createSAWBackend' be dl
    (_warnings, cb) <- mkCodebase sbe dl mdl
    let ms0 = initLLVMMethodSpec pos cb func
        lsctx0 = LLVMSetupState {

<MSG> Allow LSS to run in context of add'l imports
<DFF> @@ -14,6 +14,8 @@ import Data.String
 import Text.PrettyPrint.HughesPJ
 import Text.Read (readMaybe)
 
+import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
+
 import Text.LLVM ( modTypes, modGlobals, modDeclares, modDefines, modDataLayout
                  , defName, defRetType, defVarArgs, defArgs, defAttrs
                  , funLinkage, funGC
@@ -86,7 +88,7 @@ extractLLVM sc (LLVMModule file mdl) func _setup = do
   let dl = parseDataLayout $ modDataLayout mdl
       sym = Symbol func
   withBE $ \be -> do
-    (sbe, mem, scLLVM) <- createSAWBackend' be dl
+    (sbe, mem, scLLVM) <- createSAWBackend' be dl []
     (_warnings, cb) <- mkCodebase sbe dl mdl
     -- TODO: Print warnings from codebase.
     case lookupDefine sym cb of
@@ -143,7 +145,7 @@ verifyLLVM bic opts (LLVMModule file mdl) func overrides setup = do
   let pos = fixPos -- TODO
       dl = parseDataLayout $ modDataLayout mdl
   withBE $ \be -> do
-    (sbe, mem, scLLVM) <- createSAWBackend' be dl
+    (sbe, mem, scLLVM) <- createSAWBackend' be dl [CryptolSAW.cryptolModule]
     (_warnings, cb) <- mkCodebase sbe dl mdl
     let ms0 = initLLVMMethodSpec pos cb func
         lsctx0 = LLVMSetupState {

{'addition_count': 4, 'commit_subject': "Allow LSS to run in context of add'l imports", 'deletion_count': 2, 'file_extension': '.hs', 'lang': 'hs', 'license': 'bsd-3-clause', 'repo_name': 'GaloisInc/saw-script'}