diff --git a/CHANGES.md b/CHANGES.md index 9717a5fa5a..344d02bb69 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -95,6 +95,10 @@ on Windows at this time due to a downstream issue with CVC5 1.0.4 and earlier.) +* Add experimental support for verifying Rust programs. For more information, + see the `mir_*` commands documented in the + [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). + # Version 0.9 ## New Features diff --git a/README.md b/README.md index 6bd97dbba6..c8748ad3db 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,8 @@ This repository contains the code for SAWScript, the scripting language that forms the primary user interface to the Software Analysis Workbench (SAW). It provides the ability to reason about formal models describing the denotation of programs written in -languages such as C, Java, and Cryptol. +languages such as C, Java, and Cryptol. It also provides experimental, +incomplete support for the Rust language. ## Documentation diff --git a/doc/manual/manual.md b/doc/manual/manual.md index beb6047c2c..f34ed84e1c 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -5,7 +5,8 @@ mathematical models of the computational behavior of software, transforming these models, and proving properties about them. SAW can currently construct models of a subset of programs written in -Cryptol, LLVM (and therefore C), and JVM (and therefore Java). The +Cryptol, LLVM (and therefore C), and JVM (and therefore Java). SAW also has +experimental, incomplete support for MIR (and therefore Rust). The models take the form of typed functional programs, so in a sense SAW can be considered a translator from imperative programs to their functional equivalents. Various external proof tools, including a variety of SAT @@ -176,7 +177,7 @@ Cryptol, Haskell and ML. In particular, functions are applied by writing them next to their arguments rather than by using parentheses and commas. Rather than writing `f(x, y)`, write `f x y`. -Comments are written as in C and Java (among many other languages). All +Comments are written as in C, Java, and Rust (among many other languages). All text from `//` until the end of a line is ignored. Additionally, all text between `/*` and `*/` is ignored, regardless of whether the line ends. @@ -1568,6 +1569,8 @@ analyze JVM and LLVM programs. The first step in analyzing any code is to load it into the system. +## Loading LLVM + To load LLVM code, simply provide the location of a valid bitcode file to the `llvm_load_module` function. @@ -1583,6 +1586,8 @@ most likely case of incompleteness. We aim to support every version after 3.5, however, so report any parsing failures as [on GitHub](https://github.com/GaloisInc/saw-script/issues). +## Loading Java + Loading Java code is slightly more complex, because of the more structured nature of Java packages. First, when running `saw`, three flags control where to look for classes: @@ -1623,12 +1628,28 @@ unresolved issues in verifying code involving classes such as `String`. For more information on these issues, refer to [this GitHub issue](https://github.com/GaloisInc/crucible/issues/641). +## Loading MIR + +To load a piece of Rust code, first compile it to a MIR JSON file, as described +in [this section](#compiling-mir), and then provide the location of the JSON +file to the `mir_load_module` function: + +* `mir_load_module : String -> TopLevel MIRModule` + +SAW currently supports Rust code that can be built with a [March 22, 2020 Rust +nightly](https://static.rust-lang.org/dist/2020-03-22/). If you encounter a +Rust feature that SAW does not support, please report it [on +GitHub](https://github.com/GaloisInc/saw-script/issues). + ## Notes on Compiling Code for SAW -SAW will generally be able to load arbitrary LLVM bitcode and JVM -bytecode files, but several guidelines can help make verification -easier or more likely to succeed. For generating LLVM with `clang`, it -can be helpful to: +SAW will generally be able to load arbitrary LLVM bitcode, JVM bytecode, and +MIR JSON files, but several guidelines can help make verification easier or +more likely to succeed. + +### Compiling LLVM + +For generating LLVM with `clang`, it can be helpful to: * Turn on debugging symbols with `-g` so that SAW can find source locations of functions, names of variables, etc. @@ -1659,11 +1680,54 @@ behavior, and SAW currently does not have built in support for these functions (though you could manually create overrides for them in a verification script). +[^1]: https://clang.llvm.org/docs/UsersManual.html#controlling-code-generation + +### Compiling Java + For Java, the only compilation flag that tends to be valuable is `-g` to retain information about the names of function arguments and local variables. -[^1]: https://clang.llvm.org/docs/UsersManual.html#controlling-code-generation +### Compiling MIR + +In order to verify Rust code, SAW analyzes Rust's MIR (mid-level intermediate +representation) language. In particular, SAW analyzes a particular form of MIR +that the [`mir-json`](https://github.com/GaloisInc/mir-json) tool produces. You +will need to intall `mir-json` and run it on Rust code in order to produce MIR +JSON files that SAW can load (see [this section](#loading-mir)). + +For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called +`cargo saw-build` that builds a JSON file suitable for use with SAW. `cargo +saw-build` integrates directly with `cargo`, so you can pass flags to it like +any other `cargo` subcommand. For example: + +``` +$ export SAW_RUST_LIBRARY_PATH=<...> +$ cargo saw-build + +linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json + +``` + +Note that: + +* The full output of `cargo saw-build` here is omitted. The important part is + the `.linked-mir.json` file that appears after `linking X mir files into`, as + that is the JSON file that must be loaded with SAW. +* `SAW_RUST_LIBRARY_PATH` should point to the the MIR JSON files for the Rust + standard library. + +`mir-json` also supports compiling individual `.rs` files through `mir-json`'s +`saw-rustc` command. As the name suggests, it accepts all of the flags that +`rustc` accepts. For example: + +``` +$ export SAW_RUST_LIBRARY_PATH=<...> +$ saw-rustc example.rs + +linking 11 mir files into <...>/example.linked-mir.json + +``` ## Notes on C++ Analysis diff --git a/intTests/test_mir_load_module/Makefile b/intTests/test_mir_load_module/Makefile new file mode 100644 index 0000000000..eddd5ee141 --- /dev/null +++ b/intTests/test_mir_load_module/Makefile @@ -0,0 +1,8 @@ +all: test.json + +test.linked-mir.json: test.rs + saw-rustc $< + +.PHONY: clean +clean: + rm -f test.linked-mir.json diff --git a/intTests/test_mir_load_module/test.linked-mir.json b/intTests/test_mir_load_module/test.linked-mir.json new file mode 100644 index 0000000000..5f85cd77c2 --- /dev/null +++ b/intTests/test_mir_load_module/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"test.rs:1:23: 1:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"int","size":4,"val":"42"},"ty":"ty::i32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:27: 1:27"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}]},"name":"test/3a1fbbbh::foo[0]","return_ty":"ty::i32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/3a1fbbbh::foo[0]","kind":"Item","substs":[]},"name":"test/3a1fbbbh::foo[0]"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}}],"roots":["test/3a1fbbbh::foo[0]"]} \ No newline at end of file diff --git a/intTests/test_mir_load_module/test.rs b/intTests/test_mir_load_module/test.rs new file mode 100644 index 0000000000..8dbac789d2 --- /dev/null +++ b/intTests/test_mir_load_module/test.rs @@ -0,0 +1 @@ +pub fn foo() -> i32 { 42 } diff --git a/intTests/test_mir_load_module/test.saw b/intTests/test_mir_load_module/test.saw new file mode 100644 index 0000000000..0133aa05c4 --- /dev/null +++ b/intTests/test_mir_load_module/test.saw @@ -0,0 +1,4 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; +print m; diff --git a/intTests/test_mir_load_module/test.sh b/intTests/test_mir_load_module/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_load_module/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index ade1382ffb..34a12df8a8 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -419,6 +419,32 @@ No return fields +SAW/MIR/load module (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Load the specified MIR module. + +Parameter fields +++++++++++++++++ + + +``name`` + The name to refer to the loaded module by later. + + + +``module name`` + The file containing the MIR JSON file to load. + + + +Return fields ++++++++++++++ + +No return fields + + + SAW/Yosys/import (command) ~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 7cdf6084f3..bf987df9e6 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -45,6 +45,7 @@ common deps cryptol-saw-core, crucible, crucible-jvm, + crucible-mir, cryptonite, cryptonite-conduit, directory, @@ -81,6 +82,7 @@ library SAWServer.JVMVerify, SAWServer.LLVMCrucibleSetup, SAWServer.LLVMVerify, + SAWServer.MIRCrucibleSetup, SAWServer.NoParams, SAWServer.OK, SAWServer.ProofScript, diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 1017c747fd..68234bcfc4 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -36,6 +36,8 @@ import SAWServer.LLVMVerify llvmAssume, llvmVerifyX86Descr, llvmVerifyX86 ) +import SAWServer.MIRCrucibleSetup + ( mirLoadModuleDescr, mirLoadModule ) import SAWServer.ProofScript ( makeSimpsetDescr, makeSimpset, proveDescr, prove ) import SAWServer.SaveTerm ( saveTermDescr, saveTerm ) @@ -114,6 +116,11 @@ sawMethods = "SAW/LLVM/assume" llvmAssumeDescr llvmAssume + -- MIR + , Argo.command + "SAW/MIR/load module" + mirLoadModuleDescr + mirLoadModule -- Yosys , Argo.command "SAW/Yosys/import" diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 0f87671c20..d49ba23312 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -38,6 +38,7 @@ import qualified Data.AIG as AIG import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator) import qualified Lang.Crucible.JVM as CJ import qualified Lang.JVM.Codebase as JSS +import Mir.Generator (RustModule) --import qualified Verifier.SAW.CryptolEnv as CryptolEnv import Verifier.SAW.Module (emptyModule) import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule) @@ -78,7 +79,8 @@ import SAWServer.Exceptions notAJVMClass, notAJVMMethodSpecIR, notAYosysImport, - notAYosysTheorem, notAYosysSequential + notAYosysTheorem, notAYosysSequential, + notAMIRModule ) type SAWCont = (SAWEnv, SAWTask) @@ -317,12 +319,13 @@ data ServerVal | VJVMCrucibleSetup (Pair CrucibleSetupTypeRepr JVMSetupM) | VLLVMCrucibleSetup (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM) | VLLVMModule (Some CMS.LLVMModule) + | VMIRModule RustModule | VJVMMethodSpecIR (CMS.ProvedSpec CJ.JVM) | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.ProvedSpec) | VGhostVar CMS.GhostGlobal | VYosysImport YosysImport | VYosysTheorem YosysTheorem - | VYosysSequential YosysSequential + | VYosysSequential YosysSequential instance Show ServerVal where show (VTerm t) = "(VTerm " ++ show t ++ ")" @@ -333,6 +336,7 @@ instance Show ServerVal where show (VJVMCrucibleSetup _) = "VJVMCrucibleSetup" show (VLLVMCrucibleSetup _) = "VLLVMCrucibleSetup" show (VLLVMModule (Some _)) = "VLLVMModule" + show (VMIRModule _) = "VMIRModule" show (VLLVMMethodSpecIR _) = "VLLVMMethodSpecIR" show (VJVMMethodSpecIR _) = "VJVMMethodSpecIR" show (VGhostVar x) = "(VGhostVar " ++ show x ++ ")" @@ -391,6 +395,9 @@ instance KnownCrucibleSetupType a => IsServerVal (LLVMCrucibleSetupM a) where instance IsServerVal (Some CMS.LLVMModule) where toServerVal = VLLVMModule +instance IsServerVal RustModule where + toServerVal = VMIRModule + setServerVal :: IsServerVal val => ServerName -> val -> Argo.Command SAWState () setServerVal name val = do Argo.debugLog $ "Saving " <> (T.pack (show name)) @@ -438,6 +445,13 @@ getLLVMModule n = VLLVMModule m -> return m _other -> Argo.raise (notAnLLVMModule n) +getMIRModule :: ServerName -> Argo.Command SAWState RustModule +getMIRModule n = + do v <- getServerVal n + case v of + VMIRModule m -> return m + _other -> Argo.raise (notAMIRModule n) + getLLVMSetup :: ServerName -> Argo.Command SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM) getLLVMSetup n = do v <- getServerVal n diff --git a/saw-remote-api/src/SAWServer/Exceptions.hs b/saw-remote-api/src/SAWServer/Exceptions.hs index a580e000f0..f1584c0139 100644 --- a/saw-remote-api/src/SAWServer/Exceptions.hs +++ b/saw-remote-api/src/SAWServer/Exceptions.hs @@ -14,6 +14,7 @@ module SAWServer.Exceptions ( , notAYosysTheorem , notAYosysImport , notAYosysSequential + , notAMIRModule -- * Wrong monad errors , notSettingUpCryptol , notSettingUpLLVMCrucible @@ -192,6 +193,17 @@ notAYosysSequential name = " is not a Yosys sequential module") (Just $ object ["name" .= name]) +notAMIRModule :: + (ToJSON name, Show name) => + name {- ^ the name that should have been mapped to a MIR module -}-> + JSONRPCException +notAMIRModule name = + makeJSONRPCException 10140 + ("The server value with name " <> + T.pack (show name) <> + " is not a MIR module") + (Just $ object ["name" .= name]) + cantLoadLLVMModule :: String -> JSONRPCException cantLoadLLVMModule err = makeJSONRPCException diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs new file mode 100644 index 0000000000..a96da3bb4e --- /dev/null +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +-- | Support for interfacing with MIR-related commands in SAW. +module SAWServer.MIRCrucibleSetup + ( mirLoadModule + , mirLoadModuleDescr + ) where + +import Control.Lens ( view ) +import Data.Aeson ( FromJSON(..), withObject, (.:) ) + +import SAWScript.Crucible.MIR.Builtins ( mir_load_module ) + +import qualified Argo +import qualified Argo.Doc as Doc +import SAWServer as Server + ( ServerName(..), + SAWState, + sawTask, + setServerVal ) +import SAWServer.Exceptions ( notAtTopLevel ) +import SAWServer.OK ( OK, ok ) +import SAWServer.TopLevel ( tl ) +import SAWServer.TrackFile ( trackFile ) + +data MIRLoadModuleParams + = MIRLoadModuleParams ServerName FilePath + +instance FromJSON MIRLoadModuleParams where + parseJSON = + withObject "params for \"SAW/MIR/load module\"" $ \o -> + MIRLoadModuleParams <$> o .: "name" <*> o .: "module name" + +instance Doc.DescribedMethod MIRLoadModuleParams OK where + parameterFieldDescription = + [ ("name", + Doc.Paragraph [Doc.Text "The name to refer to the loaded module by later."]) + , ("module name", + Doc.Paragraph [Doc.Text "The file containing the MIR JSON file to load."]) + ] + resultFieldDescription = [] + +mirLoadModuleDescr :: Doc.Block +mirLoadModuleDescr = + Doc.Paragraph [Doc.Text "Load the specified MIR module."] + +-- | The implementation of the @SAW/MIR/load module@ command. +mirLoadModule :: MIRLoadModuleParams -> Argo.Command SAWState OK +mirLoadModule (MIRLoadModuleParams serverName fileName) = + do tasks <- view sawTask <$> Argo.getState + case tasks of + (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks + [] -> + do mirMod <- tl $ mir_load_module fileName + setServerVal serverName mirMod + trackFile fileName + ok diff --git a/saw-script.cabal b/saw-script.cabal index cff9ea9dc1..ed3b3257fc 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -37,6 +37,7 @@ library , crucible >= 0.4 , crucible-jvm , crucible-llvm >= 0.2 + , crucible-mir , deepseq , either , elf-edit @@ -155,6 +156,8 @@ library SAWScript.Crucible.JVM.Override SAWScript.Crucible.JVM.ResolveSetupValue + SAWScript.Crucible.MIR.Builtins + SAWScript.Prover.Mode SAWScript.Prover.Rewrite SAWScript.Prover.SolverStats diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs new file mode 100644 index 0000000000..293e88f965 --- /dev/null +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE ImplicitParams #-} + +-- | Implementations of Crucible-related SAWScript primitives for MIR. +module SAWScript.Crucible.MIR.Builtins + ( mir_load_module + ) where + +import qualified Data.ByteString.Lazy as BSL + +import Mir.Generator +import Mir.ParseTranslate + +import SAWScript.Options +import SAWScript.Value + +-- | Load a MIR JSON file and return a handle to it. +mir_load_module :: String -> TopLevel RustModule +mir_load_module inputFile = do + b <- io $ BSL.readFile inputFile + + opts <- getOptions + let ?debug = simVerbose opts + -- For now, we use the same default settings for implicit parameters as in + -- crux-mir. We may want to add options later that allow configuring these. + let ?assertFalseOnError = True + let ?printCrucible = False + + halloc <- getHandleAlloc + col <- io $ parseMIR inputFile b + io $ translateMIR mempty col halloc diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index e63271db55..bc9b50f538 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -93,6 +93,7 @@ import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ import SAWScript.Crucible.LLVM.Builtins import SAWScript.Crucible.JVM.Builtins +import SAWScript.Crucible.MIR.Builtins import SAWScript.Crucible.LLVM.X86 import SAWScript.Crucible.LLVM.Boilerplate import SAWScript.Crucible.LLVM.Skeleton.Builtins @@ -3748,6 +3749,14 @@ primitives = Map.fromList [ "Construct a `JVMValue` from a `Term`." ] --------------------------------------------------------------------- + -- Crucible/MIR commands + + , prim "mir_load_module" "String -> TopLevel MIRModule" + (pureVal mir_load_module) + Experimental + [ "Load a MIR JSON file and return a handle to it." ] + + --------------------------------------------------------------------- , prim "yosys_import" "String -> TopLevel Term" (pureVal yosys_import) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index d7c018d980..f0670630c7 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -113,6 +113,8 @@ import qualified Lang.Crucible.JVM as CJ import Lang.Crucible.Utils.StateContT import Lang.Crucible.LLVM.ArraySizeProfile +import Mir.Generator + import What4.ProgramLoc (ProgramLoc(..)) import Verifier.SAW.Heapster.Permissions @@ -158,6 +160,7 @@ data Value | VCryptolModule CryptolModule | VJavaClass JSS.Class | VLLVMModule (Some CMSLLVM.LLVMModule) + | VMIRModule RustModule | VHeapsterEnv HeapsterEnv | VSatResult SatResult | VProofResult ProofResult @@ -338,6 +341,7 @@ showsPrecValue opts nenv p v = VLLVMType t -> showString (show (LLVM.ppType t)) VCryptolModule m -> showString (showCryptolModule m) VLLVMModule (Some m) -> showString (CMSLLVM.showLLVMModule m) + VMIRModule m -> shows (PP.pretty (m^.rmCS^.collection)) VHeapsterEnv env -> showString (showHeapsterEnv env) VJavaClass c -> shows (prettyClass c) VProofResult r -> showsProofResult opts r @@ -669,7 +673,7 @@ withLocalEnv :: LocalEnv -> TopLevel a -> TopLevel a withLocalEnv env (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roLocalEnv = env }) m) withLocalEnvProof :: LocalEnv -> ProofScript a -> ProofScript a -withLocalEnvProof env (ProofScript m) = +withLocalEnvProof env (ProofScript m) = ProofScript (underExceptT (underStateT (withLocalEnv env)) m) getLocalEnv :: TopLevel LocalEnv @@ -1197,6 +1201,13 @@ instance FromValue (Some CMSLLVM.LLVMModule) where fromValue (VLLVMModule m) = m fromValue _ = error "fromValue CMSLLVM.LLVMModule" +instance IsValue RustModule where + toValue m = VMIRModule m + +instance FromValue RustModule where + fromValue (VMIRModule m) = m + fromValue _ = error "fromValue RustModule" + instance IsValue HeapsterEnv where toValue m = VHeapsterEnv m