diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index f6d70dd766..bfd9aabd49 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -53,7 +53,6 @@ common deps cryptonite-conduit, directory, jvm-parser, - jvm-verifier, lens, llvm-pretty, llvm-pretty-bc-parser, diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index e937381740..d17e163a89 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -37,7 +37,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 Text.LLVM.AST as LLVM -import qualified Verifier.Java.Codebase as JSS +import qualified Lang.JVM.Codebase as JSS import qualified Verifier.SAW.CryptolEnv as CryptolEnv import Verifier.SAW.Module (emptyModule) import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule) @@ -55,7 +55,6 @@ import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibl import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm) import Verifier.SAW.Rewriter (Simpset) -import qualified Verifier.Java.SAWBackend as JavaSAW import qualified Cryptol.Utils.Ident as Cryptol import Argo @@ -160,7 +159,6 @@ initialState readFileFn = silence $ do sc <- mkSharedContext CryptolSAW.scLoadPreludeModule sc - JavaSAW.scLoadJavaModule sc CryptolSAW.scLoadCryptolModule sc let mn = mkModuleName ["SAWScript"] scLoadModule sc (emptyModule mn) diff --git a/saw-script.cabal b/saw-script.cabal index 3133237307..2d41e6eae7 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -52,7 +52,6 @@ library , haskeline , IfElse , jvm-parser - , jvm-verifier , lens , llvm-pretty >= 0.8 , llvm-pretty-bc-parser >= 0.1.3.1 @@ -115,13 +114,8 @@ library SAWScript.Import SAWScript.ImportAIG SAWScript.Interpreter - SAWScript.JavaBuiltins SAWScript.JavaExpr - SAWScript.JavaMethodSpec - SAWScript.JavaMethodSpec.Evaluator - SAWScript.JavaMethodSpecIR SAWScript.JavaTools - SAWScript.JavaUtils SAWScript.JavaPretty SAWScript.Lexer SAWScript.LLVMBuiltins diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs index 56181fbb9b..497070bb54 100644 --- a/src/SAWScript/AutoMatch.hs +++ b/src/SAWScript/AutoMatch.hs @@ -56,7 +56,6 @@ import SAWScript.AutoMatch.LLVM import SAWScript.AutoMatch.Cryptol import SAWScript.LLVMBuiltins ---import SAWScript.JavaBuiltins import Language.JVM.Common (dotsToSlashes, mkClassName) import Prettyprinter.Render.Text (putDoc, hPutDoc) diff --git a/src/SAWScript/AutoMatch/JVM.hs b/src/SAWScript/AutoMatch/JVM.hs index d7583cf4a3..bda6c7e210 100644 --- a/src/SAWScript/AutoMatch/JVM.hs +++ b/src/SAWScript/AutoMatch/JVM.hs @@ -5,8 +5,6 @@ module SAWScript.AutoMatch.JVM where import qualified Language.JVM.Parser as JVM -import qualified Verifier.Java.Simulator as JSS hiding (lookupClass) - --import SAWScript.Builtins --import SAWScript.Options import SAWScript.AutoMatch.Declaration @@ -19,22 +17,22 @@ import Data.Either -- | Parse a Java class into a list of declarations -- Yields an Interaction so that we can talk to the user about what went wrong -getDeclsJVM :: JSS.Class -> IO (Interaction (Maybe [Decl])) +getDeclsJVM :: JVM.Class -> IO (Interaction (Maybe [Decl])) getDeclsJVM cls = return $ do let (untranslateable, translations) = - partitionEithers . for (JSS.classMethods cls) $ \method -> - maybe (Left $ JSS.methodName method) Right $ do - returnType <- jssTypeToStdType =<< JSS.methodReturnType method - argTypes <- mapM jssTypeToStdType $ JSS.methodParameterTypes method - let argIndices = map (JSS.localIndexOfParameter method) [0 .. length argTypes - 1] - tableEntries <- forM argIndices $ JSS.lookupLocalVariableByIdx method 0 - let args = zipWith Arg (map JSS.localName tableEntries) argTypes - return $ Decl (JSS.methodName method) returnType args + partitionEithers . for (JVM.classMethods cls) $ \method -> + maybe (Left $ JVM.methodName method) Right $ do + returnType <- jssTypeToStdType =<< JVM.methodReturnType method + argTypes <- mapM jssTypeToStdType $ JVM.methodParameterTypes method + let argIndices = map (JVM.localIndexOfParameter method) [0 .. length argTypes - 1] + tableEntries <- forM argIndices $ JVM.lookupLocalVariableByIdx method 0 + let args = zipWith Arg (map JVM.localName tableEntries) argTypes + return $ Decl (JVM.methodName method) returnType args when (not . null $ untranslateable) $ do separator ThinSep - liftF . flip Warning () $ "No translation for the following signatures in " ++ JVM.unClassName (JSS.className cls) ++ ".class:" + liftF . flip Warning () $ "No translation for the following signatures in " ++ JVM.unClassName (JVM.className cls) ++ ".class:" bulleted $ map (("'" ++) . (++ "'")) untranslateable return $ Just translations diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index b6bf994ffa..95f1f1cc60 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -60,10 +60,6 @@ import Data.Void (absurd) import Prettyprinter import System.IO --- jvm-verifier --- TODO: transition to Lang.JVM.Codebase from crucible-jvm -import qualified Verifier.Java.Codebase as CB - -- cryptol import qualified Cryptol.Eval.Type as Cryptol (evalValType) import qualified Cryptol.TypeCheck.Type as Cryptol @@ -88,6 +84,7 @@ import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.SimError as Crucible -- crucible-jvm +import qualified Lang.JVM.Codebase as CB import qualified Lang.Crucible.JVM as CJ -- parameterized-utils diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index a670a341a7..fc7d872347 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -83,7 +83,7 @@ import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, run import qualified Language.JVM.Common as J import qualified Language.JVM.Parser as J import qualified SAWScript.Utils as J -import qualified "jvm-verifier" Verifier.Java.Codebase as JCB +import qualified Lang.JVM.Codebase as JCB -- crucible-jvm import Lang.Crucible.JVM (IsCodebase(..)) @@ -91,13 +91,6 @@ import qualified Lang.Crucible.JVM as CJ import Debug.Trace --- --- | Use the Codebase implementation from the old Java static simulator --- -instance IsCodebase JCB.Codebase where - lookupClass cb = J.lookupClass cb fixPos - findMethod cb = J.findMethod cb fixPos - ----------------------------------------------------------------------- -- | Make sure the class is in the database and allocate handles for its -- methods and static fields diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index fca3e0c6dd..815f8feccf 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -37,10 +37,7 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) -- crucible-jvm import qualified Lang.Crucible.JVM as CJ - --- jvm-verifier --- TODO: transition to Lang.JVM.Codebase from crucible-jvm -import qualified Verifier.Java.Codebase as CB +import qualified Lang.JVM.Codebase as CB -- jvm-parser import qualified Language.JVM.Parser as J diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index a5197a70f0..c333f6df87 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -50,7 +50,6 @@ import SAWScript.AST (Located(..),Import(..)) import SAWScript.Builtins import SAWScript.Exceptions (failTypecheck) import qualified SAWScript.Import -import SAWScript.JavaBuiltins import SAWScript.JavaExpr import SAWScript.LLVMBuiltins import SAWScript.Options @@ -71,8 +70,7 @@ import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import qualified Verifier.SAW.CryptolEnv as CEnv -import qualified Verifier.Java.Codebase as JCB -import qualified Verifier.Java.SAWBackend as JavaSAW +import qualified Lang.JVM.Codebase as JCB import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW @@ -400,7 +398,6 @@ buildTopLevelEnv proxy opts = sc0 <- mkSharedContext let ?fileReader = BS.readFile CryptolSAW.scLoadPreludeModule sc0 - JavaSAW.scLoadJavaModule sc0 CryptolSAW.scLoadCryptolModule sc0 scLoadModule sc0 (emptyModule mn) cryptol_mod <- scFindModule sc0 $ mkModuleName ["Cryptol"] @@ -1647,157 +1644,11 @@ primitives = Map.fromList Current [ "The Java type corresponding to the named class." ] - --, prim "java_value" "{a} String -> a" - - , prim "java_var" "String -> JavaType -> JavaSetup Term" - (pureVal javaVar) - Deprecated - [ "Return a term corresponding to the initial value of the named Java" - , "variable, which should have the given type. The returned term can be" - , "used to construct more complex expressions. For example it can be used" - , "with 'java_return' to describe the expected return value in terms" - , "of the initial value of a variable. The Java variable can also be of" - , "the form \"args[n]\" to refer to the (0-based) nth argument of a method." - ] - - , prim "java_class_var" "String -> JavaType -> JavaSetup ()" - (pureVal javaClassVar) - Deprecated - [ "Declare that the named Java variable should point to an object of the" - , "given class type." - ] - - , prim "java_may_alias" "[String] -> JavaSetup ()" - (pureVal javaMayAlias) - Deprecated - [ "Indicate that the given set of Java variables are allowed to alias" - , "each other." - ] - - , prim "java_assert" "Term -> JavaSetup ()" - (pureVal javaAssert) - Deprecated - [ "Assert that the given term should evaluate to true in the initial" - , "state of a Java method." - ] - - , prim "java_assert_eq" "String -> Term -> JavaSetup ()" - (pureVal javaAssertEq) - Deprecated - [ "Assert that the given variable should have the given value in the" - , "initial state of a Java method." - ] - - , prim "java_ensure_eq" "String -> Term -> JavaSetup ()" - (pureVal javaEnsureEq) - Deprecated - [ "Specify that the given Java variable should have a value equal to the" - , "given term when execution finishes." - ] - - , prim "java_modify" "String -> JavaSetup ()" - (pureVal javaModify) - Deprecated - [ "Indicate that a Java method may modify the named portion of the state." ] - - , prim "java_return" "Term -> JavaSetup ()" - (pureVal javaReturn) - Deprecated - [ "Indicate the expected return value of a Java method." ] - - , prim "java_verify_tactic" "ProofScript SatResult -> JavaSetup ()" - (pureVal javaVerifyTactic) - Deprecated - [ "Use the given proof script to prove the specified properties about" - , "a Java method." - ] - - , prim "java_sat_branches" "Bool -> JavaSetup ()" - (pureVal javaSatBranches) - Deprecated - [ "Turn on or off satisfiability checking of branch conditions during" - , "symbolic execution." - ] - - , prim "java_no_simulate" "JavaSetup ()" - (pureVal javaNoSimulate) - Deprecated - [ "Skip symbolic simulation for this Java method." ] - - , prim "java_allow_alloc" "JavaSetup ()" - (pureVal javaAllowAlloc) - Deprecated - [ "Allow allocation of new objects or arrays during simulation," - , "as long as the behavior of the method can still be described" - , "as a pure function." - ] - - , prim "java_requires_class" "String -> JavaSetup ()" - (pureVal javaRequiresClass) - Deprecated - [ "Declare that the given method can only be executed if the given" - , "class has already been initialized." - ] - - , prim "java_pure" "JavaSetup ()" - (pureVal javaPure) - Deprecated - [ "The empty specification for 'java_verify'. Equivalent to 'return ()'." ] - , prim "java_load_class" "String -> TopLevel JavaClass" (pureVal CJ.loadJavaClass) Current [ "Load the named Java class and return a handle to it." ] - --, prim "java_class_info" "JavaClass -> TopLevel ()" - - , prim "java_extract" - "JavaClass -> String -> JavaSetup () -> TopLevel Term" - (pureVal extractJava) - Deprecated - [ "Translate a Java method directly to a Term. The parameters of the" - , "Term will be the parameters of the Java method, and the return" - , "value will be the return value of the method. Only static methods" - , "with scalar argument and return types are currently supported. For" - , "more flexibility, see 'java_symexec' or 'java_verify'." - ] - - , prim "java_symexec" - "JavaClass -> String -> [(String, Term)] -> [String] -> Bool -> TopLevel Term" - (pureVal symexecJava) - Deprecated - [ "Symbolically execute a Java method and construct a Term corresponding" - , "to its result. The first list contains pairs of variable or field" - , "names along with Terms specifying their initial (possibly symbolic)" - , "values. The second list contains the names of the variables or fields" - , "to treat as outputs. The resulting Term will be of tuple type, with" - , "as many elements as there are names in the output list." - , "The final boolean value indicates if path conditions should be checked for" - , "satisfiability at branch points." - ] - - , prim "java_verify" - "JavaClass -> String -> [JavaMethodSpec] -> JavaSetup () -> TopLevel JavaMethodSpec" - (pureVal verifyJava) - Deprecated - [ "Verify a Java method against a method specification. The first two" - , "arguments are the same as for 'java_extract' and 'java_symexec'." - , "The list of JavaMethodSpec values in the third argument makes it" - , "possible to use the results of previous verifications to take the" - , "place of actual execution when encountering a method call. The last" - , "parameter is a setup block, containing a sequence of commands of type" - , "'JavaSetup a' that configure the symbolic simulator and specify the" - , "types of variables in scope, the expected results of execution, and" - , "the tactics to use to verify that the method produces the expected" - , "results." - ] - -{- , prim "crucible_java_cfg" - "JavaClass -> String -> TopLevel CFG" - (bicVal crucible_java_cfg) - [ "Convert a Java method to a Crucible CFG." - ] -} - , prim "jvm_extract" "JavaClass -> String -> TopLevel Term" (pureVal CJ.jvm_extract) Current diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs deleted file mode 100644 index 4ff7cd93a9..0000000000 --- a/src/SAWScript/JavaBuiltins.hs +++ /dev/null @@ -1,544 +0,0 @@ -{- | -Module : SAWScript.JavaBuiltins -Description : Implementations of Java-related SAW-Script primitives. -License : BSD3 -Maintainer : atomb -Stability : provisional --} -{-# LANGUAGE CPP #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE FlexibleContexts #-} - -module SAWScript.JavaBuiltins where - -#if !MIN_VERSION_base(4,8,0) -import Control.Applicative hiding (empty) -#endif -import Control.Lens -import Control.Monad.State -import Control.Monad.Trans.Except -import Data.List (partition) -import Data.Maybe (mapMaybe) -import Data.IORef -import qualified Data.Map as Map -import Data.Time.Clock -import qualified Data.Text as Text -import Prettyprinter - -import Language.JVM.Common - -import Verifier.Java.Codebase hiding (lookupClass) -import Verifier.Java.Simulator as JSS hiding (lookupClass) -import Verifier.Java.SAWBackend - -import Verifier.SAW.Cryptol (importType, emptyEnv, exportFirstOrderValue) -import Verifier.SAW.Recognizer -import Verifier.SAW.FiniteValue (FirstOrderValue) -import Verifier.SAW.SCTypeCheck hiding (TypedTerm) -import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedTerm -import Verifier.SAW.TypedAST (toShortName) -import Verifier.SAW.CryptolEnv (schemaNoUser) - -import qualified SAWScript.CongruenceClosure as CC - -import SAWScript.JavaExpr -import SAWScript.JavaMethodSpec -import SAWScript.JavaMethodSpecIR -import SAWScript.JavaUtils - -import SAWScript.Builtins -import SAWScript.Options -import SAWScript.Position (Pos(..), renderDoc) -import SAWScript.Proof -import SAWScript.Utils -import SAWScript.Value as SS - -import qualified Cryptol.Backend.Monad as Cryptol (runEval) -import qualified Cryptol.Eval.Value as Cryptol (ppValue) -import qualified Cryptol.Eval.Concrete as Cryptol (Concrete(..)) -import qualified Cryptol.TypeCheck.AST as Cryptol -import qualified Cryptol.Utils.PP as Cryptol (pretty) - -loadJavaClass :: JSS.Codebase -> String -> IO Class -loadJavaClass cb = - lookupClass cb fixPos . mkClassName . dotsToSlashes - -getActualArgTypes :: JavaSetupState -> Either String [JavaActualType] -getActualArgTypes s = mapM getActualType declaredTypes - where - declaredTypes = zip [0..] (methodParameterTypes meth) - ir = jsSpec s - meth = specMethod ir - getActualType (n, ty) = do - let i = localIndexOfParameter meth n - atys = [ aty | (CC.Term (Local _ i' _), aty) <- - Map.toList (specActualTypeMap ir), i == i' ] - case atys of - [] | isPrimitiveType ty -> Right (PrimitiveType ty) - | otherwise -> - Left $ "No declared type for non-scalar parameter " ++ show n - [aty] -> Right aty - _ -> Left $ "More than one actual type given for parameter " ++ show n - -type Assign = (JavaExpr, TypedTerm) - -symexecJava :: Class - -> String - -> [(String, TypedTerm)] - -> [String] - -> Bool - -> TopLevel TypedTerm -symexecJava cls mname inputs outputs satBranches = do - cb <- getJavaCodebase - jsc <- getSharedContext - opts <- getOptions - let pos = fixPos - fl = defaultSimFlags { alwaysBitBlastBranchTerms = True - , satAtBranches = satBranches - } - (_mcls, meth) <- io $ findMethod cb pos mname cls - -- TODO: should we use mcls anywhere below? - let mkAssign (s, tm) = do - e <- parseJavaExpr' cb cls meth s - return (e, tm) - multDefErr i = error $ "Multiple terms given for " ++ ordinal (i + 1) ++ - " argument in method " ++ methodName meth - noDefErr i = fail $ "No binding for " ++ ordinal (i + 1) ++ - " argument in method " ++ methodName meth - pidx = fromIntegral . localIndexOfParameter meth - withSAWBackend Nothing $ \sbe -> io $ do - runSimulator cb sbe defaultSEH (Just fl) $ do - setVerbosity (simVerbose opts) - assigns <- mapM mkAssign inputs - let (argAssigns, otherAssigns) = partition (isArg meth . fst) assigns - argMap = Map.fromListWithKey (\i _ _ -> multDefErr i) - [ (idx, tm) | (CC.Term (Local _ idx _), tm) <- argAssigns ] - argTms <- forM [0..maxArg meth] $ \i -> - maybe (noDefErr i) return $ Map.lookup (pidx i) argMap - actualArgTys <- liftIO $ mapM (scTypeOf jsc . ttTerm) argTms - let expectedArgTys = methodParameterTypes meth - forM_ (zip actualArgTys expectedArgTys) $ \ (aty, ety) -> do - comp <- liftIO $ termTypeCompatible jsc aty ety - unless comp $ fail $ - "Passing value of type " ++ show aty ++ - " to argument expected to be of type " ++ show ety ++ "." - args <- mapM (uncurry (valueOfTerm jsc)) (zip expectedArgTys argTms) - mapM_ (uncurry (writeJavaTerm jsc)) otherAssigns - allArgs <- case methodIsStatic meth of - True -> return args - False -> do - this <- createInstance (className cls) Nothing - return (RValue this : args) - let localMap = setupLocals allArgs - mp <- execMethod (className cls) (methodKey meth) localMap - ps <- case mp of - Nothing -> fail "No paths returned from execMethod" - Just (ps, _) -> return ps - outtms <- forM outputs $ \ostr -> do - case ostr of - "$safety" -> return (ps ^. pathAssertions) - _-> do - e <- parseJavaExpr' cb cls meth ostr - readJavaTerm jsc (Just localMap) ps e - let bundle tms = case tms of - [t] -> return t - _ -> scTuple jsc tms - liftIO (mkTypedTerm jsc =<< bundle outtms) - -extractJava :: Class -> String - -> JavaSetup () - -> TopLevel TypedTerm -extractJava cls mname setup = do - cb <- getJavaCodebase - sc <- getSharedContext - opts <- getOptions - let pos = fixPos - argsRef <- io $ newIORef [] - withSAWBackend (Just argsRef) $ \sbe -> do - setupRes <- runJavaSetup pos cb cls mname setup - let fl = defaultSimFlags { alwaysBitBlastBranchTerms = - jsSatBranches setupRes } - meth = specMethod (jsSpec setupRes) - io $ runSimulator cb sbe defaultSEH (Just fl) $ do - setVerbosity (simVerbose opts) - argTypes <- either fail return (getActualArgTypes setupRes) - args <- mapM (freshJavaVal (Just argsRef) sc) argTypes - -- TODO: support initializing other state elements - rslt <- case methodIsStatic meth of - True -> execStaticMethod (className cls) (methodKey meth) args - False -> do - ~(RValue this) <- freshJavaVal (Just argsRef) sc (ClassInstance cls) - execInstanceMethod (className cls) (methodKey meth) this args - dt <- case (rslt, methodReturnType meth) of - (Nothing, _) -> fail $ "No return value from " ++ methodName meth - (_, Nothing) -> fail $ "Return value from void method " ++ methodName meth - (Just v, Just tp) -> termOfValueSim sc tp v - liftIO $ do - argBinds <- reverse <$> readIORef argsRef - let exts = mapMaybe asExtCns argBinds - -- TODO: group argBinds according to the declared types - scAbstractExts sc exts dt >>= mkTypedTerm sc - -withSAWBackend :: Maybe (IORef [Term]) - -> (Backend SharedContext -> TopLevel a) - -> TopLevel a -withSAWBackend argsRef a = do - sc <- getSharedContext - AIGProxy proxy <- getProxy - io (sawBackend sc argsRef proxy) >>= a - -runJavaSetup :: Pos -> Codebase -> Class -> String - -> StateT JavaSetupState TopLevel a - -> TopLevel JavaSetupState -runJavaSetup pos cb cls mname setup = do - sc <- getSharedContext - ms <- io $ initMethodSpec pos cb cls mname - let setupState = JavaSetupState { - jsSpec = ms - , jsContext = sc - , jsTactic = Skip - , jsSimulate = True - , jsSatBranches = False - } - execStateT setup setupState - -verifyJava :: Class -> String - -> [JavaMethodSpecIR] - -> JavaSetup () - -> TopLevel JavaMethodSpecIR -verifyJava cls mname overrides setup = do - startTime <- io $ getCurrentTime - cb <- getJavaCodebase - sc <- getSharedContext - opts <- getOptions - let pos = fixPos -- TODO - setupRes <- runJavaSetup pos cb cls mname setup - let ms = jsSpec setupRes - vp = VerifyParams { - vpCode = cb - , vpContext = sc - , vpOpts = opts - , vpSpec = ms - , vpOver = overrides - } - when (jsSimulate setupRes) $ do - let overrideText = - case overrides of - [] -> "" - irs -> " (overriding " ++ show (map renderName irs) ++ ")" - renderName ir = unClassName (className (specMethodClass ir)) ++ "." ++ - methodName (specMethod ir) - configs = [ (bs, cl) - | bs <- {- concat $ Map.elems $ -} [specBehaviors ms] - , cl <- bsRefEquivClasses bs - ] - fl = defaultSimFlags { alwaysBitBlastBranchTerms = True - , satAtBranches = jsSatBranches setupRes - } - printOutLnTop Debug $ "Starting verification of " ++ specName ms - ro <- getTopLevelRO - rw <- getTopLevelRW - forM_ configs $ \(bs,cl) -> withSAWBackend Nothing $ \sbe -> io $ do - liftIO $ bsCheckAliasTypes pos bs - liftIO $ printOutLn opts Debug $ "Executing " ++ specName ms ++ - " at PC " ++ show (bsLoc bs) ++ "." - -- runDefSimulator cb sbe $ do - runSimulator cb sbe defaultSEH (Just fl) $ do - setVerbosity (simVerbose opts) - let prover script vs n g = do - let exts = getAllExts g - gprop <- io $ scGeneralizeExts sc exts =<< scEqTrue sc g - io $ doExtraChecks opts sc gprop - let goal = ProofGoal n "vc" (vsVCName vs) (Prop gprop) - r <- evalStateT script (startProof goal) - case r of - SS.Unsat _ -> liftIO $ printOutLn opts Debug "Valid." - SS.SatMulti _ vals -> - io $ showCexResults opts sc (rwPPOpts rw) ms vs exts vals - let ovds = vpOver vp - initPS <- initializeVerification' sc ms bs cl - liftIO $ printOutLn opts Debug $ "Overriding: " ++ show (map specName ovds) - mapM_ (overrideFromSpec sc (specPos ms)) ovds - liftIO $ printOutLn opts Debug $ "Running method: " ++ specName ms - -- Execute code. - run - liftIO $ printOutLn opts Debug $ "Checking final state" - pvc <- checkFinalState sc ms bs cl initPS - let pvcs = [pvc] -- Only one for now, but that might change - liftIO $ printOutLn opts ExtraDebug "Verifying the following:" - liftIO $ mapM_ (printOutLn opts ExtraDebug . show . ppPathVC) pvcs - let validator script = runValidation (prover script) vp sc pvcs - case jsTactic setupRes of - Skip -> liftIO $ printOutLn opts Warn $ - "WARNING: skipping verification of " ++ specName ms - RunVerify script -> - liftIO $ fmap fst $ runTopLevel (validator script) ro rw - endTime <- io $ getCurrentTime - printOutLnTop Info $ "Successfully verified " ++ specName ms ++ overrideText ++ - " (" ++ showDuration (diffUTCTime endTime startTime) ++ ")" - unless (jsSimulate setupRes) $ printOutLnTop Warn $ - "WARNING: skipping simulation of " ++ specName ms - return ms - -doExtraChecks :: Options -> SharedContext -> Term -> IO () -doExtraChecks opts bsc t = do - when (extraChecks opts) $ do - printOutLn opts Debug "Type checking goal..." - tcr <- scTypeCheck bsc Nothing t - case tcr of - Left e -> printOutLn opts Warn $ unlines $ - "Ill-typed goal constructed." : prettyTCError e - Right _ -> printOutLn opts Debug "Done." - printOutLn opts ExtraDebug $ "Trying to prove: " ++ show t - -showCexResults :: Options - -> SharedContext - -> SS.PPOpts - -> JavaMethodSpecIR - -> VerifyState - -> [ExtCns Term] - -> [(String, FirstOrderValue)] - -> IO () -showCexResults vpopts sc opts ms vs exts vals = do - printOutLn vpopts Info $ "When verifying " ++ specName ms ++ ":" - printOutLn vpopts Info $ "Proof of " ++ vsVCName vs ++ " failed." - printOutLn vpopts Info $ "Counterexample:" - let showVal v = show <$> (Cryptol.runEval mempty - (Cryptol.ppValue Cryptol.Concrete (cryptolPPOpts opts) (exportFirstOrderValue v))) - mapM_ (\(n, v) -> do vdoc <- showVal v - printOutLn vpopts Info (" " ++ n ++ ": " ++ vdoc)) vals - if (length exts == length vals) - then do let cexEval = cexEvalFn sc (zip exts (map snd vals)) - doc <- vsCounterexampleFn vs cexEval - printOutLn vpopts Info (renderDoc doc) - else do printOutLn vpopts Info $ "ERROR: Can't show result, wrong number of values" - printOutLn vpopts Info $ "Constants: " ++ show (map ecName exts) - printOutLn vpopts Info $ "Value names: " ++ show (map fst vals) - fail "Proof failed." - -mkMixedExpr :: Term -> JavaSetup MixedExpr -mkMixedExpr (asJavaExpr -> Just s) = - (JE . fst) <$> getJavaExpr "mkMixedExpr" s -mkMixedExpr t = do - sc <- lift getSharedContext - let exts = getAllExts t - extNames = map ecName exts - jes <- mapM (getJavaExpr "mkMixedExpr" . Text.unpack . toShortName) extNames -- TODO????? - fn <- liftIO $ scAbstractExts sc exts t - return $ LE $ LogicExpr fn (map fst jes) - -exportJSSType :: JavaType -> JavaSetup Type -exportJSSType jty = - case jty of - JavaBoolean -> return BooleanType - JavaByte -> return ByteType - JavaChar -> return CharType - JavaShort -> return ShortType - JavaInt -> return IntType - JavaLong -> return LongType - JavaFloat -> return FloatType - JavaDouble -> return DoubleType - JavaArray _ ety -> ArrayType <$> exportJSSType ety - JavaClass name -> return $ ClassType (mkClassName (dotsToSlashes name)) - -exportJavaType :: Codebase -> JavaType -> JavaSetup JavaActualType -exportJavaType cb jty = - case jty of - JavaBoolean -> return $ PrimitiveType BooleanType - JavaByte -> return $ PrimitiveType ByteType - JavaChar -> return $ PrimitiveType CharType - JavaShort -> return $ PrimitiveType ShortType - JavaInt -> return $ PrimitiveType IntType - JavaLong -> return $ PrimitiveType LongType - JavaFloat -> return $ PrimitiveType FloatType - JavaDouble -> return $ PrimitiveType DoubleType - JavaArray n t -> ArrayInstance (fromIntegral n) <$> exportJSSType t - JavaClass name -> - do cls <- liftIO $ lookupClass cb fixPos (mkClassName (dotsToSlashes name)) - return (ClassInstance cls) - -checkCompatibleType - :: SharedContext - -> String - -> JavaActualType - -> Cryptol.Schema - -> JavaSetup () -checkCompatibleType _sc msg aty schema = - case cryptolTypeOfActual aty of - Nothing -> - throwJava $ "Type is not translatable: " ++ show aty ++ " (" ++ msg ++ ")" - Just lt -> do - unless (Cryptol.Forall [] [] lt == schemaNoUser schema) $ throwJava $ - unlines [ "Incompatible type:" - , " Expected: " ++ Cryptol.pretty lt - , " Got: " ++ Cryptol.pretty schema - , " In context: " ++ msg - ] - -parseJavaExpr' :: (MonadIO m) => - JSS.Codebase -> JSS.Class -> JSS.Method -> String - -> m JavaExpr -parseJavaExpr' cb cls meth name = - liftIO (runExceptT (parseJavaExpr cb cls meth name) >>= either fail return) - -getJavaExpr :: String -> String -> JavaSetup (JavaExpr, JavaActualType) -getJavaExpr ctx name = do - ms <- gets jsSpec - let cb = specCodebase ms - cls = specThisClass ms - meth = specMethod ms - e <- parseJavaExpr' cb cls meth name - case Map.lookup e (bsActualTypeMap (specBehaviors ms)) of - Just ty -> return (e, ty) - Nothing -> throwJava $ renderDoc $ - vcat - [ hsep [ "Unknown expression", ftext name, "in", ftext ctx ] <> "." - , ftext "Maybe you're missing a `java_var` or `java_class_var`?" - ] - -typeJavaExpr :: JSS.Codebase -> String -> JavaType - -> JavaSetup (JavaExpr, JavaActualType) -typeJavaExpr cb name ty = do - ms <- gets jsSpec - expr <- parseJavaExpr' cb (specThisClass ms) (specMethod ms) name - jty' <- exportJSSType ty - checkEqualTypes (exprType expr) jty' name - aty <- exportJavaType cb ty - return (expr, aty) - -checkEqualTypes :: Type -> Type -> String -> JavaSetup () -checkEqualTypes declared actual name = - when (declared /= actual) $ throwJava $ show $ - hsep [ "WARNING: Declared type" - , viaShow (ppType declared) -- TODO: change pretty-printer - , "doesn't match actual type" - , viaShow (ppType actual) -- TODO: change pretty-printer - , "for variable" - , pretty name - ] - -modifySpec :: (JavaMethodSpecIR -> JavaMethodSpecIR) -> JavaSetup () -modifySpec f = modify $ \st -> st { jsSpec = f (jsSpec st) } - -javaPure :: JavaSetup () -javaPure = return () - -javaNoSimulate :: JavaSetup () -javaNoSimulate = modify (\s -> s { jsSimulate = False }) - -javaSatBranches :: Bool -> JavaSetup () -javaSatBranches doSat = modify (\s -> s { jsSatBranches = doSat }) - -javaRequiresClass :: String -> JavaSetup () -javaRequiresClass cls = modifySpec $ \ms -> - let clss' = mkClassName (dotsToSlashes cls) : specInitializedClasses ms in - ms { specInitializedClasses = clss' } - -javaClassVar :: String -> JavaType - -> JavaSetup () -javaClassVar name t = do - cb <- lift getJavaCodebase - (expr, aty) <- typeJavaExpr cb name t - case aty of - ClassInstance _ -> return () - _ -> throwJava "Can't use `java_class_var` with variable of non-class type." - modifySpec (specAddVarDecl expr aty) - -javaVar :: String -> JavaType - -> JavaSetup TypedTerm -javaVar name t = do - cb <- lift getJavaCodebase - (expr, aty) <- typeJavaExpr cb name t - case aty of - ClassInstance _ -> throwJava "Can't use `java_var` with variable of class type." - _ -> return () - modifySpec (specAddVarDecl expr aty) - sc <- lift getSharedContext - case cryptolTypeOfActual aty of - Nothing -> throwJava $ "Unsupported type for `java_var`: " ++ show aty - Just cty -> - liftIO $ - do lty <- importType sc emptyEnv cty - v <- scJavaValue sc lty name - return $ TypedTerm (Cryptol.tMono cty) v - -javaMayAlias :: [String] -> JavaSetup () -javaMayAlias exprs = do - exprList <- mapM (getJavaExpr "java_may_alias") exprs - forM_ exprList $ \(e, _) -> - unless (isRefJavaExpr e) $ throwJava $ - "Can't use `java_may_alias` with non-reference variable: " ++ - ppJavaExpr e - modifySpec (specAddAliasSet (map fst exprList)) - -javaAssert :: TypedTerm -> JavaSetup () -javaAssert (TypedTerm schema v) = do - unless (schemaNoUser schema == Cryptol.Forall [] [] Cryptol.tBit) $ - throwJava $ "java_assert passed expression of non-boolean type: " ++ show schema - me <- mkMixedExpr v - case me of - LE le -> modifySpec (specAddAssumption le) - JE je -> throwJava $ "Used java_assert with Java expression: " ++ show je - -javaAssertEq :: String -> TypedTerm -> JavaSetup () -javaAssertEq name (TypedTerm schema t) = do - (expr, aty) <- (getJavaExpr "java_assert_eq") name - sc <- lift getSharedContext - checkCompatibleType sc "java_assert_eq" aty schema - me <- mkMixedExpr t - modifySpec (specAddLogicAssignment fixPos expr me) - -javaEnsureEq :: String -> TypedTerm -> JavaSetup () -javaEnsureEq name (TypedTerm schema t) = do - ms <- gets jsSpec - sc <- lift getSharedContext - (expr, aty) <- (getJavaExpr "java_ensure_eq") name - when (isArg (specMethod ms) expr && isScalarExpr expr) $ throwJava $ - "The `java_ensure_eq` function cannot be used " ++ - "to set the value of a scalar argument." - checkCompatibleType sc "java_ensure_eq" aty schema - me <- mkMixedExpr t - cmd <- case (CC.unTerm expr, aty) of - (_, ArrayInstance _ _) -> return (EnsureArray fixPos expr me) - (InstanceField r f, _) -> return (EnsureInstanceField fixPos r f me) - (StaticField f, _) -> return (EnsureStaticField fixPos f me) - _ -> throwJava $ "invalid java_ensure target: " ++ name - modifySpec (specAddBehaviorCommand cmd) - -javaModify :: String -> JavaSetup () -javaModify name = do - ms <- gets jsSpec - (expr, aty) <- (getJavaExpr "java_modify") name - when (isArg (specMethod ms) expr && isScalarExpr expr) $ throwJava $ - "The `java_modify` function cannot be used " ++ - "to set the value of a scalar argument." - cmd <- case (CC.unTerm expr, aty) of - (_, ArrayInstance _ _) -> return (ModifyArray expr aty) - (InstanceField r f, _) -> return (ModifyInstanceField r f) - (StaticField f, _) -> return (ModifyStaticField f) - _ -> throwJava $ "invalid java_modify target: " ++ name - modifySpec (specAddBehaviorCommand cmd) - -javaReturn :: TypedTerm -> JavaSetup () -javaReturn (TypedTerm _ t) = do - ms <- gets jsSpec - let meth = specMethod ms - case methodReturnType meth of - Just _ty -> do - -- TODO: check that types are compatible - me <- mkMixedExpr t - modifySpec (specAddBehaviorCommand (ReturnValue me)) - Nothing -> - throwJava $ "can't use `java_return` on void method " ++ methodName meth - -javaVerifyTactic :: ProofScript SatResult -> JavaSetup () -javaVerifyTactic script = - modify $ \st -> st { jsTactic = RunVerify script } - -javaAllowAlloc :: JavaSetup () -javaAllowAlloc = modifySpec specSetAllowAllocation diff --git a/src/SAWScript/JavaExpr.hs b/src/SAWScript/JavaExpr.hs index 5389b9f6a7..836b3b5a89 100644 --- a/src/SAWScript/JavaExpr.hs +++ b/src/SAWScript/JavaExpr.hs @@ -72,8 +72,7 @@ import qualified Data.Text as Text import qualified Data.Vector as V import Text.Read hiding (lift) -import Verifier.Java.Codebase as JSS -import Verifier.Java.SAWBackend hiding (basic_ss) +import Lang.JVM.Codebase as JSS import Verifier.SAW.Cryptol import Verifier.SAW.Recognizer diff --git a/src/SAWScript/JavaMethodSpec.hs b/src/SAWScript/JavaMethodSpec.hs deleted file mode 100644 index 706d5e5e35..0000000000 --- a/src/SAWScript/JavaMethodSpec.hs +++ /dev/null @@ -1,809 +0,0 @@ -{- | -Module : SAWScript.JavaMethodSpec -Description : Interface to the Java symbolic simulator. -License : BSD3 -Maintainer : atomb -Stability : provisional --} -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DoAndIfThenElse #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE MonoLocalBinds #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE TupleSections #-} - -module SAWScript.JavaMethodSpec - ( JavaMethodSpecIR - , specMethod - , specName - , specMethodClass - , SymbolicRunHandler - , initializeVerification' - , runValidation - , checkFinalState - , overrideFromSpec - , PathVC(..) - , pvcgAssertEq - , pvcgAssert - , pvcgFail - , ppPathVC - , VerifyParams(..) - , VerifyState(..) - , EvalContext(..) - ) where - --- Imports {{{1 - -#if !MIN_VERSION_base(4,8,0) -import Control.Applicative hiding (empty) -#endif -import Control.Lens -import Control.Monad -import Control.Monad.Cont -import qualified Control.Monad.Fail as Fail -import Control.Monad.State -import Data.Function -import Data.List (intercalate, sortBy) -import qualified Data.Map.Strict as Map -import Data.Maybe -import qualified Data.Set as Set -import Prettyprinter -import qualified Text.PrettyPrint.HughesPJ as PP - -import Language.JVM.Common (ppFldId) -import qualified SAWScript.CongruenceClosure as CC -import SAWScript.JavaExpr as TC -import SAWScript.Options hiding (Verbosity) -import qualified SAWScript.Options as Opts -import SAWScript.Utils -import SAWScript.JavaMethodSpecIR -import SAWScript.JavaMethodSpec.Evaluator -import SAWScript.JavaUtils -import SAWScript.PathVC -import SAWScript.Position (Pos(..)) -import SAWScript.Value (TopLevel, TopLevelRW(rwPPOpts), getTopLevelRW, io, printOutTop, printOutLnTop) -import SAWScript.VerificationCheck - -import Data.JVM.Symbolic.AST (entryBlock) - -import Verifier.Java.Simulator hiding (asBool, State, InvalidType) -import Verifier.Java.SAWBackend hiding (basic_ss) - -import Verifier.SAW.Prelude -import Verifier.SAW.Recognizer -import Verifier.SAW.SharedTerm -import Verifier.SAW.Term.Pretty (SawDoc) -import Verifier.SAW.TypedTerm - --- JSS Utilities {{{1 - -type Verbosity = Int - --- EvalContext {{{1 - -evalErrExpr :: ExprEvalError -> TC.JavaExpr -evalErrExpr (EvalExprUndefined e) = e -evalErrExpr (EvalExprUnknownArray e) = e -evalErrExpr (EvalExprUnknownLocal _ e) = e -evalErrExpr (EvalExprUnknownField _ e) = e -evalErrExpr (EvalExprBadJavaType _ e) = e -evalErrExpr (EvalExprBadLogicType _ _) = - error "evalErrExpr: EvalExprBadLogicType" -evalErrExpr (EvalExprNoReturn e) = e - --- Method specification overrides {{{1 --- OverrideComputation definition {{{2 - --- | State for running the behavior specifications in a method override. -data OCState = OCState { - ocsLoc :: Breakpoint - , ocsEvalContext :: !EvalContext - , ocsResultState :: !SpecPathState - , ocsErrors :: [OverrideError] - } - -data OverrideError - = UndefinedExpr TC.JavaExpr - | FalseAssertion Pos - | AliasingInputs !TC.JavaExpr !TC.JavaExpr - | JavaExceptionThrown Ref - | SimException String - | InvalidType String - | Abort - deriving (Show) - -ppOverrideError :: OverrideError -> String -ppOverrideError (UndefinedExpr expr) = - "Could not evaluate " ++ show (TC.ppJavaExpr expr) ++ "." -ppOverrideError (FalseAssertion p) = - "Assertion at " ++ show p ++ " is false." -ppOverrideError (AliasingInputs x y) = - "The expressions " ++ show (TC.ppJavaExpr x) ++ " and " ++ - show (TC.ppJavaExpr y) ++ - " point to the same reference, but are not allowed to alias each other." -ppOverrideError (JavaExceptionThrown _) = "A Java exception was thrown." -ppOverrideError (SimException s) = "Simulation exception: " ++ s ++ "." -ppOverrideError (InvalidType ty) = - "Invalid type in modify clause: " ++ show ty -ppOverrideError Abort = "Path was aborted." - -data OverrideResult - = SuccessfulRun (Path SharedContext) (Maybe Breakpoint) (Maybe SpecJavaValue) - | FailedRun (Path SharedContext) (Maybe Breakpoint) [OverrideError] - -type RunResult = ( Path SharedContext - , Maybe Breakpoint - , Either [OverrideError] (Maybe SpecJavaValue) - ) - -orParseResults :: [OverrideResult] -> [RunResult] -orParseResults l = - [ (ps, block, Left e) | FailedRun ps block e <- l ] ++ - [ (ps, block, Right v) | SuccessfulRun ps block v <- l ] - -type OverrideComputation m = - ContT OverrideResult (StateT OCState (SAWJavaSim m)) - -ocError :: OverrideError -> OverrideComputation m () -ocError e = modify $ \ocs -> ocs { ocsErrors = e : ocsErrors ocs } - --- OverrideComputation utilities {{{2 - --- | Runs an evaluate within an override computation. -ocEval :: (EvalContext -> ExprEvaluator b) - -> (b -> OverrideComputation m ()) - -> OverrideComputation m () -ocEval fn m = do - ec <- gets ocsEvalContext - res <- runEval (fn ec) - case res of - Left e -> ocError $ UndefinedExpr (evalErrExpr e) - Right v -> m v - -ocDoesEval :: (EvalContext -> ExprEvaluator b) - -> OverrideComputation m Bool -ocDoesEval fn = do - ec <- gets ocsEvalContext - res <- runEval (fn ec) - return $ either (const False) (const True) res - --- Modify result state -ocModifyResultState :: (SpecPathState -> SpecPathState) - -> OverrideComputation m () -ocModifyResultState fn = do - bcs <- get - put $! bcs { ocsResultState = fn (ocsResultState bcs) } - -ocModifyResultStateIO :: (SpecPathState -> IO SpecPathState) - -> OverrideComputation m () -ocModifyResultStateIO fn = do - bcs <- get - new <- liftIO $ fn $ ocsResultState bcs - put $! bcs { ocsResultState = new } - -ocSetReturnValue :: Maybe SpecJavaValue - -> OverrideComputation m () -ocSetReturnValue mrv = do - bcs <- get - let ec = ocsEvalContext bcs - ec' = ec { ecReturnValue = mrv } - put $! bcs { ocsEvalContext = ec' } - -ocSetJavaExpr :: JavaExpr -> SpecJavaValue - -> OverrideComputation m () -ocSetJavaExpr e v = do - ocEval (setJavaExpr e v) $ \ec -> do - modify $ \ocs -> ocs { ocsEvalContext = ec } - -- Anything other than a local or the return value should be set in - -- the result state, as well. - case e of - CC.Term (ReturnVal _ ) -> return () - CC.Term (Local _ _ _) -> ocError (UndefinedExpr e) - CC.Term (InstanceField refExpr f) -> - ocEval (evalJavaRefExpr refExpr) $ \lhsRef -> - ocModifyResultState $ setInstanceFieldValuePS lhsRef f v - CC.Term (StaticField f) -> - ocModifyResultState $ setStaticFieldValuePS f v - --- | Add assumption for predicate. -ocAssert :: Pos -> String -> Term -> OverrideComputation m () -ocAssert p _nm x = do - sc <- (ecContext . ocsEvalContext) <$> get - case asBool x of - Just True -> return () - Just False -> ocError (FalseAssertion p) - _ -> ocModifyResultStateIO (addAssertionPS sc x) - --- ocStep {{{2 - -ocStep :: BehaviorCommand -> OverrideComputation m () -ocStep (EnsureInstanceField _pos refExpr f rhsExpr) = - ocEval (evalJavaRefExpr refExpr) $ \lhsRef -> - ocEval (evalMixedExpr (fieldIdType f) rhsExpr) $ \value -> - ocModifyResultState $ setInstanceFieldValuePS lhsRef f value -ocStep (EnsureStaticField _pos f rhsExpr) = - ocEval (evalMixedExpr (fieldIdType f) rhsExpr) $ \value -> - ocModifyResultState $ setStaticFieldValuePS f value -ocStep (EnsureArray _pos lhsExpr rhsExpr) = - ocEval (evalJavaRefExpr lhsExpr) $ \lhsRef -> - ocEval (evalMixedExprAsLogic (exprType lhsExpr) rhsExpr) $ \rhsVal -> do - sc <- gets (ecContext . ocsEvalContext) - ty <- liftIO $ scTypeOf sc rhsVal >>= scWhnf sc - case ty of - (isVecType (const (return ())) -> Just (n :*: _)) -> - ocModifyResultState $ setArrayValuePS lhsRef (fromIntegral n) rhsVal - _ -> ocError (InvalidType (show ty)) -ocStep (ModifyInstanceField refExpr f) = - ocEval (evalJavaRefExpr refExpr) $ \lhsRef -> do - sc <- gets (ecContext . ocsEvalContext) - let tp = fieldIdType f - w = fromIntegral $ stackWidth tp - logicType <- liftIO $ scBitvector sc (fromInteger w) - n <- liftIO $ scFreshGlobal sc (TC.ppJavaExpr refExpr) logicType - v <- liftIO $ mkJSSValue sc tp n - ocModifyResultState $ setInstanceFieldValuePS lhsRef f v -ocStep (ModifyStaticField f) = do - sc <- gets (ecContext . ocsEvalContext) - let tp = fieldIdType f - w = fromIntegral $ stackWidth tp - logicType <- liftIO $ scBitvector sc (fromInteger w) - n <- liftIO $ scFreshGlobal sc (ppFldId f) logicType - v <- liftIO $ mkJSSValue sc tp n - ocModifyResultState $ setStaticFieldValuePS f v -ocStep (ModifyArray refExpr ty) = - ocEval (evalJavaRefExpr refExpr) $ \ref -> do - sc <- gets (ecContext . ocsEvalContext) - case ty of - ArrayInstance n tp -> do - rhsVal <- liftIO $ do - elTy <- scBitvector sc (fromIntegral (stackWidth tp)) - lTm <- scNat sc (fromIntegral n) - aty <- scVecType sc lTm elTy - scFreshGlobal sc (TC.ppJavaExpr refExpr) aty - ocModifyResultState $ setArrayValuePS ref (fromIntegral n) rhsVal - _ -> ocError (InvalidType (show ty)) -ocStep (ReturnValue expr) = do - mrty <- gets (ecReturnType . ocsEvalContext) - case mrty of - Just rty -> - ocEval (evalMixedExpr rty expr) $ \val -> - ocSetReturnValue (Just val) - Nothing -> fail "Return type specification given for method of type void." - --- Executing overrides {{{2 - -execBehavior :: Method - -> BehaviorSpec - -> SharedContext - -> Maybe Ref - -> [(LocalVariableIndex, SpecJavaValue)] - -> SpecPathState - -> SAWJavaSim m [RunResult] -execBehavior meth bsl sc mbThis argLocals ps = do - - -- Get state of current execution path in simulator. - fmap orParseResults $ forM [bsl] $ \bs -> do - let ec = EvalContext { ecContext = sc - , ecLocals = Map.fromList $ - case mbThis of - Just th -> (0, RValue th) : argLocals - Nothing -> argLocals - , ecReturnType = methodReturnType meth - , ecReturnValue = Nothing - , ecPathState = ps - } - let initOCS = - OCState { ocsLoc = bsLoc bs - , ocsEvalContext = ec - , ocsResultState = ps - , ocsErrors = [] - } - let resCont () = do - OCState { ocsLoc = loc - , ocsResultState = resPS - , ocsEvalContext = ecres - , ocsErrors = l } <- get - return $ - if null l then - SuccessfulRun resPS (Just loc) (ecReturnValue ecres) - else - FailedRun resPS (Just loc) l - flip evalStateT initOCS $ flip runContT resCont $ do - -- If any of the reference expressions mentioned in the spec - -- doesn't already evaluate to a reference, we need to allocate - -- it. - forM_ (sortBy (compare `on` exprDepth) (bsRefExprs bsl)) $ \e -> do - exists <- ocDoesEval (evalJavaExpr e) - unless exists $ do - r <- lift $ lift $ genRef (exprType e) - ocSetJavaExpr e (RValue r) - - ec' <- gets ocsEvalContext - -- Check that all expressions that reference each other may do so. - do -- Build map from references to expressions that map to them. - let exprs = bsRefExprs bs - ocEval (\_ -> mapM (flip evalJavaRefExpr ec') exprs) $ \refs -> do - let refExprMap = - Map.fromListWith (++) $ refs `zip` [[e] | e <- exprs] - --- Get counterexamples. - let mayAliasSet = bsMayAliasSet bs - let badPairs = catMaybes - $ map (\cl -> CC.checkEquivalence cl mayAliasSet) - $ Map.elems refExprMap - -- Throw error if counterexample is found. - case badPairs of - [] -> return () - (x,y):_ -> ocError (AliasingInputs x y) - -- Verify the initial logic assignments - forM_ (bsLogicAssignments bs) $ \(pos, lhs, rhs) -> do - ocEval (evalJavaExprAsLogic lhs) $ \lhsVal -> - ocEval (evalMixedExprAsLogic (exprType lhs) rhs) $ \rhsVal -> - ocAssert pos "Override value assertion" - =<< liftIO (scEq sc lhsVal rhsVal) - -- Verify assumptions - forM_ (bsAssumptions bs) $ \le -> do - ocEval (evalLogicExpr le) $ \assumptions -> - ocAssert (PosInternal "assumption") "Override assumption check" assumptions - -- Execute statements. - mapM_ ocStep (bsCommands bs) - -checkClassesInitialized :: MonadSim SharedContext m => - Pos -> String -> [ClassName] - -> SAWJavaSim m () -checkClassesInitialized pos nm requiredClasses = do - forM_ requiredClasses $ \c -> do - mem <- getMem (PP.text "checkClassesInitialized") - let status = Map.lookup c (mem ^. memInitialization) - when (status /= Just Initialized) $ - let msg = "The method spec \'" ++ nm ++ - "\' requires that the class " ++ slashesToDots (unClassName c) ++ - " is initialized. SAWScript does not " ++ - "currently support methods that initialize new classes." - in throwIOExecException pos (ftext msg) "" - -execOverride :: MonadSim SharedContext m - => SharedContext - -> Pos - -> JavaMethodSpecIR - -> Maybe Ref - -> [Value Term] - -> SAWJavaSim m () -execOverride sc pos ir mbThis args = do - -- Execute behaviors. - let bsl = specBehaviors ir -- Map.lookup (BreakPC 0) (specBehaviors ir) -- TODO - let method = specMethod ir - argLocals = map (localIndexOfParameter method) [0..] `zip` args - -- Check class initialization. - checkClassesInitialized pos (specName ir) (specInitializedClasses ir) - initPS <- getPath "execOverride" - res <- execBehavior method bsl sc mbThis argLocals initPS - -- Create function for generation resume actions. - case res of - [(_, _, Left el)] -> do - let msg = "Unsatisified assertions in " ++ specName ir ++ ":\n" - ++ intercalate "\n" (map ppOverrideError el) - fail msg - [(ps, _, Right mval)] -> - modifyPathM_ (PP.text "path result") $ \_ -> - return $ - case (mval, ps ^. pathStack) of - -- If the current path stack is empty, the result of the - -- override is the return value of the current method. - (_, []) -> ps & set pathRetVal mval - -- If the current path stack is non-empty and the override - -- returned a value, put it on the operand stack of the - -- current call frame. - (Just val, (f:fr)) -> ps & set pathStack (f' : fr) - where f' = f & cfOpds %~ (val :) - -- If the current path stack is non-empty and the override - -- returned no value, leave the state alone. - (Nothing, _:_) -> ps - [] -> fail "Zero paths returned from override execution." - _ -> fail "More than one path returned from override execution." - --- | Add a method override for the given method to the simulator. -overrideFromSpec :: MonadSim SharedContext m => - SharedContext - -> Pos - -> JavaMethodSpecIR - -> SAWJavaSim m () -overrideFromSpec de pos ir - | methodIsStatic method = - overrideStaticMethod cName key $ \args -> - execOverride de pos ir Nothing args - | otherwise = - overrideInstanceMethod cName key $ \thisVal args -> - execOverride de pos ir (Just thisVal) args - where cName = className (specMethodClass ir) - method = specMethod ir - key = methodKey method - -data VerifyParams = VerifyParams - { vpCode :: Codebase - , vpContext :: SharedContext - , vpOpts :: Options - , vpSpec :: JavaMethodSpecIR - , vpOver :: [JavaMethodSpecIR] - } - -type SymbolicRunHandler = - SharedContext -> [PathVC Breakpoint] -> TopLevel () -type Prover = - VerifyState -> Int -> Term -> TopLevel () - -runValidation :: Prover -> VerifyParams -> SymbolicRunHandler -runValidation prover params sc results = do - let ir = vpSpec params - printLn = printOutLnTop - opts <- fmap rwPPOpts getTopLevelRW - forM_ results $ \pvc -> do - let mkVState nm cfn = - VState { vsVCName = nm - , vsMethodSpec = ir - , vsVerbosity = case Opts.verbLevel (vpOpts params) of - Opts.Silent -> 0 - Opts.OnlyCounterExamples -> 0 - Opts.Error -> 1 - Opts.Warn -> 2 - Opts.Info -> 3 - _ -> 4 - , vsCounterexampleFn = cfn - , vsStaticErrors = pvcStaticErrors pvc - } - if null (pvcStaticErrors pvc) then - forM_ (zip [0..] (pvcChecks pvc)) $ \(n, vc) -> do - let vs = mkVState (vcName vc) (vcCounterexample sc opts vc) - g <- io $ scImplies sc (pvcAssumptions pvc) =<< vcGoal sc vc - printOutTop Debug $ "Checking " ++ vcName vc - printOutTop ExtraDebug $ " (" ++ scPrettyTerm defaultPPOpts g ++ ")" - printOutTop Debug "" - prover vs n g - else do - let vsName = "an invalid path" - let vs = mkVState vsName (\_ -> return $ vcat (pvcStaticErrors pvc)) - false <- io $ scBool sc False - g <- io $ scImplies sc (pvcAssumptions pvc) false - printLn Info $ "Checking " ++ vsName - printLn Info $ show $ pvcStaticErrors pvc - printLn Debug $ "Calling prover to disprove " ++ - scPrettyTerm defaultPPOpts (pvcAssumptions pvc) - prover vs 0 g - -data VerifyState = VState { - vsVCName :: String - , vsMethodSpec :: JavaMethodSpecIR - , vsVerbosity :: Verbosity - -- | Starting Block is used for checking VerifyAt commands. - -- , vsFromBlock :: BlockId - -- | Evaluation context used for parsing expressions during - -- verification. - -- , vsEvalContext :: EvalContext - , vsCounterexampleFn :: CounterexampleFn - , vsStaticErrors :: [SawDoc] - } - -{- Alternative implementation of JavaMethodSpec -} - -initializeVerification' :: MonadSim SharedContext m - => SharedContext - -- ^ The SharedContext for creating new symbolic - -- expressions. - -> JavaMethodSpecIR - -- ^ The specification of the overall method. - -> BehaviorSpec - -- ^ The particular behavioral specification that - -- we are checking. - -> RefEquivConfiguration - -- ^ The particular relationship between which references - -- alias each other for verification purposes. - -> SAWJavaSim m SpecPathState -initializeVerification' sc ir bs refConfig = do - -- Generate a reference for each reference equivalence class that - -- isn't entirely involved in a return expression. Sort by depth so - -- that we create enclosing objects before enclosed objects. - let refConfig' = sortBy (compare `on` (maximum . map exprDepth . fst)) $ - filter (not . all containsReturn . fst) refConfig - exprRefs <- mapM (genRef . jssTypeOfActual . snd) refConfig' - let refAssignments = (exprRefs `zip` map fst refConfig') - pushFrame cs = case mcs' of - Nothing -> fail "internal: failed to push call frame" - Just cs' -> return cs' - where - mcs' = pushCallFrame - (className (specMethodClass ir)) - (specMethod ir) - entryBlock -- FIXME: not the right block - Map.empty - cs - forM_ (specInitializedClasses ir) initializeClass - modifyCSM_ pushFrame - forM_ refAssignments $ \(r, cl) -> - forM_ cl $ \e -> writeJavaValue e (RValue r) - lcs <- liftIO $ bsLogicClasses bs refConfig' - case lcs of - Nothing -> - let msg = "Unresolvable cyclic dependencies between assumptions." - in throwIOExecException (specPos ir) (ftext msg) "" - Just assignments -> mapM_ (\(l, t, r) -> setClassValues sc l t r) assignments - getPath (PP.text "initializeVerification") - -evalLogicExpr' :: MonadSim SharedContext m => - SharedContext -> LogicExpr - -> SAWJavaSim m Term -evalLogicExpr' sc initExpr = do - let exprs = logicExprJavaExprs initExpr - args <- forM exprs $ \expr -> do - t <- readJavaTermSim sc expr - return (expr, t) - let argMap = Map.fromList args - argTerms = mapMaybe (\k -> Map.lookup k argMap) $ - logicExprJavaExprs initExpr - liftIO $ useLogicExpr sc initExpr argTerms - -resolveClassRHS :: MonadSim SharedContext m => - SharedContext - -> JavaExpr - -> JavaActualType - -> [LogicExpr] - -> SAWJavaSim m TypedTerm -resolveClassRHS sc e tp [] = do - mlty <- liftIO $ TC.narrowTypeOfActual sc tp - case (mlty, tp) of - (Just lty, PrimitiveType pt) | pt /= LongType -> do - liftIO $ (scFreshGlobal sc (jeVarName e) lty >>= - mkTypedTerm sc) - (Just lty, _) -> do - liftIO $ (scFreshGlobal sc (jeVarName e) lty >>= mkTypedTerm sc) - (Nothing, _) -> - fail $ "Can't convert Java type to logic type: " ++ - show (TC.ppActualType tp) -resolveClassRHS sc _ _ [r] = do - t <- evalLogicExpr' sc r - liftIO $ mkTypedTerm sc t -resolveClassRHS _ _ _ _ = - fail "Not yet implemented." - -setClassValues :: (MonadSim SharedContext m) => - SharedContext - -> [JavaExpr] - -> JavaActualType - -> [LogicExpr] - -> SAWJavaSim m () -setClassValues sc l tp rs = - forM_ l $ \e -> - unless (containsReturn e) $ do - t <- resolveClassRHS sc e tp rs - writeJavaTerm sc e t - -valueEqTerm :: (Fail.MonadFail m, MonadIO m) => - SharedContext - -> String - -> SpecPathState - -> Type - -> SpecJavaValue - -> Term - -> StateT (PathVC Breakpoint) m () -valueEqTerm sc name ps ty v t = do - t' <- termOfValue sc ps ty v - pvcgAssertEq name t' t - -valueEqValue :: (Fail.MonadFail m, MonadIO m) => - SharedContext - -> String - -> SpecPathState - -> SpecJavaValue - -> SpecPathState - -> SpecJavaValue - -> StateT (PathVC Breakpoint) m () -valueEqValue _ _ _ (IValue i) _ (IValue i') | i == i' = return () -valueEqValue _ _ _ (LValue l) _ (LValue l') | l == l' = return () -valueEqValue _ _ _ (DValue d) _ (DValue d') | isNaN d && isNaN d' = return () -valueEqValue _ _ _ (DValue d) _ (DValue d') | d == d' = return () -valueEqValue _ _ _ (FValue f) _ (FValue f') | isNaN f && isNaN f' = return () -valueEqValue _ _ _ (FValue f) _ (FValue f') | f == f' = return () -valueEqValue _ _ _ (RValue r) _ (RValue r') | r == r' = return () -valueEqValue _sc name _ (IValue t) _ (IValue t') = do - pvcgAssertEq name t t' -valueEqValue _ name _ (LValue t) _ (LValue t') = - pvcgAssertEq name t t' -valueEqValue _ name ps (RValue r) ps' (RValue r') = do - let ma = Map.lookup r (ps ^. pathMemory . memScalarArrays) - ma' = Map.lookup r' (ps' ^. pathMemory . memScalarArrays) - case (ma, ma') of - (Just (len, t), Just (len', t')) - | len == len' -> pvcgAssertEq name t t' - | otherwise -> fail $ "valueEqValue: array sizes don't match: " ++ show (len, len') - _ -> fail $ "valueEqValue: " ++ name ++ ": ref does not point to array" -valueEqValue _ name _ v _ v' = fail $ "valueEqValue: " ++ name ++ ": unspported value type: " ++ show v ++ ", " ++ show v' - -readJavaValueVerif :: (Fail.MonadFail m) => - VerificationState - -> Path' Term - -> JavaExpr - -> m SpecJavaValue -readJavaValueVerif vs ps refExpr = do - let initPS = vsInitialState vs - readJavaValue ((^. cfLocals) <$> currentCallFrame initPS) ps refExpr - -checkStep :: (Fail.MonadFail m, MonadIO m) => - VerificationState - -> SpecPathState - -> BehaviorCommand - -> StateT (PathVC Breakpoint) m () -checkStep vs ps (ReturnValue expr) = do - let mrty = methodReturnType (specMethod (vsSpec vs)) - t <- liftIO $ mixedExprToTerm (vsContext vs) (vsInitialState vs) expr - case (ps ^. pathRetVal, mrty) of - (Just rv, Just rty) -> valueEqTerm (vsContext vs) "return" ps rty rv t - (Nothing, _) -> fail "Return specification provided, but method did not return a value." - (_, Nothing) -> fail "Return specification provided, but method has void type." -checkStep vs ps (EnsureInstanceField _pos refExpr f rhsExpr) = do - rv <- readJavaValueVerif vs ps refExpr - case rv of - RValue ref -> do - let mfv = getInstanceFieldValuePS ps ref f - case mfv of - Just fv -> do - ft <- liftIO $ mixedExprToTerm (vsContext vs) (vsInitialState vs) rhsExpr - valueEqTerm (vsContext vs) (ppJavaExpr refExpr ++ "." ++ fieldIdName f) ps (fieldIdType f) fv ft - Nothing -> fail "Invalid instance field in java_ensure_eq." - _ -> fail "Left-hand side of . did not evaluate to a reference." -checkStep vs ps (EnsureStaticField _pos f rhsExpr) = do - let mfv = getStaticFieldValuePS ps f - ft <- liftIO $ mixedExprToTerm (vsContext vs) (vsInitialState vs) rhsExpr - case mfv of - Just fv -> valueEqTerm (vsContext vs) (ppFldId f) ps (fieldIdType f) fv ft - Nothing -> fail "Invalid static field in java_ensure_eq." -checkStep _vs _ps (ModifyInstanceField _refExpr _f) = return () -checkStep _vs _ps (ModifyStaticField _f) = return () -checkStep vs ps (EnsureArray _pos refExpr rhsExpr) = do - rv <- readJavaValueVerif vs ps refExpr - t <- liftIO $ mixedExprToTerm (vsContext vs) (vsInitialState vs) rhsExpr - case rv of - RValue (Ref _ ty) -> - valueEqTerm (vsContext vs) (ppJavaExpr refExpr) ps ty rv t - _ -> fail "Non-reference value in EnsureArray" -checkStep _vs _ps (ModifyArray _refExpr _aty) = return () - -data VerificationState = VerificationState - { vsContext :: SharedContext - , vsSpec :: JavaMethodSpecIR - , vsInitialState :: SpecPathState - } - -checkFinalState :: MonadSim SharedContext m => - SharedContext - -> JavaMethodSpecIR - -> BehaviorSpec - -> RefEquivConfiguration - -> SpecPathState - -> SAWJavaSim m (PathVC Breakpoint) -checkFinalState sc ms bs cl initPS = do - let st = VerificationState { vsContext = sc - , vsSpec = ms - , vsInitialState = initPS - } - cmds = bsCommands bs - finalPS <- getPath "checkFinalState" - let maybeRetVal = finalPS ^. pathRetVal - initLocals = (^. cfLocals) <$> currentCallFrame initPS - refList <- forM (concatMap fst cl) $ \e -> do - rv <- readJavaValue initLocals finalPS e - case rv of - RValue r -> return (r, e) - _ -> fail "internal: refMap" - let refMap = Map.fromList refList - assumptions <- liftIO $ evalAssumptions sc initPS (specAssumptions ms) - let initState = - PathVC { pvcStartLoc = bsLoc bs - , pvcEndLoc = Nothing - , pvcAssumptions = assumptions - , pvcStaticErrors = [] - , pvcChecks = [] - } - let mentionedSFields = - Set.fromList $ - [ fid | EnsureStaticField _ fid _ <- cmds] ++ - [ fid | ModifyStaticField fid <- cmds ] - mentionedIFieldExprs = - [ (e, fid) | EnsureInstanceField _ e fid _ <- cmds] ++ - [ (e, fid) | ModifyInstanceField e fid <- cmds ] - mentionedArrayExprs = - [ e | EnsureArray _ e _ <- cmds] ++ - [ e | ModifyArray e _ <- cmds ] - mentionedIFields <- forM mentionedIFieldExprs $ \(e, fid) -> do - -- TODO: best combination of initLocals and finalPS unclear here. - rv <- readJavaValue initLocals finalPS e - case rv of - RValue r -> return (r, fid) - _ -> fail "internal: mentionedIFields" - mentionedArrays <- forM mentionedArrayExprs $ \e -> do - -- TODO: best combination of initLocals and finalPS unclear here. - rv <- readJavaValue initLocals finalPS e - case rv of - RValue r -> return r - _ -> fail "internal: mentionedArrays" - let mentionedIFieldSet = Set.fromList mentionedIFields - let mentionedArraySet = Set.fromList mentionedArrays - let mcf = currentCallFrame initPS - args <- case mcf of - Just cf -> return (Map.elems (cf ^. cfLocals)) - Nothing -> fail "internal: no call frame in initial path state" - let reachable = reachableRefs finalPS (maybeToList maybeRetVal ++ args) - flip execStateT initState $ do - mapM_ (checkStep st finalPS) cmds - let initMem = initPS ^. pathMemory - finalMem = finalPS ^. pathMemory - initRefArrays = initMem ^. memRefArrays - finalRefArrays = finalMem ^. memRefArrays - when (initMem ^. memInitialization /= finalMem ^. memInitialization) $ - let newClasses = Map.keys ((finalMem ^. memInitialization) `Map.difference` - (initMem ^. memInitialization)) in - unless (specAllowAlloc ms) $ - pvcgFail (pretty ("Initializes extra classes " ++ show newClasses)) - when (initMem ^. memClassObjects /= finalMem ^. memClassObjects) $ - pvcgFail "Allocates a class object." - when (Map.keys initRefArrays /= Map.keys finalRefArrays) $ - unless (specAllowAlloc ms) $ - pvcgFail "Allocates a reference array" - forM_ (Map.toList initRefArrays) $ \(r, a) -> - case Map.lookup r finalRefArrays of - Just a' -> when (a /= a') $ pvcgFail "Modifies a reference array." - Nothing -> pvcgFail "Reference array disappeared?" - forM_ (Map.toList (finalMem ^. memStaticFields)) $ \(f, fval) -> - unless (Set.member f mentionedSFields) $ - unless(isArrayType (fieldIdType f)) $ - let fieldDesc = unClassName (fieldIdClass f) ++ "." ++ fieldIdName f in - case Map.lookup f (initMem ^. memStaticFields) of - Nothing -> pvcgFail $ hsep - [ ftext "Modifies the unspecified static field" - , ftext fieldDesc - , "of type" - , ftext (show (fieldIdType f)) - ] - Just ival -> valueEqValue sc fieldDesc initPS ival finalPS fval - forM_ (Map.toList (finalMem ^. memInstanceFields)) $ \((ref, f), fval) -> do - unless (Set.member (ref, f) mentionedIFieldSet) $ - when (ref `Set.member` reachable && not (isArrayType (fieldIdType f))) $ - let fname = - case Map.lookup ref refMap of - Just e -> ppJavaExpr e ++ "." ++ fieldIdName f - Nothing -> "field " ++ fieldIdName f ++ " of a new object" - in - case Map.lookup (ref, f) (initMem ^. memInstanceFields) of - Nothing -> pvcgFail $ hsep - [ ftext "Modifies the unspecified instance field" - , ftext fname - , "of type" - , ftext (show (fieldIdType f)) - ] - Just ival -> do - valueEqValue sc fname initPS ival finalPS fval - forM_ (Map.toList (finalMem ^. memScalarArrays)) $ \(ref, (flen, fval)) -> - unless (Set.member ref mentionedArraySet) $ - when (ref `Set.member` reachable) $ - case Map.lookup ref (initMem ^. memScalarArrays) of - Nothing -> unless (specAllowAlloc ms) $ - pvcgFail "Allocates scalar array." - Just (ilen, ival) - | ilen == flen -> - let aname = - case Map.lookup ref refMap of - Just e -> ppJavaExpr e - Nothing -> "a new array" - in - pvcgAssertEq aname ival fval -- TODO: name - | otherwise -> pvcgFail $ hsep - [ "Array changed size from" - , pretty ilen - , "to" - , pretty flen - ] - -- TODO: check that return value has been specified if method returns a value - pvcgAssert "final assertions" (finalPS ^. pathAssertions) diff --git a/src/SAWScript/JavaMethodSpec/Evaluator.hs b/src/SAWScript/JavaMethodSpec/Evaluator.hs deleted file mode 100644 index 78f163fe53..0000000000 --- a/src/SAWScript/JavaMethodSpec/Evaluator.hs +++ /dev/null @@ -1,159 +0,0 @@ -module SAWScript.JavaMethodSpec.Evaluator - ( EvalContext(..) - , ExprEvaluator - , runEval - , evalJavaExpr - , setJavaExpr - , evalJavaExprAsLogic - , evalJavaRefExpr - , evalLogicExpr - , evalMixedExpr - , evalMixedExprAsLogic - , ExprEvalError(..) - -- * Utilities - , SpecPathState - , SpecJavaValue - , addAssertionPS - , setArrayValuePS - ) where - -import Control.Lens -import Control.Monad (forM) -import Control.Monad.IO.Class -import Control.Monad.Trans.Except -import Data.Map.Strict (Map) -import qualified Data.Map.Strict as Map -import Data.Maybe (mapMaybe) - -import qualified SAWScript.CongruenceClosure as CC (Term(..)) -import qualified SAWScript.JavaExpr as TC -import SAWScript.JavaUtils - -import Execution.JavaSemantics (AtomicValue(..)) -import Verifier.Java.Codebase (LocalVariableIndex, FieldId, Type) -import Verifier.Java.Common - - -import Verifier.SAW.SharedTerm - --- EvalContext {{{1 - --- | Contextual information needed to evaluate expressions. -data EvalContext = EvalContext { - ecContext :: SharedContext - , ecReturnType :: Maybe Type - , ecLocals :: Map LocalVariableIndex SpecJavaValue - , ecReturnValue :: Maybe SpecJavaValue - , ecPathState :: SpecPathState - } - --- ExprEvalError {{{1 - -data ExprEvalError - = EvalExprUndefined TC.JavaExpr - | EvalExprBadJavaType String TC.JavaExpr - | EvalExprBadLogicType String String - | EvalExprUnknownArray TC.JavaExpr - | EvalExprUnknownLocal LocalVariableIndex TC.JavaExpr - | EvalExprUnknownField FieldId TC.JavaExpr - | EvalExprNoReturn TC.JavaExpr - deriving Show - - --- ExprEvaluator {{{1 - -type ExprEvaluator a = ExceptT ExprEvalError IO a - -runEval :: MonadIO m => ExprEvaluator b -> m (Either ExprEvalError b) -runEval v = liftIO (runExceptT v) - --- N.B. This method assumes that the Java path state is well-formed, the the --- JavaExpression syntactically referes to the correct type of method (static --- versus instance), and correct well-typed arguments. It does not assume that --- all the instanceFields in the JavaEvalContext are initialized. -evalJavaExpr :: TC.JavaExpr -> EvalContext -> ExprEvaluator SpecJavaValue -evalJavaExpr expr ec = eval expr - where eval (CC.Term app) = - case app of - TC.ReturnVal _ -> - case ecReturnValue ec of - Just rv -> return rv - Nothing -> throwE (EvalExprNoReturn expr) - TC.Local _ idx _ -> - case Map.lookup idx (ecLocals ec) of - Just v -> return v - Nothing -> throwE $ EvalExprUnknownLocal idx expr - TC.InstanceField r f -> do - RValue ref <- eval r - let ifields = (ecPathState ec) ^. pathMemory . memInstanceFields - case Map.lookup (ref, f) ifields of - Just v -> return v - Nothing -> throwE $ EvalExprUnknownField f expr - TC.StaticField f -> do - let sfields = (ecPathState ec) ^. pathMemory . memStaticFields - case Map.lookup f sfields of - Just v -> return v - Nothing -> throwE $ EvalExprUnknownField f expr - -setJavaExpr :: TC.JavaExpr -> SpecJavaValue -> EvalContext - -> ExprEvaluator EvalContext -setJavaExpr (CC.Term app) v ec = - case app of - TC.ReturnVal _ -> - return (ec { ecReturnValue = Just v }) - TC.Local _ idx _ -> - return (ec { ecLocals = Map.insert idx v (ecLocals ec) }) - TC.InstanceField r f -> do - RValue ref <- evalJavaExpr r ec - return (ec { ecPathState = - setInstanceFieldValuePS ref f v (ecPathState ec) }) - TC.StaticField f -> do - return (ec { ecPathState = - setStaticFieldValuePS f v (ecPathState ec) }) - -evalJavaExprAsLogic :: TC.JavaExpr -> EvalContext -> ExprEvaluator Term -evalJavaExprAsLogic expr ec = do - val <- evalJavaExpr expr ec - case val of - RValue r -> - let arrs = (ecPathState ec) ^. pathMemory . memScalarArrays in - case Map.lookup r arrs of - Nothing -> throwE $ EvalExprUnknownArray expr - Just (_,n) -> return n - IValue n -> liftIO $ truncateIValue (ecContext ec) (TC.exprType expr) n - LValue n -> return n - _ -> throwE $ EvalExprBadJavaType "evalJavaExprAsLogic" expr - --- | Return Java value associated with mixed expression. -evalMixedExpr :: Type - -> TC.MixedExpr - -> EvalContext - -> ExprEvaluator SpecJavaValue -evalMixedExpr ty (TC.LE expr) ec = do - n <- evalLogicExpr expr ec - liftIO $ mkJSSValue (ecContext ec) ty n -evalMixedExpr _ (TC.JE expr) ec = evalJavaExpr expr ec - --- | Evaluates a typed expression in the context of a particular state. -evalLogicExpr :: TC.LogicExpr -> EvalContext -> ExprEvaluator Term -evalLogicExpr initExpr ec = do - let sc = ecContext ec - exprs = TC.logicExprJavaExprs initExpr - args <- forM exprs $ \expr -> do - t <- evalJavaExprAsLogic expr ec - return (expr, t) - let argMap = Map.fromList args - argTerms = mapMaybe (\k -> Map.lookup k argMap) $ - TC.logicExprJavaExprs initExpr - liftIO $ TC.useLogicExpr sc initExpr argTerms - -evalJavaRefExpr :: TC.JavaExpr -> EvalContext -> ExprEvaluator Ref -evalJavaRefExpr expr ec = do - val <- evalJavaExpr expr ec - case val of - RValue ref -> return ref - _ -> throwE $ EvalExprBadJavaType "evalJavaRefExpr" expr - -evalMixedExprAsLogic :: Type -> TC.MixedExpr -> EvalContext -> ExprEvaluator Term -evalMixedExprAsLogic _ (TC.LE expr) = evalLogicExpr expr -evalMixedExprAsLogic _ (TC.JE expr) = evalJavaExprAsLogic expr diff --git a/src/SAWScript/JavaMethodSpecIR.hs b/src/SAWScript/JavaMethodSpecIR.hs deleted file mode 100644 index f43548ed59..0000000000 --- a/src/SAWScript/JavaMethodSpecIR.hs +++ /dev/null @@ -1,464 +0,0 @@ -{- | -Module : SAWScript.JavaMethodSpecIR -Description : Provides typechecked representation for method specifications and function for creating it from AST representation. -License : BSD3 -Maintainer : jhendrix, atomb -Stability : provisional --} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DoAndIfThenElse #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} - -module SAWScript.JavaMethodSpecIR - (-- * MethodSpec record - JavaMethodSpecIR - , specName - , specPos - , specCodebase - , specThisClass - , specMethod - , specMethodClass - , specInitializedClasses - , specBehaviors - , specAddBehaviorCommand - , specAddVarDecl - , specAddLogicAssignment - , specAddAliasSet - , specAddAssumption - , specActualTypeMap - , specAllowAlloc - , specSetAllowAllocation - , specAssumptions - , initMethodSpec - --, resolveMethodSpecIR - -- * Method behavior. - , BehaviorSpec - , bsLoc - , bsRefExprs - , bsMayAliasSet - , RefEquivConfiguration - , bsRefEquivClasses - , bsActualTypeMap - , bsLogicAssignments - , bsAssumptions - , bsLogicClasses - , bsCheckAliasTypes - , BehaviorCommand(..) - , bsCommands - -- * Equivalence classes for references. - , JavaExprEquivClass - , ppJavaExprEquivClass - , ppMethodSpec - ) where - --- Imports {{{1 - -#if !MIN_VERSION_base(4,8,0) -import Control.Applicative -#endif -import Control.Monad -import Data.Graph.Inductive (scc, Gr, mkGraph) -import Data.List (intercalate, sort) -import Data.Map (Map) -import qualified Data.Map as Map -import Data.Maybe (catMaybes) -import qualified Data.Set as Set -import qualified Data.Vector as V -import Prettyprinter - -import qualified Verifier.Java.Codebase as JSS -import qualified Verifier.Java.Common as JSS - ---import Verifier.SAW.TypedAST (ppTerm, defaultPPOpts) -import Verifier.SAW.Term.Pretty (SawDoc, ppTerm, defaultPPOpts) - -import qualified SAWScript.CongruenceClosure as CC -import SAWScript.CongruenceClosure (CCSet) -import SAWScript.JavaExpr -import SAWScript.Position (Pos(..)) -import SAWScript.Utils - --- ExprActualTypeMap {{{1 - --- | Maps Java expressions for references to actual type. -type ExprActualTypeMap = Map JavaExpr JavaActualType - --- Alias definitions {{{1 - -type JavaExprEquivClass = [JavaExpr] - --- | Returns a name for the equivalence class. -ppJavaExprEquivClass :: JavaExprEquivClass -> String -ppJavaExprEquivClass [] = error "internal: ppJavaExprEquivClass" -ppJavaExprEquivClass [expr] = ppJavaExpr expr -ppJavaExprEquivClass cl = "{ " ++ intercalate ", " (map ppJavaExpr (sort cl)) ++ " }" - --- BehaviorSpec {{{1 - --- | Postconditions used for implementing behavior specification. All --- LogicExprs in behavior commands need to be extracted with --- useLogicExpr, in a specific shared context, before they can be --- used. -data BehaviorCommand - -- | Assign Java expression the value given by the mixed expression. - = EnsureInstanceField Pos JavaExpr JSS.FieldId MixedExpr - -- | Assign static Java field the value given by the mixed expression. - | EnsureStaticField Pos JSS.FieldId MixedExpr - -- | Assign array value of Java expression the value given by the rhs. - | EnsureArray Pos JavaExpr MixedExpr - -- | Modify the Java expression to an arbitrary value. - -- May point to integral type or array. - | ModifyInstanceField JavaExpr JSS.FieldId - -- | Modify the Java static field to an arbitrary value. - | ModifyStaticField JSS.FieldId - -- | Modify the Java array to an arbitrary value. - -- May point to integral type or array. - | ModifyArray JavaExpr JavaActualType - -- | Specifies value method returns. - | ReturnValue MixedExpr - deriving (Show) - -data BehaviorSpec = BS { - -- | Program counter for spec. - bsLoc :: JSS.Breakpoint - -- | Maps all expressions seen along path to actual type. - , bsActualTypeMap :: ExprActualTypeMap - -- | Stores which Java expressions must alias each other. - , bsMustAliasSet :: CCSet JavaExprF - -- | May alias relation between Java expressions. - , bsMayAliasClasses :: [[JavaExpr]] - -- | Equations - , bsLogicAssignments :: [(Pos, JavaExpr, MixedExpr)] - -- | Conditions assumed by this specification. - , bsAssumptions :: [LogicExpr] - -- | Commands to execute in reverse order. - , bsReversedCommands :: [BehaviorCommand] - } deriving (Show) - --- TODO: Change this when 'ppJavaExpr' is converted to prettyprinter -prettyJavaExpr :: JavaExpr -> Doc ann -prettyJavaExpr = pretty . ppJavaExpr - --- TODO: Change this when 'ppJavaExpr' is converted to prettyprinter -prettyActualType :: JavaActualType -> Doc ann -prettyActualType = pretty . ppActualType - --- TODO: avoid intermediate conversion to 'String' -prettyClassName :: JSS.ClassName -> Doc ann -prettyClassName = pretty . JSS.unClassName - -ppLogicExpr :: LogicExpr -> SawDoc -ppLogicExpr (LogicExpr t args) = - vcat $ - parens (ppTerm defaultPPOpts t) : - map prettyJavaExpr args - -ppMixedExpr :: MixedExpr -> SawDoc -ppMixedExpr (JE je) = prettyJavaExpr je -ppMixedExpr (LE le) = ppLogicExpr le - -ppBehaviorCommand :: BehaviorCommand -> SawDoc -ppBehaviorCommand cmd = - case cmd of - (EnsureInstanceField _ je f me) -> - "sets instance field" <+> - prettyJavaExpr je <> "." <> ppField f <+> - "to" <+> ppMixedExpr me - (EnsureStaticField _ f me) -> - "sets static field" <+> - ppStaticField f <+> - "to" <+> ppMixedExpr me - (EnsureArray _ je me) -> - "sets array" <+> prettyJavaExpr je <+> - "to" <+> ppMixedExpr me - (ModifyInstanceField je f) -> - "modifies instance field" <+> - prettyJavaExpr je <> "." <> ppField f - (ModifyStaticField f) -> - "modifies static field" <+> - ppStaticField f - (ModifyArray je _) -> - "modifies array" <+> prettyJavaExpr je - (ReturnValue me) -> - "returns" <+> ppMixedExpr me - where - ppField f = pretty (JSS.fieldIdName f) - ppStaticField f = - prettyClassName (JSS.fieldIdClass f) <> "." <> ppField f - -ppBehavior :: BehaviorSpec -> SawDoc -ppBehavior bs = - vcat [ "Assumes the following types for Java locations:" - , indent 2 $ vcat $ map ppActualTypeEntry $ - Map.toList (bsActualTypeMap bs) - , "" - , "Assumes the following sets of references must alias:" - , indent 2 $ vcat $ map ppSet $ CC.toList $ bsMustAliasSet bs - , "" - , "Assumes the following sets of references may alias:" - , indent 2 $ vcat $ map ppSet $ bsMayAliasClasses bs - , "" - , "Assumes the following set of assignments:" - , indent 2 $ vcat $ map ppAssign $ bsLogicAssignments bs - , "" - , "Assumes the following preconditions:" - , indent 2 $ vcat $ map ppLogicExpr $ bsAssumptions bs - , "" - , "Ensures the following postconditions:" - , indent 2 $ vcat $ map ppBehaviorCommand $ bsCommands bs - , "" - ] - where - ppActualTypeEntry (e, t) = - prettyJavaExpr e <+> "::" <+> prettyActualType t - ppSet = - hcat . map prettyJavaExpr - ppAssign (_, je, me) = - prettyJavaExpr je <+> ":=" <+> ppMixedExpr me - -ppMethodSpec :: JavaMethodSpecIR -> SawDoc -ppMethodSpec ms = - vcat [ "Java Method specification." - , "" - , "Instance class:" <+> prettyClassName (JSS.className (specThisClass ms)) - , "Definition class:" <+> prettyClassName (JSS.className (specMethodClass ms)) - , "Method:" <+> pretty (JSS.methodName (specMethod ms)) - , "" - , "Requires these classes to be initialized:" - , indent 2 $ vcat $ map prettyClassName $ specInitializedClasses ms - , "" - , if specAllowAlloc ms - then "Allows allocation." - else "Does not allow allocation." - , "" - , ppBehavior $ specBehaviors ms - ] - --- | Returns list of all Java expressions that are references. -bsExprs :: BehaviorSpec -> [JavaExpr] -bsExprs bs = Map.keys (bsActualTypeMap bs) - --- | Returns list of all Java expressions that are references. -bsRefExprs :: BehaviorSpec -> [JavaExpr] -bsRefExprs bs = filter isRefJavaExpr (bsExprs bs) - -bsMayAliasSet :: BehaviorSpec -> CCSet JavaExprF -bsMayAliasSet bs = - CC.foldr CC.insertEquivalenceClass - (bsMustAliasSet bs) - (bsMayAliasClasses bs) - --- | Check that all expressions that may alias have equal types. -bsCheckAliasTypes :: Pos -> BehaviorSpec -> IO () -bsCheckAliasTypes pos bs = mapM_ checkClass (CC.toList (bsMayAliasSet bs)) - where atm = bsActualTypeMap bs - checkClass [] = error "internal: Equivalence class empty" - checkClass (x:l) = do - let Just xType = Map.lookup x atm - forM l $ \y -> do - let Just yType = Map.lookup x atm - when (xType /= yType) $ do - let msg = "Different types are assigned to " ++ show x ++ " and " ++ show y ++ "." - res = "All references that may alias must be assigned the same type." - throwIOExecException pos (ftext msg) res - -type RefEquivConfiguration = [(JavaExprEquivClass, JavaActualType)] - --- | Returns all possible potential equivalence classes for spec. -bsRefEquivClasses :: BehaviorSpec -> [RefEquivConfiguration] -bsRefEquivClasses bs = - map (map parseSet . CC.toList) $ Set.toList $ - CC.mayAliases (bsMayAliasClasses bs) (bsMustAliasSet bs) - where parseSet l@(e:_) = - case Map.lookup e (bsActualTypeMap bs) of - Just tp -> (l,tp) - Nothing -> error $ "internal: bsRefEquivClass given bad expression: " ++ show e - parseSet [] = error "internal: bsRefEquivClasses given empty list." - -bsPrimitiveExprs :: BehaviorSpec -> [JavaExpr] -bsPrimitiveExprs bs = - [ e | (e, PrimitiveType _) <- Map.toList (bsActualTypeMap bs) ] - -bsLogicEqs :: BehaviorSpec -> [(JavaExpr, JavaExpr)] -bsLogicEqs bs = - [ (lhs, rhs) | (_, lhs, JE rhs) <- bsLogicAssignments bs ] - --- | Returns logic assignments to equivance class. -bsAssignmentsForClass :: BehaviorSpec -> JavaExprEquivClass - -> [LogicExpr] -bsAssignmentsForClass bs cl = res - where s = Set.fromList cl - res = [ rhs - | (_, lhs, LE rhs) <- bsLogicAssignments bs - , Set.member lhs s - ] - --- | Retuns ordering of Java expressions to corresponding logic value. -bsLogicClasses :: BehaviorSpec - -> RefEquivConfiguration - -> IO (Maybe [(JavaExprEquivClass, JavaActualType, [LogicExpr])]) -bsLogicClasses bs cfg = do - let allClasses = CC.toList - -- Add logic equations. - $ flip (foldr (uncurry CC.insertEquation)) (bsLogicEqs bs) - -- Add primitive expression. - $ flip (foldr CC.insertTerm) (bsPrimitiveExprs bs) - -- Create initial set with references. - $ CC.fromList (map fst cfg) - logicClasses <- (catMaybes <$>) $ - forM allClasses $ \(cl@(e:_)) -> - case Map.lookup e (bsActualTypeMap bs) of - Just (ClassInstance _) -> return Nothing - Just at -> return (Just (cl, at)) - Nothing -> return Nothing - let v = V.fromList logicClasses - -- Create nodes. - grNodes = [0..] `zip` logicClasses - -- Create edges - exprNodeMap = Map.fromList [ (e,n) | (n,(cl,_)) <- grNodes, e <- cl ] - grEdges = [ (s,t,()) | (t,(cl,_)) <- grNodes - , src:_ <- [bsAssignmentsForClass bs cl] - , se <- logicExprJavaExprs src - , let Just s = Map.lookup se exprNodeMap ] - -- Compute strongly connected components. - components = scc (mkGraph grNodes grEdges :: Gr (JavaExprEquivClass, JavaActualType) ()) - return $ if all (\l -> length l == 1) components - then Just [ (cl, at, bsAssignmentsForClass bs cl) - | [n] <- components - , let (cl,at) = v V.! n ] - else Nothing - --- Command utilities {{{2 - --- | Return commands in behavior in order they appeared in spec. -bsCommands :: BehaviorSpec -> [BehaviorCommand] -bsCommands = reverse . bsReversedCommands - -bsAddCommand :: BehaviorCommand -> BehaviorSpec -> BehaviorSpec -bsAddCommand bc bs = - bs { bsReversedCommands = bc : bsReversedCommands bs } - -bsAddAssumption :: LogicExpr -> BehaviorSpec -> BehaviorSpec -bsAddAssumption le bs = - bs { bsAssumptions = le : bsAssumptions bs } - -initMethodSpec :: Pos -> JSS.Codebase - -> JSS.Class -> String - -> IO JavaMethodSpecIR -initMethodSpec pos cb thisClass mname = do - (methodClass,method) <- findMethod cb pos mname thisClass - superClasses <- JSS.supers cb thisClass - let this = thisJavaExpr thisClass - initTypeMap | JSS.methodIsStatic method = Map.empty - | otherwise = Map.singleton this (ClassInstance thisClass) - initBS = BS { bsLoc = JSS.BreakEntry - , bsActualTypeMap = initTypeMap - , bsMustAliasSet = - if JSS.methodIsStatic method then - CC.empty - else - CC.insertTerm this CC.empty - , bsMayAliasClasses = [] - , bsLogicAssignments = [] - , bsAssumptions = [] - , bsReversedCommands = [] - } - initMS = MSIR { specPos = pos - , specCodebase = cb - , specThisClass = thisClass - , specMethodClass = methodClass - , specMethod = method - , specInitializedClasses = - map JSS.className superClasses - , specBehaviors = initBS - , specAllowAlloc = False - } - return initMS - --- JavaMethodSpecIR {{{1 - --- | This class captures the spec for the overall method. -data JavaMethodSpecIR = MSIR { - -- | The position of the specification for error reporting purposes. - specPos :: Pos - -- | The codebase containing the method being specified. - , specCodebase :: JSS.Codebase - -- | Class used for this instance. - , specThisClass :: JSS.Class - -- | Class where method is defined. - , specMethodClass :: JSS.Class - -- | Method to verify. - , specMethod :: JSS.Method - -- | Class names expected to be initialized using JVM "/" separators. - -- (as opposed to Java "." path separators). Currently this is set - -- to the list of superclasses of specThisClass. - , specInitializedClasses :: [JSS.ClassName] - -- | Behavior specifications for method at different PC values. - -- A list is used because the behavior may depend on the inputs. - , specBehaviors :: BehaviorSpec -- Map JSS.Breakpoint [BehaviorSpec] - -- | Whether this method is allowed to (invisibly) allocate new objects. - , specAllowAlloc :: Bool - } - --- | Return user printable name of method spec (currently the class + method name). -specName :: JavaMethodSpecIR -> String -specName ir = - let clName = JSS.className (specThisClass ir) - mName = JSS.methodName (specMethod ir) - in JSS.slashesToDots (JSS.unClassName clName) ++ ('.' : mName) - --- TODO: error if already declared -specAddVarDecl :: JavaExpr -> JavaActualType - -> JavaMethodSpecIR -> JavaMethodSpecIR -specAddVarDecl expr jt ms = ms { specBehaviors = bs' - , specInitializedClasses = cs' - } - where bs = specBehaviors ms - cs = specInitializedClasses ms - cs' = case jt of - ClassInstance c -> JSS.className c : cs - _ -> cs - bs' = bs { bsActualTypeMap = - Map.insert expr jt (bsActualTypeMap bs) - , bsMustAliasSet = - if isRefJavaExpr expr then - CC.insertTerm expr (bsMustAliasSet bs) - else - bsMustAliasSet bs - } - -specAddLogicAssignment :: Pos -> JavaExpr -> MixedExpr - -> JavaMethodSpecIR -> JavaMethodSpecIR -specAddLogicAssignment pos expr t ms = ms { specBehaviors = bs' } - where bs = specBehaviors ms - las = bsLogicAssignments bs - bs' = bs { bsLogicAssignments = (pos, expr, t) : las } - -specAddAliasSet :: [JavaExpr] -> JavaMethodSpecIR -> JavaMethodSpecIR -specAddAliasSet exprs ms = ms { specBehaviors = bs' } - where bs = specBehaviors ms - bs' = bs { bsMayAliasClasses = exprs : bsMayAliasClasses bs } - -specAddBehaviorCommand :: BehaviorCommand - -> JavaMethodSpecIR -> JavaMethodSpecIR -specAddBehaviorCommand bc ms = - ms { specBehaviors = bsAddCommand bc (specBehaviors ms) } - - -specAddAssumption :: LogicExpr -> JavaMethodSpecIR -> JavaMethodSpecIR -specAddAssumption le ms = - ms { specBehaviors = bsAddAssumption le (specBehaviors ms)} - -specActualTypeMap :: JavaMethodSpecIR -> Map JavaExpr JavaActualType -specActualTypeMap = bsActualTypeMap . specBehaviors - -specSetAllowAllocation :: JavaMethodSpecIR -> JavaMethodSpecIR -specSetAllowAllocation ms = ms { specAllowAlloc = True } - -specAssumptions :: JavaMethodSpecIR -> [LogicExpr] -specAssumptions = bsAssumptions . specBehaviors diff --git a/src/SAWScript/JavaPretty.hs b/src/SAWScript/JavaPretty.hs index 9d9108bd99..2efb246874 100644 --- a/src/SAWScript/JavaPretty.hs +++ b/src/SAWScript/JavaPretty.hs @@ -14,7 +14,7 @@ import Prettyprinter import Language.JVM.Common -import Verifier.Java.Codebase +import Lang.JVM.Codebase prettyClass :: Class -> Doc ann prettyClass cls = vcat $ diff --git a/src/SAWScript/JavaUtils.hs b/src/SAWScript/JavaUtils.hs deleted file mode 100644 index 0fc3e70067..0000000000 --- a/src/SAWScript/JavaUtils.hs +++ /dev/null @@ -1,456 +0,0 @@ -{- | -Module : SAWScript.JavaUtils -Description : Miscellaneous utilities for Java. -License : BSD3 -Maintainer : atomb -Stability : provisional --} -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE MonoLocalBinds #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ViewPatterns #-} - -module SAWScript.JavaUtils where - -#if !MIN_VERSION_base(4,8,0) -import Control.Applicative -#endif -import Control.Lens -import Control.Monad -import qualified Control.Monad.Fail as Fail -import Control.Monad.IO.Class -import qualified Data.Array as Array -import Data.Int -import Data.IORef -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Set as Set - -import Verifier.Java.Simulator as JSS -import Verifier.Java.SAWImport -import Verifier.SAW.Recognizer -import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedTerm - -import qualified SAWScript.CongruenceClosure as CC -import SAWScript.JavaExpr - -type SAWBackend = SharedContext -type SpecPathState = Path SharedContext -type SpecJavaValue = Value Term -type SAWJavaSim = Simulator SharedContext -type LocalMap t = Map.Map LocalVariableIndex (Value t) - -boolExtend' :: SharedContext -> Term -> IO Term -boolExtend' sc x = do - n31 <- scNat sc 31 - n1 <- scNat sc 1 - scBvUExt sc n31 n1 x - -arrayApply :: SharedContext - -> (SharedContext -> Term -> Term -> IO b) - -> Term -> IO b -arrayApply sc fn tm = do - ty <- scTypeOf sc =<< scWhnf sc tm - case ty of - (asVecType -> Just (n :*: _)) -> do - l <- scNat sc n - fn sc l tm - _ -> fail "Invalid type passed to extendArray" - -extendToIValue :: SharedContext -> JSS.Type -> Term -> IO Term -extendToIValue sc ty tm = do - case ty of - JSS.BooleanType -> scApplyJava_boolExtend sc tm - JSS.ByteType -> scApplyJava_byteExtend sc tm - JSS.ShortType -> scApplyJava_shortExtend sc tm - JSS.CharType -> scApplyJava_charExtend sc tm - JSS.IntType -> return tm - JSS.ArrayType JSS.BooleanType -> arrayApply sc scApplyJava_extendBoolArray tm - JSS.ArrayType JSS.ByteType -> arrayApply sc scApplyJava_extendByteArray tm - JSS.ArrayType JSS.CharType -> arrayApply sc scApplyJava_extendCharArray tm - JSS.ArrayType JSS.ShortType -> arrayApply sc scApplyJava_extendShortArray tm - JSS.ArrayType JSS.IntType -> return tm - _ -> fail $ "Invalid type passed to extendToIValue: " ++ show ty - -truncateIValue :: SharedContext -> JSS.Type -> Term -> IO Term -truncateIValue sc ty tm = do - case ty of - JSS.BooleanType -> scApplyJava_boolTrunc sc tm - JSS.ByteType -> scApplyJava_byteTrunc sc tm - JSS.ShortType -> scApplyJava_shortTrunc sc tm - JSS.CharType -> scApplyJava_shortTrunc sc tm - JSS.IntType -> return tm - JSS.ArrayType JSS.BooleanType -> arrayApply sc scApplyJava_truncBoolArray tm - JSS.ArrayType JSS.ByteType -> arrayApply sc scApplyJava_truncByteArray tm - JSS.ArrayType JSS.CharType -> arrayApply sc scApplyJava_truncCharArray tm - JSS.ArrayType JSS.ShortType -> arrayApply sc scApplyJava_truncShortArray tm - JSS.ArrayType JSS.IntType -> return tm - _ -> fail $ "Invalid type passed to truncateIValue: " ++ show ty - -termTypeCompatible :: SharedContext -> Term -> JSS.Type -> IO Bool -termTypeCompatible sc tm ty = do - tm' <- scWhnf sc tm - case (tm', ty) of - (asBoolType -> Just (), JSS.BooleanType) -> return True - (asBitvectorType -> Just 8, JSS.ByteType) -> return True - (asBitvectorType -> Just 16, JSS.ShortType) -> return True - (asBitvectorType -> Just 16, JSS.CharType) -> return True - (asBitvectorType -> Just 32, JSS.IntType) -> return True - (asBitvectorType -> Just 64, JSS.LongType) -> return True - (asVecType -> Just (_ :*: elty), JSS.ArrayType ety) -> - termTypeCompatible sc elty ety - _ -> return False - -termTypeToJSSType :: SharedContext -> Term -> IO JSS.Type -termTypeToJSSType sc t = do - ty <- scWhnf sc t - case ty of - (asBoolType -> Just ()) -> return JSS.BooleanType - (asBitvectorType -> Just 8) -> return JSS.ByteType - (asBitvectorType -> Just 16) -> return JSS.ShortType - (asBitvectorType -> Just 32) -> return JSS.IntType - (asBitvectorType -> Just 64) -> return JSS.IntType - (asVecType -> Just (_ :*: ety)) -> - JSS.ArrayType <$> termTypeToJSSType sc ety - _ -> fail "Invalid type for termTypeToJSSType" - --- SpecPathState {{{1 - --- | Add assertion for predicate to path state. -addAssertionPS :: SharedContext -> Term - -> SpecPathState - -> IO SpecPathState -addAssertionPS sc x p = do - p & pathAssertions %%~ \a -> liftIO (scAnd sc a x) - --- | Set value bound to array in path state. --- Assumes value is an array with a ground length. -setArrayValuePS :: Ref -> Int32 -> Term - -> SpecPathState - -> SpecPathState -setArrayValuePS r n v = - pathMemory . memScalarArrays %~ Map.insert r (n, v) - --- | Set value of bound to instance field in path state. -setInstanceFieldValuePS :: Ref -> FieldId -> SpecJavaValue - -> SpecPathState -> SpecPathState -setInstanceFieldValuePS r f v = - pathMemory . memInstanceFields %~ Map.insert (r, f) v - --- | Set value of bound to static field in path state. -setStaticFieldValuePS :: FieldId -> SpecJavaValue - -> SpecPathState -> SpecPathState -setStaticFieldValuePS f v = - pathMemory . memStaticFields %~ Map.insert f v - --- | Get value of bound to instance field in path state. -getInstanceFieldValuePS :: SpecPathState -> Ref -> FieldId - -> Maybe SpecJavaValue -getInstanceFieldValuePS ps r f = - Map.lookup (r, f) (ps ^. pathMemory . memInstanceFields) - --- | Get value of bound to static field in path state. -getStaticFieldValuePS :: SpecPathState -> FieldId - -> Maybe SpecJavaValue -getStaticFieldValuePS ps f = - Map.lookup f (ps ^. pathMemory . memStaticFields) - --- | Returns value constructor from node. -mkJSSValue :: SharedContext -> Type -> Term -> IO SpecJavaValue -mkJSSValue _ (ClassType _) _ = fail "mkJSSValue called on class type" -mkJSSValue _ (ArrayType _) _ = fail "mkJSSValue called on array type" -mkJSSValue _ FloatType _ = fail "mkJSSValue called on float type" -mkJSSValue _ DoubleType _ = fail "mkJSSValue called on double type" -mkJSSValue sc LongType n = do - ty <- scTypeOf sc n - case ty of - (asBitvectorType -> Just 64) -> return (LValue n) - _ -> fail "internal: invalid LValue passed to mkJSSValue." -mkJSSValue sc ty n = IValue <$> extendToIValue sc ty n - -writeJavaTerm :: (MonadSim SharedContext m) => - SharedContext - -> JavaExpr - -> TypedTerm - -> Simulator SharedContext m () -writeJavaTerm sc e tm = do - v <- valueOfTerm sc (exprType e) tm - writeJavaValue e v - -writeJavaValue :: (MonadSim SharedContext m) => - JavaExpr - -> SpecJavaValue - -> Simulator SharedContext m () -writeJavaValue (CC.Term e) v = - case e of - ReturnVal _ -> fail "Can't set return value" - Local _ idx _ -> setLocal idx v - InstanceField rexp f -> do - rv <- readJavaValueSim rexp - case rv of - RValue r -> setInstanceFieldValue r f v - _ -> fail "Instance argument of instance field evaluates to non-reference" - StaticField f -> setStaticFieldValue f v - -writeJavaValuePS :: (Fail.MonadFail m) => - JavaExpr - -> SpecJavaValue - -> SpecPathState - -> m SpecPathState -writeJavaValuePS (CC.Term e) v ps = - case e of - ReturnVal _ -> return (ps & set pathRetVal (Just v)) - Local _ i _ -> - case ps ^. pathStack of - [] -> fail "no stack frames" - (cf:cfs) -> do - let cf' = cf & cfLocals %~ Map.insert i v - return (ps & pathStack .~ (cf':cfs)) - InstanceField rexp f -> do - rv <- readJavaValue ((^. cfLocals) <$> currentCallFrame ps) ps rexp - case rv of - RValue r -> return (setInstanceFieldValuePS r f v ps) - _ -> fail "Instance argument of instance field evaluates to non-reference" - StaticField f -> return (setStaticFieldValuePS f v ps) - -readJavaTerm :: (Fail.MonadFail m, MonadIO m) => - SharedContext -> Maybe (LocalMap Term) -> Path' Term -> JavaExpr -> m Term -readJavaTerm sc mcf ps et = - termOfValue sc ps (exprType et) =<< readJavaValue mcf ps et - -readJavaTermSim :: (Functor m, Monad m) => - SharedContext - -> JavaExpr - -> Simulator SharedContext m Term -readJavaTermSim sc e = do - ps <- getPath "readJavaTermSim" - readJavaTerm sc ((^. cfLocals) <$> currentCallFrame ps) ps e - -termOfValue :: (Fail.MonadFail m, MonadIO m) => - SharedContext -> Path' Term -> JSS.Type -> SpecJavaValue -> m Term -termOfValue sc _ tp (IValue t) = liftIO $ truncateIValue sc tp t -termOfValue _ _ _ (LValue t) = return t -termOfValue sc ps tp (RValue r@(Ref _ (ArrayType ety))) = do - case (Map.lookup r (ps ^. pathMemory . memScalarArrays), ety) of - (Just (_, a), JSS.LongType) -> return a - (Just (_, a), _) -> liftIO $ truncateIValue sc tp a - (Nothing, _) -> fail "Reference not found in arrays map" -termOfValue _ _ _ (RValue (Ref _ (ClassType _))) = - fail "Translating objects to terms not yet implemented" -- TODO -termOfValue _ _ _ _ = fail "Can't convert term to value" - -termOfValueSim :: (Functor m, Monad m) => - SharedContext -> JSS.Type -> SpecJavaValue - -> Simulator SharedContext m Term -termOfValueSim sc tp v = do - ps <- getPath "termOfValueSim" - termOfValue sc ps tp v - -valueOfTerm :: (MonadSim SharedContext m) => - SharedContext - -> JSS.Type - -> TypedTerm - -> Simulator SharedContext m SpecJavaValue -valueOfTerm sc jty (TypedTerm _schema t) = do - ty <- liftIO $ (scTypeOf sc t >>= scWhnf sc) - case (ty, jty) of - (asBoolType -> Just (), JSS.BooleanType) -> IValue <$> (liftIO $ scApplyJava_boolExtend sc t) - -- TODO: remove the following case when no longer needed, and use extendToIValue - (asBitvectorType -> Just 1, JSS.BooleanType) -> IValue <$> (liftIO $ scApplyJava_byteExtend sc t) - (asBitvectorType -> Just 8, JSS.ByteType) -> IValue <$> (liftIO $ scApplyJava_byteExtend sc t) - (asBitvectorType -> Just 16, JSS.ShortType) -> IValue <$> (liftIO $ scApplyJava_shortExtend sc t) - (asBitvectorType -> Just 16, JSS.CharType) -> IValue <$> (liftIO $ scApplyJava_charExtend sc t) - (asBitvectorType -> Just 32, JSS.IntType) -> return (IValue t) - (asBitvectorType -> Just 64, JSS.LongType) -> return (LValue t) - (asVecType -> Just (n :*: _), JSS.ArrayType JSS.LongType) -> do - RValue <$> newSymbolicArray (ArrayType JSS.LongType) (fromIntegral n) t - (asVecType -> Just (n :*: _), JSS.ArrayType ety) -> do - t' <- liftIO $ extendToIValue sc jty t - RValue <$> newSymbolicArray (ArrayType ety) (fromIntegral n) t' - _ -> fail $ "Can't translate term of type: " ++ show ty ++ " to Java type " ++ show jty --- If vector of other things, allocate array, translate those things, and store --- If record, allocate appropriate object, translate fields, assign fields --- For the last case, we need information about the desired Java type - --- NB: the CallFrame parameter allows this function to use a different --- call frame than the one in the current state, which can be useful to --- access parameters of a method that has returned. -readJavaValue :: (Fail.MonadFail m) => - Maybe (LocalMap Term) - -> Path' Term - -> JavaExpr - -> m SpecJavaValue -readJavaValue mlocals ps (CC.Term e) = do - case e of - ReturnVal _ -> - case ps ^. pathRetVal of - Just rv -> return rv - Nothing -> fail "Return value not found" - Local _ idx _ -> - case mlocals of - Just locals -> - case Map.lookup idx locals of - Just v -> return v - Nothing -> fail $ "Local variable " ++ show idx ++ " not found" - Nothing -> fail "Trying to read local variable with no call frame." - InstanceField rexp f -> do - rv <- readJavaValue mlocals ps rexp - case rv of - RValue ref -> do - let ifields = ps ^. pathMemory . memInstanceFields - case Map.lookup (ref, f) ifields of - Just fv -> return fv - _ -> fail $ "Instance field '" ++ fieldIdName f ++ "' not found." - _ -> fail "Object of instance field selector evaluated to non-reference." - StaticField f -> do - let sfields = ps ^. pathMemory . memStaticFields - case Map.lookup f sfields of - Just v -> return v - _ -> fail $ "Static field '" ++ fieldIdName f ++ - "' not found in class '" ++ JSS.unClassName (fieldIdClass f) ++ "'" - -readJavaValueSim :: (Monad m) => - JavaExpr - -> Simulator SharedContext m SpecJavaValue -readJavaValueSim e = do - ps <- getPath "readJavaValueSim" - readJavaValue ((^. cfLocals) <$> currentCallFrame ps) ps e - -logicExprToTerm :: SharedContext - -> Maybe (LocalMap Term) - -> Path' Term -> LogicExpr - -> IO Term -logicExprToTerm sc mlocals ps le = do - let exprs = logicExprJavaExprs le - args <- forM exprs $ \expr -> do - t <- readJavaTerm sc mlocals ps expr - return (expr, t) - let argMap = Map.fromList args - argTerms = mapMaybe (\k -> Map.lookup k argMap) exprs - useLogicExpr sc le argTerms - --- NB: uses call frame from path -mixedExprToTerm :: SharedContext - -> Path' Term -> MixedExpr - -> IO Term -mixedExprToTerm sc ps me = do - let mlocals = (^. cfLocals) <$> currentCallFrame ps - case me of - LE le -> logicExprToTerm sc mlocals ps le - JE je -> readJavaTerm sc mlocals ps je - -logicExprToTermSim :: (Functor m, Monad m) => - SharedContext - -> LogicExpr - -> Simulator SAWBackend m Term -logicExprToTermSim sc le = do - ps <- getPath "logicExprToTermSim" - liftIO $ logicExprToTerm sc ((^. cfLocals) <$> currentCallFrame ps) ps le - -freshJavaVal :: (MonadIO m, Functor m) => - Maybe (IORef [Term]) - -> SharedContext - -> JavaActualType - -> Simulator SAWBackend m SpecJavaValue -freshJavaVal _ _ (PrimitiveType ty) = do - case ty of - BooleanType -> withSBE $ \sbe -> IValue <$> freshBool sbe - ByteType -> withSBE $ \sbe -> IValue <$> freshByte sbe - CharType -> withSBE $ \sbe -> IValue <$> freshChar sbe - ShortType -> withSBE $ \sbe -> IValue <$> freshShort sbe - IntType -> withSBE $ \sbe -> IValue <$> freshInt sbe - LongType -> withSBE $ \sbe -> LValue <$> freshLong sbe - _ -> fail $ "Can't create fresh primitive value of type " ++ show ty -freshJavaVal argsRef sc (ArrayInstance n ty) | isPrimitiveType ty = do - -- TODO: should this use bvAt? - elts <- liftIO $ do - ety <- scBitvector sc (fromIntegral (JSS.stackWidth ty)) - ntm <- scNat sc (fromIntegral n) - aty <- scVecType sc ntm ety - atm <- scFreshGlobal sc "_" aty - maybe (return ()) (\r -> modifyIORef r (atm :)) argsRef - mapM (scAt sc ntm ety atm) =<< mapM (scNat sc) [0..(fromIntegral n) - 1] - case ty of - LongType -> RValue <$> newLongArray elts - _ | isIValue ty -> RValue <$> newIntArray (ArrayType ty) elts - _ -> fail $ "Can't create array with element type " ++ show ty --- TODO: allow input declarations to specialize types of fields -freshJavaVal _ _ (ArrayInstance _ _) = - fail $ "Can't create fresh array of non-scalar elements" -freshJavaVal argsRef sc (ClassInstance c) = do - r <- createInstance (className c) Nothing - forM_ (classFields c) $ \f -> do - let ty = fieldType f - v <- freshJavaVal argsRef sc (PrimitiveType ty) - setInstanceFieldValue r (FieldId (className c) (fieldName f) ty) v - return (RValue r) - -isArrayType :: Type -> Bool -isArrayType (ArrayType _) = True -isArrayType _ = False - -refInstanceFields :: (Ord f) => - Map.Map (Ref, f) v - -> Ref - -> Map.Map f v -refInstanceFields m r = - Map.fromList [ (f, v) | ((mr, f), v) <- Map.toList m, mr == r ] - -pathRefInstanceFields :: Path SharedContext - -> Ref - -> Map.Map FieldId SpecJavaValue -pathRefInstanceFields ps = - refInstanceFields (ps ^. pathMemory . memInstanceFields) - -pathArrayRefs :: Path SharedContext - -> Ref - -> [Ref] -pathArrayRefs ps r = - concat - [ Array.elems a - | (ar, a) <- Map.toList (ps ^. pathMemory . memRefArrays) - , ar == r - ] - -pathStaticFieldRefs :: Path SharedContext - -> [Ref] -pathStaticFieldRefs ps = - valueRefs $ map snd $ Map.toList (ps ^. pathMemory . memStaticFields) - -reachableFromRef :: SpecPathState -> Set.Set Ref -> Ref -> Set.Set Ref -reachableFromRef _ seen r | r `Set.member` seen = Set.empty -reachableFromRef ps seen r = - Set.unions - [ Set.singleton r - , Set.unions (map (reachableFromRef ps seen') refArrayRefs) - , Set.unions (map (reachableFromRef ps seen') instFieldRefs) - ] - where refArrayRefs = pathArrayRefs ps r - instFieldRefs = valueRefs $ map snd $ Map.toList $ pathRefInstanceFields ps r - seen' = Set.insert r seen - -reachableRefs :: SpecPathState -> [SpecJavaValue] -> Set.Set Ref -reachableRefs ps vs = - Set.unions [ reachableFromRef ps Set.empty r | r <- roots ] - where roots = pathStaticFieldRefs ps ++ valueRefs vs - -valueRefs :: [SpecJavaValue] -> [Ref] -valueRefs vs = [ r | RValue r <- vs ] - -useLogicExprPS :: JSS.Path SharedContext - -> SharedContext - -> LogicExpr - -> IO Term -useLogicExprPS ps sc le = do - let mlocals = (^. cfLocals) <$> currentCallFrame ps - args <- mapM (readJavaTerm sc mlocals ps) (logicExprJavaExprs le) - useLogicExpr sc le args - -evalAssumptions :: SharedContext -> SpecPathState -> [LogicExpr] -> IO Term -evalAssumptions sc ps as = do - assumptionList <- mapM (useLogicExprPS ps sc) as - true <- scBool sc True - foldM (scAnd sc) true assumptionList diff --git a/src/SAWScript/Utils.hs b/src/SAWScript/Utils.hs index 7d5d9392e5..7fd23f49ea 100644 --- a/src/SAWScript/Utils.hs +++ b/src/SAWScript/Utils.hs @@ -38,7 +38,7 @@ import System.Exit import Text.Printf import Numeric(showFFloat) -import qualified Verifier.Java.Codebase as JSS +import qualified Lang.JVM.Codebase as JSS import SAWScript.Options import SAWScript.Position diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 057ed898f1..3028c1e4c2 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -62,13 +62,12 @@ import qualified Data.AIG as AIG import qualified SAWScript.AST as SS import qualified SAWScript.Exceptions as SS import qualified SAWScript.Position as SS -import qualified SAWScript.JavaMethodSpecIR as JIR import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMSLLVM import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible import qualified SAWScript.Crucible.JVM.MethodSpecIR () -import qualified Verifier.Java.Codebase as JSS +import qualified Lang.JVM.Codebase as JSS import qualified Text.LLVM.AST as LLVM (Type) import qualified Text.LLVM.PP as LLVM (ppType) import SAWScript.JavaExpr (JavaType(..)) @@ -128,8 +127,6 @@ data Value | VProofScript (ProofScript Value) | VSimpset Simpset | VTheorem Theorem - | VJavaSetup (JavaSetup Value) - | VJavaMethodSpec JIR.JavaMethodSpecIR ----- | VLLVMCrucibleSetup !(LLVMCrucibleSetupM Value) | VLLVMCrucibleMethodSpec (CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR) @@ -289,10 +286,8 @@ showsPrecValue opts p v = VTheorem (Theorem (Prop t) _stats) -> showString "Theorem " . showParen True (showString (SAWCorePP.scPrettyTerm opts' t)) - VJavaSetup {} -> showString "<>" VLLVMCrucibleSetup{} -> showString "<>" VLLVMCrucibleSetupValue{} -> showString "<>" - VJavaMethodSpec ms -> shows (JIR.ppMethodSpec ms) VLLVMCrucibleMethodSpec{} -> showString "<>" VLLVMModuleSkeleton s -> shows s VLLVMFunctionSkeleton s -> shows s @@ -556,26 +551,6 @@ typedTermOfString cs = TypedTerm schema trm -- Other SAWScript Monads ------------------------------------------------------ --- The ProofScript in RunVerify is in the SAWScript context, and --- should stay there. -data ValidationPlan - = Skip - | RunVerify (ProofScript SatResult) - -data JavaSetupState - = JavaSetupState { - jsSpec :: JIR.JavaMethodSpecIR - , jsContext :: SharedContext - , jsTactic :: ValidationPlan - , jsSimulate :: Bool - , jsSatBranches :: Bool - } - -type JavaSetup a = StateT JavaSetupState TopLevel a - -throwJava :: String -> JavaSetup a -throwJava = lift . throwTopLevel - type CrucibleSetup ext = Setup.CrucibleSetupT ext TopLevel -- | 'CrucibleMethodSpecIR' requires a specific syntax extension, but our method @@ -703,18 +678,6 @@ instance FromValue a => FromValue (StateT ProofState TopLevel a) where fromValue m2 fromValue _ = error "fromValue ProofScript" -instance IsValue a => IsValue (StateT JavaSetupState TopLevel a) where - toValue m = VJavaSetup (fmap toValue m) - -instance FromValue a => FromValue (StateT JavaSetupState TopLevel a) where - fromValue (VJavaSetup m) = fmap fromValue m - fromValue (VReturn v) = return (fromValue v) - fromValue (VBind _pos m1 v2) = do - v1 <- fromValue m1 - m2 <- lift $ applyValue v2 v1 - fromValue m2 - fromValue _ = error "fromValue JavaSetup" - --------------------------------------------------------------------------------- instance IsValue a => IsValue (LLVMCrucibleSetupM a) where toValue m = VLLVMCrucibleSetup (fmap toValue m) @@ -883,13 +846,6 @@ instance FromValue Theorem where fromValue (VTheorem t) = t fromValue _ = error "fromValue Theorem" -instance IsValue JIR.JavaMethodSpecIR where - toValue ms = VJavaMethodSpec ms - -instance FromValue JIR.JavaMethodSpecIR where - fromValue (VJavaMethodSpec ms) = ms - fromValue _ = error "fromValue JavaMethodSpec" - instance IsValue JavaType where toValue t = VJavaType t @@ -975,7 +931,6 @@ addTrace str val = VLambda f -> VLambda (\x -> addTrace str `fmap` addTraceTopLevel str (f x)) VTopLevel m -> VTopLevel (addTrace str `fmap` addTraceTopLevel str m) VProofScript m -> VProofScript (addTrace str `fmap` addTraceStateT str m) - VJavaSetup m -> VJavaSetup (addTrace str `fmap` addTraceStateT str m) VBind pos v1 v2 -> VBind pos (addTrace str v1) (addTrace str v2) VLLVMCrucibleSetup (LLVMCrucibleSetupM m) -> VLLVMCrucibleSetup $ LLVMCrucibleSetupM $ addTrace str `fmap` underStateT (addTraceTopLevel str) m