From d32a87c82953665ac251c6a56c3a66e0e44c5ba4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 9 Jun 2021 16:55:10 -0700 Subject: [PATCH 01/10] JVM contract compilation with up-to-date types --- .../src/SAWServer/JVMCrucibleSetup.hs | 195 +++++++++--------- 1 file changed, 93 insertions(+), 102 deletions(-) diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index bd5331d2b0..55e5a89d39 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -8,6 +8,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TupleSections #-} module SAWServer.JVMCrucibleSetup ( jvmLoadClass , compileJVMContract @@ -16,17 +17,10 @@ module SAWServer.JVMCrucibleSetup import Control.Exception (throw) import Control.Lens ( view ) import Control.Monad.IO.Class ( MonadIO(liftIO) ) -import Control.Monad.State - ( evalStateT, - MonadState(get, put), - MonadTrans(lift), - modify' ) import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) -import Data.Foldable ( traverse_ ) import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe ( maybeToList ) import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -35,6 +29,9 @@ import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) import SAWScript.Crucible.JVM.Builtins ( jvm_alloc_array, jvm_alloc_object, + jvm_elem_is, + jvm_field_is, + jvm_static_field_is, jvm_execute_func, jvm_fresh_var, jvm_postcond, @@ -52,8 +49,7 @@ import qualified Argo.Doc as Doc import SAWServer ( ServerName(..), SAWState, - SetupStep(..), - CrucibleSetupVal(CryptolExpr, NullValue, NamedValue), + CrucibleSetupVal(..), sawTask, setServerVal ) import SAWServer.Data.Contract @@ -86,113 +82,108 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where newtype ServerSetupVal = Val (SetupValue CJ.JVM) --- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now. compileJVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> CryptolEnv -> Contract JavaType (P.Expr P.PName) -> JVMSetupM () -compileJVMContract fileReader bic cenv c = interpretJVMSetup fileReader bic cenv steps +compileJVMContract fileReader bic cenv0 c = + do allocsPre <- mapM setupAlloc (preAllocated c) + (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) + mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) + mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) + --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func + allocsPost <- mapM setupAlloc (postAllocated c) + (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) + mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) + mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) + --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + case returnVal c of + Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return + Nothing -> return () where - setupFresh (ContractVar n dn ty) = SetupFresh n dn ty - setupAlloc (Allocated n ty mut align) = SetupAlloc n ty mut align - steps = - map setupFresh (preVars c) ++ - map SetupPrecond (preConds c) ++ - map setupAlloc (preAllocated c) ++ - map (\(PointsTo p v chkV cond) -> SetupPointsTo p v chkV cond) (prePointsTos c) ++ - [ SetupExecuteFunction (argumentVals c) ] ++ - map setupFresh (postVars c) ++ - map SetupPostcond (postConds c) ++ - map setupAlloc (postAllocated c) ++ - map (\(PointsTo p v chkV cond) -> SetupPointsTo p v chkV cond) (postPointsTos c) ++ - [ SetupReturn v | v <- maybeToList (returnVal c) ] - -interpretJVMSetup :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - [SetupStep JavaType] -> - JVMSetupM () -interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty, cenv0) - where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return - -- TODO: do we really want two names here? - go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ jvm_fresh_var debugName ty - (env, cenv) <- get - put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) - save name (Val (MS.SetupTerm t)) - go (SetupAlloc name _ _ (Just _)) = - error $ "attempted to allocate a Java object with alignment information: " ++ show name - go (SetupAlloc name (JavaArray n ty) True Nothing) = - lift (jvm_alloc_array n ty) >>= save name . Val - go (SetupAlloc name (JavaClass c) True Nothing) = - lift (jvm_alloc_object c) >>= save name . Val - go (SetupAlloc _ ty _ Nothing) = - error $ "cannot allocate type: " ++ show ty - go (SetupGhostValue _serverName _displayName _v) = get >>= \_env -> lift $ - error "nyi: ghost points-to" - go (SetupPointsTo src tgt _chkTgt _cond) = get >>= \env -> lift $ - do _ptr <- getSetupVal env src - _tgt' <- getSetupVal env tgt - error "nyi: points-to" - go (SetupExecuteFunction args) = - get >>= \env -> - lift $ traverse (getSetupVal env) args >>= jvm_execute_func - go (SetupPrecond p) = get >>= \env -> lift $ - getTypedTerm env p >>= jvm_precond - go (SetupPostcond p) = get >>= \env -> lift $ - getTypedTerm env p >>= jvm_postcond - - save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv)) - - getSetupVal :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - CrucibleSetupVal (P.Expr P.PName) -> - JVMSetupM (MS.SetupValue CJ.JVM) - getSetupVal _ NullValue = JVMSetupM $ return $ MS.SetupNull () - {- - getSetupVal env (ArrayValue elts) = - do elts' <- mapM (getSetupVal env) elts - JVMSetupM $ return $ MS.SetupArray () elts' - getSetupVal env (FieldLValue base fld) = - do base' <- getSetupVal env base - JVMSetupM $ return $ MS.SetupField () base' fld - getSetupVal env (ElementLValue base idx) = - do base' <- getSetupVal env base - JVMSetupM $ return $ MS.SetupElem () base' idx - getSetupVal _ (GlobalInitializer name) = - JVMSetupM $ return $ MS.SetupGlobalInitializer () name - getSetupVal _ (GlobalLValue name) = - JVMSetupM $ return $ MS.SetupGlobal () name - -} - getSetupVal (env, _) (NamedValue n) = JVMSetupM $ - resolve env n >>= - \case - Val x -> return x -- TODO add cases for the server values that - -- are not coming from the setup monad - -- (e.g. surrounding context) - getSetupVal env (CryptolExpr expr) = - do t <- getTypedTerm env expr - return (MS.SetupTerm t) - getSetupVal _ _sv = error $ "unrecognized setup value" -- ++ show sv + setupFresh :: ContractVar JavaType -> JVMSetupM (ServerName, TypedTerm) + setupFresh (ContractVar n dn ty) = + do t <- jvm_fresh_var dn ty + return (n, t) + setupState allocs (env, cenv) vars = + do freshTerms <- mapM setupFresh vars + let cenv' = foldr (\(ServerName n, t) -> CEnv.bindTypedTerm (mkIdent n, t)) cenv freshTerms + let env' = Map.union env $ Map.fromList $ + [ (n, Val (MS.SetupTerm t)) | (n, t) <- freshTerms ] ++ + [ (n, Val v) | (n, v) <- allocs ] + return (env', cenv') + + setupAlloc :: Allocated JavaType -> JVMSetupM (ServerName, MS.SetupValue CJ.JVM) + setupAlloc (Allocated _ _ False _) = + JVMSetupM $ fail "Immutable allocations not supported in JVM API." + setupAlloc (Allocated _ _ _ (Just _)) = + JVMSetupM $ fail "Alignment not supported in JVM API." + setupAlloc (Allocated n ty True Nothing) = + case ty of + JavaArray sz ety -> (n,) <$> jvm_alloc_array sz ety + JavaClass cname -> (n,) <$> jvm_alloc_object cname + _ -> JVMSetupM $ fail $ "Cannot allocate Java object of type " ++ show ty + + setupPointsTo _ (PointsTo _ _ (Just _) _) = + JVMSetupM $ fail "Points-to without type checking not supported in JVM API." + setupPointsTo _ (PointsTo _ _ _ (Just _)) = + JVMSetupM $ fail "Conditional points-to not supported in JVM API." + setupPointsTo env (PointsTo p v Nothing Nothing) = + do sv <- getSetupVal env v + case p of + FieldLValue base fld -> + getSetupVal env base >>= \o -> jvm_field_is o fld sv + ElementLValue base eidx -> + getSetupVal env base >>= \o -> jvm_elem_is o eidx sv + GlobalLValue name -> jvm_static_field_is name sv + _ -> JVMSetupM $ fail "Invalid points-to statement." + + --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." + + resolve :: Map ServerName a -> ServerName -> JVMSetupM a + resolve env name = + JVMSetupM $ + case Map.lookup name env of + Just v -> return v + Nothing -> fail $ unlines + [ "Server value " ++ show name ++ " not found - impossible!" -- rule out elsewhere + , show (Map.keys env) + ] getTypedTerm :: - (Map ServerName ServerSetupVal, CryptolEnv) -> + CryptolEnv -> P.Expr P.PName -> JVMSetupM TypedTerm - getTypedTerm (_, cenv) expr = JVMSetupM $ liftIO $ - do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr + getTypedTerm cenv expr = JVMSetupM $ + do (res, warnings) <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr case res of - Right (t, _) -> return t -- TODO: Report warnings + Right (t, _) -> return t Left err -> throw $ CryptolModuleException err warnings - resolve env name = - case Map.lookup name env of - Just v -> return v - Nothing -> error "Server value not found - impossible!" -- rule out elsewhere + getSetupVal :: + (Map ServerName ServerSetupVal, CryptolEnv) -> + CrucibleSetupVal (P.Expr P.PName) -> + JVMSetupM (MS.SetupValue CJ.JVM) + getSetupVal _ NullValue = JVMSetupM $ return (MS.SetupNull ()) + getSetupVal (env, _) (NamedValue n) = + resolve env n >>= \case Val x -> return x + getSetupVal (_, cenv) (CryptolExpr expr) = + MS.SetupTerm <$> getTypedTerm cenv expr + getSetupVal _ (ArrayValue _) = + JVMSetupM $ fail "Array setup values unsupported in JVM API." + getSetupVal _ (TupleValue _) = + JVMSetupM $ fail "Tuple setup values unsupported in JVM API." + getSetupVal _ (FieldLValue _ _) = + JVMSetupM $ fail "Field l-values unsupported in JVM API." + getSetupVal _ (ElementLValue _ _) = + JVMSetupM $ fail "Element l-values unsupported in JVM API." + getSetupVal _ (GlobalInitializer _) = + JVMSetupM $ fail "Global initializers unsupported in JVM API." + getSetupVal _ (GlobalLValue _) = + JVMSetupM $ fail "Global l-values unsupported in JVM API." data JVMLoadClassParams = JVMLoadClassParams ServerName String From 79cb2f62c5025aa53e810a23b9040504e8a32b54 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 6 Jul 2021 14:07:35 -0700 Subject: [PATCH 02/10] Refactor LLVM Python libraries to prepare for JVM --- saw-remote-api/python/saw_client/crucible.py | 627 ++++++++++++++++ saw-remote-api/python/saw_client/jvm_type.py | 55 ++ saw-remote-api/python/saw_client/llvm.py | 669 +----------------- saw-remote-api/python/saw_client/llvm_type.py | 54 ++ 4 files changed, 738 insertions(+), 667 deletions(-) create mode 100644 saw-remote-api/python/saw_client/crucible.py create mode 100644 saw-remote-api/python/saw_client/jvm_type.py create mode 100644 saw-remote-api/python/saw_client/llvm_type.py diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py new file mode 100644 index 0000000000..abe98b7ce5 --- /dev/null +++ b/saw-remote-api/python/saw_client/crucible.py @@ -0,0 +1,627 @@ +from abc import ABCMeta, abstractmethod +from cryptol import cryptoltypes +from .utils import deprecated +from dataclasses import dataclass +import dataclasses +import re +from typing import Any, Dict, List, Optional, Set, Union, overload +from typing_extensions import Literal +import inspect +import uuid + +from .llvm_type import * +from .jvm_type import * + +class SetupVal(metaclass=ABCMeta): + """Represent a ``SetupValue`` in SawScript, which "corresponds to + values that can occur during symbolic execution, which includes both 'Term' + values, pointers, and composite types consisting of either of these + (both structures and arrays)." + """ + @abstractmethod + def to_json(self) -> Any: + """JSON representation for this ``SetupVal`` (i.e., how it is represented in expressions, etc). + + N.B., should be a JSON object with a ``'setup value'`` field with a unique tag which the + server will dispatch on to then interpret the rest of the JSON object.``""" + pass + + @overload + def __getitem__(self, key : int) -> 'ElemVal': + pass + @overload + def __getitem__(self, key : str) -> 'FieldVal': + pass + def __getitem__(self, key : Union[int,str]) -> 'SetupVal': + """``SetupVal`` element indexing and field access. + :param key: If ``key`` is an integer, a ``SetupVal`` corresponding to accessing the element + at that index is returned. If ``key`` is a string, a ``SetupVal`` corresponding + to accessing a field with that name is returned. + """ + if isinstance(key, int): + return elem(self, key) + elif isinstance(key, str): + return field(self, key) + else: + raise ValueError(f'{key!r} is not a valid element index or field name.') + + +class NamedSetupVal(SetupVal): + """Represents those ``SetupVal``s which are a named reference to some value, e.e., a variable + or reference to allocated memory.""" + @abstractmethod + def to_init_json(self) -> Any: + """JSON representation with the information for those ``SetupVal``s which require additional + information to initialize/allocate them vs that which is required later to reference them. + + I.e., ``.to_json()`` will be used to refer to such ``SetupVal``s in expressions, and + ``.to_init_json() is used to initialize/allocate them.`` + """ + pass + +class CryptolTerm(SetupVal): + expression : cryptoltypes.CryptolJSON + + def __init__(self, code : Union[str, cryptoltypes.CryptolJSON]): + if isinstance(code, str): + self.expression = cryptoltypes.CryptolLiteral(code) + else: + self.expression = code + + def __call__(self, *args : cryptoltypes.CryptolJSON) -> 'CryptolTerm': + out_term = self.expression + for a in args: + out_term = cryptoltypes.CryptolApplication(out_term, a) + + return CryptolTerm(out_term) + + def __repr__(self) -> str: + return f"CryptolTerm({self.expression!r})" + + def to_json(self) -> Any: + return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)} + + def __to_cryptol__(self, ty : Any) -> Any: + return self.expression.__to_cryptol__(ty) + +class FreshVar(NamedSetupVal): + __name : Optional[str] + + def __init__(self, spec : 'Contract', type : 'LLVMType', suggested_name : Optional[str] = None) -> None: + self.__name = suggested_name + self.spec = spec + self.type = type + + def __to_cryptol__(self, ty : Any) -> Any: + return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty) + + def to_init_json(self) -> Any: + #FIXME it seems we don't actually use two names ever... just the one...do we actually need both? + name = self.name() + return {"server name": name, + "name": name, + "type": self.type.to_json()} + + def name(self) -> str: + if self.__name is None: + self.__name = self.spec.get_fresh_name() + return self.__name + + def to_json(self) -> Any: + return {'setup value': 'named', 'name': self.name()} + + def __gt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: + gt = CryptolTerm("(>)") + return gt(self, other) + + def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: + lt = CryptolTerm("(<)") + return lt(self, other) + + +class Allocated(NamedSetupVal): + name : Optional[str] + + def __init__(self, spec : 'Contract', type : 'LLVMType', *, + mutable : bool = True, alignment : Optional[int] = None) -> None: + self.name = None + self.spec = spec + self.type = type + self.mutable = mutable + self.alignment = alignment + + def to_init_json(self) -> Any: + if self.name is None: + self.name = self.spec.get_fresh_name() + return {"server name": self.name, + "type": self.type.to_json(), + "mutable": self.mutable, + "alignment": self.alignment} + + def to_json(self) -> Any: + if self.name is None: + self.name = self.spec.get_fresh_name() + return {'setup value': 'named', 'name': self.name} + +class StructVal(SetupVal): + fields : List[SetupVal] + + def __init__(self, fields : List[SetupVal]) -> None: + self.fields = fields + + def to_json(self) -> Any: + return {'setup value': 'tuple', 'elements': [fld.to_json() for fld in self.fields]} + +class ElemVal(SetupVal): + base : SetupVal + index : int + + def __init__(self, base : SetupVal, index : int) -> None: + self.base = base + self.index = index + + def to_json(self) -> Any: + return {'setup value': 'element lvalue', + 'base': self.base.to_json(), 'index': self.index} + +class FieldVal(SetupVal): + base : SetupVal + field_name : str + + def __init__(self, base : SetupVal, field_name : str) -> None: + self.base = base + self.field_name = field_name + + def to_json(self) -> Any: + return {'setup value': 'field', + 'base': self.base.to_json(), 'field': self.field_name} + +class GlobalInitializerVal(SetupVal): + name : str + + def __init__(self, name : str) -> None: + self.name = name + + def to_json(self) -> Any: + return {'setup value': 'global initializer', 'name': self.name} + +class GlobalVarVal(SetupVal): + name : str + + def __init__(self, name : str) -> None: + self.name = name + + def to_json(self) -> Any: + return {'setup value': 'global lvalue', 'name': self.name} + +class NullVal(SetupVal): + def to_json(self) -> Any: + return {'setup value': 'null'} + +class ArrayVal(SetupVal): + elements : List[SetupVal] + + def __init__(self, elements : List[SetupVal]) -> None: + self.elements = elements + + def to_json(self) -> Any: + return {'setup value': 'array', + 'elements': [element.to_json() for element in self.elements]} + +name_regexp = re.compile('^(?P.*[^0-9])?(?P[0-9]+)?$') + +def next_name(x : str) -> str: + match = name_regexp.match(x) + if match is None: + return 'x' + prefix, number = match.group('prefix', 'number') + + if prefix is None: + prefix = 'x' + if number is None: + next_number = 0 + else: + next_number = int(number) + 1 + return f'{prefix}{next_number}' + + +def uniquify(x : str, used : Set[str]) -> str: + while x in used: + x = next_name(x) + return x + + +class PointerType: + """A trivial class indicating that PointsTo should check ``target``'s type + against the type that ``pointer``'s type points to. + """ + pass + + +class Condition: + def __init__(self, condition : CryptolTerm) -> None: + self.cryptol_term = condition + + def to_json(self) -> Any: + return cryptoltypes.to_cryptol(self.cryptol_term) + + +class PointsTo: + """The workhorse for ``points_to``. + """ + def __init__(self, pointer : SetupVal, target : SetupVal, *, + check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), + condition : Optional[Condition] = None) -> None: + self.pointer = pointer + self.target = target + self.check_target_type = check_target_type + self.condition = condition + + def to_json(self) -> Any: + check_target_type_json: Optional[Dict[str, Any]] + if self.check_target_type is None: + check_target_type_json = None + elif isinstance(self.check_target_type, PointerType): + check_target_type_json = { "check against": "pointer type" } + elif isinstance(self.check_target_type, LLVMType): + check_target_type_json = { "check against": "casted type" + , "type": self.check_target_type.to_json() } + return {"pointer": self.pointer.to_json(), + "points to": self.target.to_json(), + "check points to type": check_target_type_json, + "condition": self.condition.to_json() if self.condition is not None else self.condition} + +@dataclass +class GhostVariable: + name: str + server_name: str + +class GhostValue: + """A class containing the statement that a given ghost variable should have the + value given by a Cryptol expression. + """ + def __init__(self, name: str, value: CryptolTerm) -> None: + self.name = name + self.value = value + + def to_json(self) -> Any: + return {"server name": self.name, + "value": cryptoltypes.to_cryptol(self.value)} + +@dataclass +class State: + contract : 'Contract' + fresh : List[FreshVar] = dataclasses.field(default_factory=list) + conditions : List[Condition] = dataclasses.field(default_factory=list) + allocated : List[Allocated] = dataclasses.field(default_factory=list) + points_to : List[PointsTo] = dataclasses.field(default_factory=list) + ghost_values : List[GhostValue] = dataclasses.field(default_factory=list) + + def to_json(self) -> Any: + return {'variables': [v.to_init_json() for v in self.fresh], + 'conditions': [c.to_json() for c in self.conditions], + 'allocated': [a.to_init_json() for a in self.allocated], + 'points to': [p.to_json() for p in self.points_to], + 'ghost values': [g.to_json() for g in self.ghost_values] + } + +ContractState = \ + Union[Literal['pre'], + Literal['post'], + Literal['done']] + +@dataclass +class Void: + def to_json(self) -> Any: + return None + +void = Void() + +@dataclass +class VerifyResult: + contract : 'Contract' + lemma_name : str + +# Lemma names are generated deterministically with respect to a +# particular Python execution trace. This means that re-running the +# same script will be fast when using caching, but REPL-style usage +# will be slow, invalidating the cache at each step. We should be +# smarter about this. +used_lemma_names = set([]) # type: Set[str] + +class Contract: + __used_names : Set[str] + + __state : ContractState = 'pre' + + __pre_state : State + __post_state : State + + __returns : Optional[Union[SetupVal, Void]] + + __arguments : Optional[List[SetupVal]] + + __definition_lineno : Optional[int] + __definition_filename : Optional[str] + __unique_id : uuid.UUID + __cached_json : Optional[Any] + + def __init__(self) -> None: + self.__pre_state = State(self) + self.__post_state = State(self) + self.__used_names = set() + self.__arguments = None + self.__returns = None + self.__unique_id = uuid.uuid4() + self.__cached_json = None + frame = inspect.currentframe() + if frame is not None and frame.f_back is not None: + self.__definition_lineno = frame.f_back.f_lineno + self.__definition_filename = frame.f_back.f_code.co_filename + else: + self.__definition_lineno = None + self.__definition_filename = None + + # To be overridden by users + def specification(self) -> None: + pass + + def execute_func(self, *args : SetupVal) -> None: + """Denotes the end of the precondition specification portion of this ``Contract``, records that + the function is executed with arguments ``args``, and denotes the beginning of the postcondition + portion of this ``Contract``.""" + if self.__arguments is not None: + raise ValueError("The function has already been called once during the specification.") + elif self.__state != 'pre': + raise ValueError("Contract state expected to be 'pre', but found {self.__state!r} (has `execute_func` already been called for this contract?).") + else: + self.__arguments = [arg for arg in args] + self.__state = 'post' + + def get_fresh_name(self, hint : str = 'x') -> str: + new_name = uniquify(hint, self.__used_names) + self.__used_names.add(new_name) + return new_name + + def fresh_var(self, type : 'LLVMType', suggested_name : Optional[str] = None) -> FreshVar: + """Declares a fresh variable of type ``type`` (with name ``suggested_name`` if provided and available).""" + fresh_name = self.get_fresh_name('x' if suggested_name is None else self.get_fresh_name(suggested_name)) + v = FreshVar(self, type, fresh_name) + if self.__state == 'pre': + self.__pre_state.fresh.append(v) + elif self.__state == 'post': + self.__post_state.fresh.append(v) + else: + raise Exception("wrong state") + return v + + def alloc(self, type : 'LLVMType', *, read_only : bool = False, + alignment : Optional[int] = None, + points_to : Optional[SetupVal] = None) -> SetupVal: + """Allocates a pointer of type ``type``. + + If ``read_only == True`` then the allocated memory is immutable. + + If ``alignment != None``, then the start of the allocated region of + memory will be aligned to a multiple of the specified number of bytes + (which must be a power of 2). + + If ``points_to != None``, it will also be asserted that the allocated memory contains the + value specified by ``points_to``. + + :returns A pointer of the proper type to the allocated region.""" + a = Allocated(self, type, mutable = not read_only, alignment = alignment) + if self.__state == 'pre': + self.__pre_state.allocated.append(a) + elif self.__state == 'post': + self.__post_state.allocated.append(a) + else: + raise Exception("wrong state") + + if points_to is not None: + self.points_to(a, points_to) + + return a + + def points_to(self, pointer : SetupVal, target : SetupVal, *, + check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), + condition : Optional[Condition] = None) -> None: + """Declare that the memory location indicated by the ``pointer`` + contains the ``target``. + + If ``check_target_type == PointerType()``, then this will check that + ``target``'s type matches the type that ``pointer``'s type points to. + If ``check_target_type`` is an ``LLVMType``, then this will check that + ``target``'s type matches that type. + If ``check_target_type == None`, then this will not check ``target``'s + type at all. + + If ``condition != None`, then this will only declare that ``pointer`` + points to ``target`` is the ``condition`` holds. + """ + pt = PointsTo(pointer, target, check_target_type = check_target_type, condition = condition) + if self.__state == 'pre': + self.__pre_state.points_to.append(pt) + elif self.__state == 'post': + self.__post_state.points_to.append(pt) + else: + raise Exception("wrong state") + + def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None: + """Declare that the given ghost variable should have a value specified by the given Cryptol expression. + + Usable either before or after `execute_func`. + """ + gv = GhostValue(var.name, value) + if self.__state == 'pre': + self.__pre_state.ghost_values.append(gv) + elif self.__state == 'post': + self.__post_state.ghost_values.append(gv) + else: + raise Exception("wrong state") + + @deprecated + def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: + """DEPRECATED: Use ``precondition`` or ``postcondition`` instead. This method will + eventually be removed.""" + if not isinstance(proposition, CryptolTerm): + condition = Condition(CryptolTerm(proposition)) + else: + condition = Condition(proposition) + if self.__state == 'pre': + self.__pre_state.conditions.append(condition) + elif self.__state == 'post': + self.__post_state.conditions.append(condition) + else: + raise Exception("wrong state") + + def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: + """Establishes ``proposition`` as a precondition for the function ```Contract``` + being specified. + + Preconditions must be specified before ``execute_func`` is called in the contract specification.""" + if not isinstance(proposition, CryptolTerm): + condition = Condition(CryptolTerm(proposition)) + else: + condition = Condition(proposition) + if self.__state == 'pre': + self.__pre_state.conditions.append(condition) + else: + raise Exception("preconditions must be specified before execute_func is called in the contract") + + def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: + """Establishes ``proposition`` as a postcondition for the function ```Contract``` + being specified. + + Postconditions must be specified after ``execute_func`` is called in the contract specification.""" + if not isinstance(proposition, CryptolTerm): + condition = Condition(CryptolTerm(proposition)) + else: + condition = Condition(proposition) + if self.__state == 'post': + self.__post_state.conditions.append(condition) + else: + raise Exception("postconditions must be specified after execute_func is called in the contract") + + def returns(self, val : Union[Void,SetupVal]) -> None: + if self.__state == 'post': + if self.__returns is None: + self.__returns = val + else: + raise ValueError("Return value already specified") + else: + raise ValueError("Not in postcondition") + + def lemma_name(self, hint : Optional[str] = None) -> str: + if hint is None: + hint = self.__class__.__name__ + + name = uniquify('lemma_' + hint, used_lemma_names) + + used_lemma_names.add(name) + + return name + + def definition_lineno(self) -> Optional[int]: + return self.__definition_lineno + + def definition_filename(self) -> Optional[str]: + return self.__definition_filename + + def to_json(self) -> Any: + if self.__cached_json is not None: + return self.__cached_json + else: + if self.__state != 'pre': + raise Exception(f'Internal error: wrong contract state -- expected \'pre\', but got: {self.__state!r}') + + self.specification() + + if self.__state != 'post': + raise Exception(f'Internal error: wrong contract state -- expected \'post\', but got: {self.__state!r}') + + self.__state = 'done' + + if self.__returns is None: + raise Exception("forgot return") + + self.__cached_json = \ + {'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], + 'pre conds': [c.to_json() for c in self.__pre_state.conditions], + 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], + 'pre ghost values': [g.to_json() for g in self.__pre_state.ghost_values], + 'pre points tos': [pt.to_json() for pt in self.__pre_state.points_to], + 'argument vals': [a.to_json() for a in self.__arguments] if self.__arguments is not None else [], + 'post vars': [v.to_init_json() for v in self.__post_state.fresh], + 'post conds': [c.to_json() for c in self.__post_state.conditions], + 'post allocated': [a.to_init_json() for a in self.__post_state.allocated], + 'post ghost values': [g.to_json() for g in self.__post_state.ghost_values], + 'post points tos': [pt.to_json() for pt in self.__post_state.points_to], + 'return val': self.__returns.to_json()} + + return self.__cached_json + +################################################## +# Helpers for value construction +################################################## + +# It's tempting to name this `global` to mirror SAWScript's `llvm_global`, +# but that would clash with the Python keyword `global`. +def global_var(name: str) -> SetupVal: + """Returns a pointer to the named global ``name`` (i.e., a ``GlobalVarVal``).""" + return GlobalVarVal(name) + +# FIXME Is `Any` too permissive here -- can we be a little more precise? +def cryptol(data : Any) -> 'CryptolTerm': + """Constructs a Cryptol value from ``data`` (i.e., a ``CryptolTerm``, which is also a ``SetupVal``). + + ``data`` should be a string literal representing Cryptol syntax or the result of a Cryptol-realted server computation.""" + return CryptolTerm(data) + +def array(*elements: SetupVal) -> SetupVal: + """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``). + + N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out. + if len(elements) == 0: + raise ValueError('An array must be constructed with one or more elements') + for e in elements: + if not isinstance(e, SetupVal): + raise ValueError('array expected a SetupVal, but got {e!r}') + return ArrayVal(list(elements)) + +def elem(base: SetupVal, index: int) -> SetupVal: + """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``). + + Can also be created by using an ``int`` indexing key on a ``SetupVal``: ``base[index]``.""" + if not isinstance(base, SetupVal): + raise ValueError('elem expected a SetupVal, but got {base!r}') + if not isinstance(index, int): + raise ValueError('elem expected an int, but got {index!r}') + return ElemVal(base, index) + +def field(base : SetupVal, field_name : str) -> SetupVal: + """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``). + + Can also be created by using a ``str`` indexing key on a ``SetupVal``: ``base[field_name]``.""" + if not isinstance(base, SetupVal): + raise ValueError('field expected a SetupVal, but got {base!r}') + if not isinstance(field_name, str): + raise ValueError('field expected a str, but got {field_name!r}') + return FieldVal(base, field_name) + +def global_initializer(name: str) -> SetupVal: + """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``).""" + if not isinstance(name, str): + raise ValueError('global_initializer expected a str naming a global value, but got {name!r}') + return GlobalInitializerVal(name) + +def null() -> SetupVal: + """Returns a null pointer value (i.e., a ``NullVal``).""" + return NullVal() + +def struct(*fields : SetupVal) -> SetupVal: + """Returns an LLVM structure value with the given ``fields`` (i.e., a ``StructVal``).""" + for field in fields: + if not isinstance(field, SetupVal): + raise ValueError('struct expected a SetupVal, but got {field!r}') + return StructVal(list(fields)) diff --git a/saw-remote-api/python/saw_client/jvm_type.py b/saw-remote-api/python/saw_client/jvm_type.py new file mode 100644 index 0000000000..ba941f3c00 --- /dev/null +++ b/saw-remote-api/python/saw_client/jvm_type.py @@ -0,0 +1,55 @@ +from abc import ABCMeta, abstractmethod +from typing import Any, Dict, List, Optional, Set, Union, overload + +class JVMType(metaclass=ABCMeta): + @abstractmethod + def to_json(self) -> Any: pass + +class JVMPrimType(JVMType): + def __init__(self, prim: str): + self.prim = prim + + def to_json(self) -> Any: + return {'type': 'primitive type', 'primitive': self.prim} + +class JVMBooleanType(JVMPrimType): + def __init__(self): super().__init__('boolean') + +class JVMByteType(JVMPrimType): + def __init__(self): super().__init__('byte') + +class JVMCharType(JVMPrimType): + def __init__(self): super().__init__('char') + +class JVMDoubleType(JVMPrimType): + def __init__(self): super().__init__('double') + +class JVMFloatType(JVMPrimType): + def __init__(self): super().__init__('float') + +class JVMIntType(JVMPrimType): + def __init__(self): super().__init__('int') + +class JVMLongType(JVMPrimType): + def __init__(self): super().__init__('long') + +class JVMShortType(JVMPrimType): + def __init__(self): super().__init__('short') + +class JVMArrayType(JVMType): + def __init__(self, elemtype : 'JVMType', size : int) -> None: + self.size = size + self.elemtype = elemtype + + def to_json(self) -> Any: + return { 'type': 'array type', + 'element type': self.elemtype.to_json(), + 'size': self.size } + +class JVMClassType(JVMType): + def __init__(self, name: str) -> None: + self.name = name + + def to_json(self) -> Any: + return { 'type': 'class type', + 'class name': self.name } diff --git a/saw-remote-api/python/saw_client/llvm.py b/saw-remote-api/python/saw_client/llvm.py index 725e72268d..861f96f226 100644 --- a/saw-remote-api/python/saw_client/llvm.py +++ b/saw-remote-api/python/saw_client/llvm.py @@ -9,674 +9,9 @@ import inspect import uuid -class SetupVal(metaclass=ABCMeta): - """Represent a ``SetupValue`` in SawScript, which "corresponds to - values that can occur during symbolic execution, which includes both 'Term' - values, pointers, and composite types consisting of either of these - (both structures and arrays)." - """ - @abstractmethod - def to_json(self) -> Any: - """JSON representation for this ``SetupVal`` (i.e., how it is represented in expressions, etc). - - N.B., should be a JSON object with a ``'setup value'`` field with a unique tag which the - server will dispatch on to then interpret the rest of the JSON object.``""" - pass - - @overload - def __getitem__(self, key : int) -> 'ElemVal': - pass - @overload - def __getitem__(self, key : str) -> 'FieldVal': - pass - def __getitem__(self, key : Union[int,str]) -> 'SetupVal': - """``SetupVal`` element indexing and field access. - :param key: If ``key`` is an integer, a ``SetupVal`` corresponding to accessing the element - at that index is returned. If ``key`` is a string, a ``SetupVal`` corresponding - to accessing a field with that name is returned. - """ - if isinstance(key, int): - return elem(self, key) - elif isinstance(key, str): - return field(self, key) - else: - raise ValueError(f'{key!r} is not a valid element index or field name.') - - -class NamedSetupVal(SetupVal): - """Represents those ``SetupVal``s which are a named reference to some value, e.e., a variable - or reference to allocated memory.""" - @abstractmethod - def to_init_json(self) -> Any: - """JSON representation with the information for those ``SetupVal``s which require additional - information to initialize/allocate them vs that which is required later to reference them. - - I.e., ``.to_json()`` will be used to refer to such ``SetupVal``s in expressions, and - ``.to_init_json() is used to initialize/allocate them.`` - """ - pass - -class CryptolTerm(SetupVal): - expression : cryptoltypes.CryptolJSON - - def __init__(self, code : Union[str, cryptoltypes.CryptolJSON]): - if isinstance(code, str): - self.expression = cryptoltypes.CryptolLiteral(code) - else: - self.expression = code - - def __call__(self, *args : cryptoltypes.CryptolJSON) -> 'CryptolTerm': - out_term = self.expression - for a in args: - out_term = cryptoltypes.CryptolApplication(out_term, a) - - return CryptolTerm(out_term) - - def __repr__(self) -> str: - return f"CryptolTerm({self.expression!r})" - - def to_json(self) -> Any: - return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)} - - def __to_cryptol__(self, ty : Any) -> Any: - return self.expression.__to_cryptol__(ty) - -class FreshVar(NamedSetupVal): - __name : Optional[str] - - def __init__(self, spec : 'Contract', type : 'LLVMType', suggested_name : Optional[str] = None) -> None: - self.__name = suggested_name - self.spec = spec - self.type = type - - def __to_cryptol__(self, ty : Any) -> Any: - return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty) - - def to_init_json(self) -> Any: - #FIXME it seems we don't actually use two names ever... just the one...do we actually need both? - name = self.name() - return {"server name": name, - "name": name, - "type": self.type.to_json()} - - def name(self) -> str: - if self.__name is None: - self.__name = self.spec.get_fresh_name() - return self.__name - - def to_json(self) -> Any: - return {'setup value': 'named', 'name': self.name()} - - def __gt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: - gt = CryptolTerm("(>)") - return gt(self, other) - - def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: - lt = CryptolTerm("(<)") - return lt(self, other) - - -class Allocated(NamedSetupVal): - name : Optional[str] - - def __init__(self, spec : 'Contract', type : 'LLVMType', *, - mutable : bool = True, alignment : Optional[int] = None) -> None: - self.name = None - self.spec = spec - self.type = type - self.mutable = mutable - self.alignment = alignment - - def to_init_json(self) -> Any: - if self.name is None: - self.name = self.spec.get_fresh_name() - return {"server name": self.name, - "type": self.type.to_json(), - "mutable": self.mutable, - "alignment": self.alignment} - - def to_json(self) -> Any: - if self.name is None: - self.name = self.spec.get_fresh_name() - return {'setup value': 'named', 'name': self.name} - -class StructVal(SetupVal): - fields : List[SetupVal] - - def __init__(self, fields : List[SetupVal]) -> None: - self.fields = fields - - def to_json(self) -> Any: - return {'setup value': 'tuple', 'elements': [fld.to_json() for fld in self.fields]} - -class ElemVal(SetupVal): - base : SetupVal - index : int - - def __init__(self, base : SetupVal, index : int) -> None: - self.base = base - self.index = index - - def to_json(self) -> Any: - return {'setup value': 'element lvalue', - 'base': self.base.to_json(), 'index': self.index} - -class FieldVal(SetupVal): - base : SetupVal - field_name : str - - def __init__(self, base : SetupVal, field_name : str) -> None: - self.base = base - self.field_name = field_name - - def to_json(self) -> Any: - return {'setup value': 'field', - 'base': self.base.to_json(), 'field': self.field_name} - -class GlobalInitializerVal(SetupVal): - name : str - - def __init__(self, name : str) -> None: - self.name = name - - def to_json(self) -> Any: - return {'setup value': 'global initializer', 'name': self.name} - -class GlobalVarVal(SetupVal): - name : str - - def __init__(self, name : str) -> None: - self.name = name - - def to_json(self) -> Any: - return {'setup value': 'global lvalue', 'name': self.name} - -class NullVal(SetupVal): - def to_json(self) -> Any: - return {'setup value': 'null'} - -class ArrayVal(SetupVal): - elements : List[SetupVal] - - def __init__(self, elements : List[SetupVal]) -> None: - self.elements = elements - - def to_json(self) -> Any: - return {'setup value': 'array', - 'elements': [element.to_json() for element in self.elements]} - -name_regexp = re.compile('^(?P.*[^0-9])?(?P[0-9]+)?$') - -def next_name(x : str) -> str: - match = name_regexp.match(x) - if match is None: - return 'x' - prefix, number = match.group('prefix', 'number') - - if prefix is None: - prefix = 'x' - if number is None: - next_number = 0 - else: - next_number = int(number) + 1 - return f'{prefix}{next_number}' - - -def uniquify(x : str, used : Set[str]) -> str: - while x in used: - x = next_name(x) - return x - - -class PointerType: - """A trivial class indicating that PointsTo should check ``target``'s type - against the type that ``pointer``'s type points to. - """ - pass - - -class Condition: - def __init__(self, condition : CryptolTerm) -> None: - self.cryptol_term = condition - - def to_json(self) -> Any: - return cryptoltypes.to_cryptol(self.cryptol_term) - - -class PointsTo: - """The workhorse for ``points_to``. - """ - def __init__(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), - condition : Optional[Condition] = None) -> None: - self.pointer = pointer - self.target = target - self.check_target_type = check_target_type - self.condition = condition - - def to_json(self) -> Any: - check_target_type_json: Optional[Dict[str, Any]] - if self.check_target_type is None: - check_target_type_json = None - elif isinstance(self.check_target_type, PointerType): - check_target_type_json = { "check against": "pointer type" } - elif isinstance(self.check_target_type, LLVMType): - check_target_type_json = { "check against": "casted type" - , "type": self.check_target_type.to_json() } - return {"pointer": self.pointer.to_json(), - "points to": self.target.to_json(), - "check points to type": check_target_type_json, - "condition": self.condition.to_json() if self.condition is not None else self.condition} - -@dataclass -class GhostVariable: - name: str - server_name: str - -class GhostValue: - """A class containing the statement that a given ghost variable should have the - value given by a Cryptol expression. - """ - def __init__(self, name: str, value: CryptolTerm) -> None: - self.name = name - self.value = value - - def to_json(self) -> Any: - return {"server name": self.name, - "value": cryptoltypes.to_cryptol(self.value)} - -@dataclass -class State: - contract : 'Contract' - fresh : List[FreshVar] = dataclasses.field(default_factory=list) - conditions : List[Condition] = dataclasses.field(default_factory=list) - allocated : List[Allocated] = dataclasses.field(default_factory=list) - points_to : List[PointsTo] = dataclasses.field(default_factory=list) - ghost_values : List[GhostValue] = dataclasses.field(default_factory=list) - - def to_json(self) -> Any: - return {'variables': [v.to_init_json() for v in self.fresh], - 'conditions': [c.to_json() for c in self.conditions], - 'allocated': [a.to_init_json() for a in self.allocated], - 'points to': [p.to_json() for p in self.points_to], - 'ghost values': [g.to_json() for g in self.ghost_values] - } - -ContractState = \ - Union[Literal['pre'], - Literal['post'], - Literal['done']] - -@dataclass -class Void: - def to_json(self) -> Any: - return None - -void = Void() - -@dataclass -class VerifyResult: - contract : 'Contract' - lemma_name : str - -# Lemma names are generated deterministically with respect to a -# particular Python execution trace. This means that re-running the -# same script will be fast when using caching, but REPL-style usage -# will be slow, invalidating the cache at each step. We should be -# smarter about this. -used_lemma_names = set([]) # type: Set[str] - -class Contract: - __used_names : Set[str] - - __state : ContractState = 'pre' - - __pre_state : State - __post_state : State - - __returns : Optional[Union[SetupVal, Void]] - - __arguments : Optional[List[SetupVal]] - - __definition_lineno : Optional[int] - __definition_filename : Optional[str] - __unique_id : uuid.UUID - __cached_json : Optional[Any] - - def __init__(self) -> None: - self.__pre_state = State(self) - self.__post_state = State(self) - self.__used_names = set() - self.__arguments = None - self.__returns = None - self.__unique_id = uuid.uuid4() - self.__cached_json = None - frame = inspect.currentframe() - if frame is not None and frame.f_back is not None: - self.__definition_lineno = frame.f_back.f_lineno - self.__definition_filename = frame.f_back.f_code.co_filename - else: - self.__definition_lineno = None - self.__definition_filename = None - - # To be overridden by users - def specification(self) -> None: - pass - - def execute_func(self, *args : SetupVal) -> None: - """Denotes the end of the precondition specification portion of this ``Contract``, records that - the function is executed with arguments ``args``, and denotes the beginning of the postcondition - portion of this ``Contract``.""" - if self.__arguments is not None: - raise ValueError("The function has already been called once during the specification.") - elif self.__state != 'pre': - raise ValueError("Contract state expected to be 'pre', but found {self.__state!r} (has `execute_func` already been called for this contract?).") - else: - self.__arguments = [arg for arg in args] - self.__state = 'post' - - def get_fresh_name(self, hint : str = 'x') -> str: - new_name = uniquify(hint, self.__used_names) - self.__used_names.add(new_name) - return new_name - - def fresh_var(self, type : 'LLVMType', suggested_name : Optional[str] = None) -> FreshVar: - """Declares a fresh variable of type ``type`` (with name ``suggested_name`` if provided and available).""" - fresh_name = self.get_fresh_name('x' if suggested_name is None else self.get_fresh_name(suggested_name)) - v = FreshVar(self, type, fresh_name) - if self.__state == 'pre': - self.__pre_state.fresh.append(v) - elif self.__state == 'post': - self.__post_state.fresh.append(v) - else: - raise Exception("wrong state") - return v - - def alloc(self, type : 'LLVMType', *, read_only : bool = False, - alignment : Optional[int] = None, - points_to : Optional[SetupVal] = None) -> SetupVal: - """Allocates a pointer of type ``type``. - - If ``read_only == True`` then the allocated memory is immutable. - - If ``alignment != None``, then the start of the allocated region of - memory will be aligned to a multiple of the specified number of bytes - (which must be a power of 2). - - If ``points_to != None``, it will also be asserted that the allocated memory contains the - value specified by ``points_to``. - - :returns A pointer of the proper type to the allocated region.""" - a = Allocated(self, type, mutable = not read_only, alignment = alignment) - if self.__state == 'pre': - self.__pre_state.allocated.append(a) - elif self.__state == 'post': - self.__post_state.allocated.append(a) - else: - raise Exception("wrong state") - - if points_to is not None: - self.points_to(a, points_to) - - return a - - def points_to(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), - condition : Optional[Condition] = None) -> None: - """Declare that the memory location indicated by the ``pointer`` - contains the ``target``. - - If ``check_target_type == PointerType()``, then this will check that - ``target``'s type matches the type that ``pointer``'s type points to. - If ``check_target_type`` is an ``LLVMType``, then this will check that - ``target``'s type matches that type. - If ``check_target_type == None`, then this will not check ``target``'s - type at all. - - If ``condition != None`, then this will only declare that ``pointer`` - points to ``target`` is the ``condition`` holds. - """ - pt = PointsTo(pointer, target, check_target_type = check_target_type, condition = condition) - if self.__state == 'pre': - self.__pre_state.points_to.append(pt) - elif self.__state == 'post': - self.__post_state.points_to.append(pt) - else: - raise Exception("wrong state") - - def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None: - """Declare that the given ghost variable should have a value specified by the given Cryptol expression. - - Usable either before or after `execute_func`. - """ - gv = GhostValue(var.name, value) - if self.__state == 'pre': - self.__pre_state.ghost_values.append(gv) - elif self.__state == 'post': - self.__post_state.ghost_values.append(gv) - else: - raise Exception("wrong state") - - @deprecated - def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: - """DEPRECATED: Use ``precondition`` or ``postcondition`` instead. This method will - eventually be removed.""" - if not isinstance(proposition, CryptolTerm): - condition = Condition(CryptolTerm(proposition)) - else: - condition = Condition(proposition) - if self.__state == 'pre': - self.__pre_state.conditions.append(condition) - elif self.__state == 'post': - self.__post_state.conditions.append(condition) - else: - raise Exception("wrong state") - - def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: - """Establishes ``proposition`` as a precondition for the function ```Contract``` - being specified. - - Preconditions must be specified before ``execute_func`` is called in the contract specification.""" - if not isinstance(proposition, CryptolTerm): - condition = Condition(CryptolTerm(proposition)) - else: - condition = Condition(proposition) - if self.__state == 'pre': - self.__pre_state.conditions.append(condition) - else: - raise Exception("preconditions must be specified before execute_func is called in the contract") - - def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: - """Establishes ``proposition`` as a postcondition for the function ```Contract``` - being specified. - - Postconditions must be specified after ``execute_func`` is called in the contract specification.""" - if not isinstance(proposition, CryptolTerm): - condition = Condition(CryptolTerm(proposition)) - else: - condition = Condition(proposition) - if self.__state == 'post': - self.__post_state.conditions.append(condition) - else: - raise Exception("postconditions must be specified after execute_func is called in the contract") - - def returns(self, val : Union[Void,SetupVal]) -> None: - if self.__state == 'post': - if self.__returns is None: - self.__returns = val - else: - raise ValueError("Return value already specified") - else: - raise ValueError("Not in postcondition") - - def lemma_name(self, hint : Optional[str] = None) -> str: - if hint is None: - hint = self.__class__.__name__ - - name = uniquify('lemma_' + hint, used_lemma_names) - - used_lemma_names.add(name) - - return name - - def definition_lineno(self) -> Optional[int]: - return self.__definition_lineno - - def definition_filename(self) -> Optional[str]: - return self.__definition_filename - - def to_json(self) -> Any: - if self.__cached_json is not None: - return self.__cached_json - else: - if self.__state != 'pre': - raise Exception(f'Internal error: wrong contract state -- expected \'pre\', but got: {self.__state!r}') - - self.specification() - - if self.__state != 'post': - raise Exception(f'Internal error: wrong contract state -- expected \'post\', but got: {self.__state!r}') - - self.__state = 'done' - - if self.__returns is None: - raise Exception("forgot return") - - self.__cached_json = \ - {'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], - 'pre conds': [c.to_json() for c in self.__pre_state.conditions], - 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], - 'pre ghost values': [g.to_json() for g in self.__pre_state.ghost_values], - 'pre points tos': [pt.to_json() for pt in self.__pre_state.points_to], - 'argument vals': [a.to_json() for a in self.__arguments] if self.__arguments is not None else [], - 'post vars': [v.to_init_json() for v in self.__post_state.fresh], - 'post conds': [c.to_json() for c in self.__post_state.conditions], - 'post allocated': [a.to_init_json() for a in self.__post_state.allocated], - 'post ghost values': [g.to_json() for g in self.__post_state.ghost_values], - 'post points tos': [pt.to_json() for pt in self.__post_state.points_to], - 'return val': self.__returns.to_json()} - - return self.__cached_json - -class LLVMType(metaclass=ABCMeta): - @abstractmethod - def to_json(self) -> Any: pass - -class LLVMIntType(LLVMType): - def __init__(self, width : int) -> None: - self.width = width - - def to_json(self) -> Any: - return {'type': 'primitive type', 'primitive': 'integer', 'size': self.width} - -class LLVMArrayType(LLVMType): - def __init__(self, elemtype : 'LLVMType', size : int) -> None: - self.size = size - self.elemtype = elemtype - - def to_json(self) -> Any: - return { 'type': 'array', - 'element type': self.elemtype.to_json(), - 'size': self.size } - -class LLVMPointerType(LLVMType): - def __init__(self, points_to : 'LLVMType') -> None: - self.points_to = points_to - - def to_json(self) -> Any: - return {'type': 'pointer', 'to type': self.points_to.to_json()} - -class LLVMAliasType(LLVMType): - def __init__(self, name : str) -> None: - self.name = name - - def to_json(self) -> Any: - return {'type': 'type alias', - 'alias of': self.name} - -class LLVMStructType(LLVMType): - def __init__(self, field_types : List[LLVMType]) -> None: - self.field_types = field_types - - def to_json(self) -> Any: - return {'type': 'struct', - 'fields': [fld_ty.to_json() for fld_ty in self.field_types]} - -class LLVMPackedStructType(LLVMType): - def __init__(self, field_types : List[LLVMType]) -> None: - self.field_types = field_types - - def to_json(self) -> Any: - return {'type': 'packed struct', - 'fields': [fld_ty.to_json() for fld_ty in self.field_types]} - - -################################################## -# Helpers for value construction -################################################## - -# It's tempting to name this `global` to mirror SAWScript's `llvm_global`, -# but that would clash with the Python keyword `global`. -def global_var(name: str) -> SetupVal: - """Returns a pointer to the named global ``name`` (i.e., a ``GlobalVarVal``).""" - return GlobalVarVal(name) - -# FIXME Is `Any` too permissive here -- can we be a little more precise? -def cryptol(data : Any) -> 'CryptolTerm': - """Constructs a Cryptol value from ``data`` (i.e., a ``CryptolTerm``, which is also a ``SetupVal``). - - ``data`` should be a string literal representing Cryptol syntax or the result of a Cryptol-realted server computation.""" - return CryptolTerm(data) - -def array(*elements: SetupVal) -> SetupVal: - """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``). - - N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out. - if len(elements) == 0: - raise ValueError('An array must be constructed with one or more elements') - for e in elements: - if not isinstance(e, SetupVal): - raise ValueError('array expected a SetupVal, but got {e!r}') - return ArrayVal(list(elements)) - -def elem(base: SetupVal, index: int) -> SetupVal: - """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``). - - Can also be created by using an ``int`` indexing key on a ``SetupVal``: ``base[index]``.""" - if not isinstance(base, SetupVal): - raise ValueError('elem expected a SetupVal, but got {base!r}') - if not isinstance(index, int): - raise ValueError('elem expected an int, but got {index!r}') - return ElemVal(base, index) - -def field(base : SetupVal, field_name : str) -> SetupVal: - """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``). - - Can also be created by using a ``str`` indexing key on a ``SetupVal``: ``base[field_name]``.""" - if not isinstance(base, SetupVal): - raise ValueError('field expected a SetupVal, but got {base!r}') - if not isinstance(field_name, str): - raise ValueError('field expected a str, but got {field_name!r}') - return FieldVal(base, field_name) - -def global_initializer(name: str) -> SetupVal: - """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``).""" - if not isinstance(name, str): - raise ValueError('global_initializer expected a str naming a global value, but got {name!r}') - return GlobalInitializerVal(name) - -def null() -> SetupVal: - """Returns a null pointer value (i.e., a ``NullVal``).""" - return NullVal() - -def struct(*fields : SetupVal) -> SetupVal: - """Returns an LLVM structure value with the given ``fields`` (i.e., a ``StructVal``).""" - for field in fields: - if not isinstance(field, SetupVal): - raise ValueError('struct expected a SetupVal, but got {field!r}') - return StructVal(list(fields)) - +from .llvm_type import * +from .crucible import * ################################################## # Helpers for type construction diff --git a/saw-remote-api/python/saw_client/llvm_type.py b/saw-remote-api/python/saw_client/llvm_type.py new file mode 100644 index 0000000000..599805314d --- /dev/null +++ b/saw-remote-api/python/saw_client/llvm_type.py @@ -0,0 +1,54 @@ +from abc import ABCMeta, abstractmethod +from typing import Any, Dict, List, Optional, Set, Union, overload + +class LLVMType(metaclass=ABCMeta): + @abstractmethod + def to_json(self) -> Any: pass + +class LLVMIntType(LLVMType): + def __init__(self, width : int) -> None: + self.width = width + + def to_json(self) -> Any: + return {'type': 'primitive type', 'primitive': 'integer', 'size': self.width} + +class LLVMArrayType(LLVMType): + def __init__(self, elemtype : 'LLVMType', size : int) -> None: + self.size = size + self.elemtype = elemtype + + def to_json(self) -> Any: + return { 'type': 'array', + 'element type': self.elemtype.to_json(), + 'size': self.size } + +class LLVMPointerType(LLVMType): + def __init__(self, points_to : 'LLVMType') -> None: + self.points_to = points_to + + def to_json(self) -> Any: + return {'type': 'pointer', 'to type': self.points_to.to_json()} + +class LLVMAliasType(LLVMType): + def __init__(self, name : str) -> None: + self.name = name + + def to_json(self) -> Any: + return {'type': 'type alias', + 'alias of': self.name} + +class LLVMStructType(LLVMType): + def __init__(self, field_types : List[LLVMType]) -> None: + self.field_types = field_types + + def to_json(self) -> Any: + return {'type': 'struct', + 'fields': [fld_ty.to_json() for fld_ty in self.field_types]} + +class LLVMPackedStructType(LLVMType): + def __init__(self, field_types : List[LLVMType]) -> None: + self.field_types = field_types + + def to_json(self) -> Any: + return {'type': 'packed struct', + 'fields': [fld_ty.to_json() for fld_ty in self.field_types]} From 916828c41bc3be6c9d5e848941fd3ec2b40024c8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 21 Jul 2021 16:30:19 -0700 Subject: [PATCH 03/10] Beginning Python client for Java verification API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Currently fails because there’s no way to set the Java CLASSPATH. --- saw-remote-api/python/saw_client/__init__.py | 126 ++++++++++++++++++ saw-remote-api/python/saw_client/commands.py | 53 ++++++++ .../python/saw_client/connection.py | 37 +++++ saw-remote-api/python/saw_client/crucible.py | 12 +- saw-remote-api/python/saw_client/jvm.py | 5 + saw-remote-api/python/saw_client/jvm_type.py | 15 +++ .../python/tests/saw/test-files/Add.class | Bin 0 -> 436 bytes .../python/tests/saw/test-files/Add.java | 9 ++ .../python/tests/saw/test_basic_java.py | 33 +++++ saw-remote-api/saw-remote-api/Main.hs | 22 ++- .../src/SAWServer/JVMCrucibleSetup.hs | 4 +- 11 files changed, 301 insertions(+), 15 deletions(-) create mode 100644 saw-remote-api/python/saw_client/jvm.py create mode 100644 saw-remote-api/python/tests/saw/test-files/Add.class create mode 100644 saw-remote-api/python/tests/saw/test-files/Add.java create mode 100644 saw-remote-api/python/tests/saw/test_basic_java.py diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index b8fe7628c2..f566703aec 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -381,6 +381,132 @@ def create_ghost_variable(name: str) -> llvm.GhostVariable: return llvm.GhostVariable(name, server_name) +@dataclass +class JVMClass: + class_name: str + server_name: str + + +def jvm_load_class(class_name: str) -> JVMClass: + name = __fresh_server_name(class_name) + __get_designated_connection().jvm_load_class(name, class_name).result() + return JVMClass(class_name, name) + +# TODO: this is almost identical to llvm_assume. Can we reduce duplication? +def jvm_assume(cls: JVMClass, + method_name: str, + contract: llvm.Contract, + lemma_name_hint: Optional[str] = None) -> VerificationResult: + """Assume that the given method satisfies the given contract. Returns an + override linking the method and contract that can be passed as an + argument in calls to `jvm_verify` + """ + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + method_name + name = __fresh_server_name(lemma_name_hint) + + result: VerificationResult + try: + conn = __get_designated_connection() + res = conn.jvm_assume(cls.class_name, + method_name, + contract.to_json(), + name) + result = AssumptionSucceeded(server_name=name, + contract=contract, + stdout=res.stdout(), + stderr=res.stderr()) + __global_success = True + # If something stopped us from even **assuming**... + except exceptions.VerificationError as err: + __global_success = False + result = AssumptionFailed(server_name=name, + assumptions=[], + contract=contract, + exception=err) + except Exception as err: + __global_success = False + for view in __designated_views: + view.on_python_exception(err) + raise err from None + + return result + +# TODO: this is almost identical to llvm_verify. Can we reduce duplication? +def jvm_verify(cls: JVMClass, + method_name: str, + contract: llvm.Contract, + lemmas: Optional[List[VerificationResult]] = None, + check_sat: bool = False, + script: Optional[proofscript.ProofScript] = None, + lemma_name_hint: Optional[str] = None) -> VerificationResult: + """Verify that the given method satisfies the given contract. Returns an + override linking the method and contract that can be passed as an + argument in further calls to `jvm_verify` + """ + + if lemmas is None: + lemmas = [] + if script is None: + script = proofscript.ProofScript([proofscript.z3([])]) + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + method_name + + name = __fresh_server_name(lemma_name_hint) + + result: VerificationResult + conn = __get_designated_connection() + + global __global_success + global __designated_views + + try: + res = conn.jvm_verify(cls.class_name, + method_name, + [l.server_name for l in lemmas], + check_sat, + contract.to_json(), + script.to_json(), + name) + + stdout = res.stdout() + stderr = res.stderr() + result = VerificationSucceeded(server_name=name, + assumptions=lemmas, + contract=contract, + stdout=stdout, + stderr=stderr) + # If the verification did not succeed... + except exceptions.VerificationError as err: + # FIXME add the goal as an assumption if it failed...? + result = VerificationFailed(server_name=name, + assumptions=lemmas, + contract=contract, + exception=err) + # If something else went wrong... + except Exception as err: + __global_success = False + for view in __designated_views: + view.on_python_exception(err) + raise err from None + + # Log or otherwise process the verification result + for view in __designated_views: + if isinstance(result, VerificationSucceeded): + view.on_success(result) + elif isinstance(result, VerificationFailed): + view.on_failure(result) + + # Note when any failure occurs + __global_success = __global_success and result.is_success() + + # Abort the proof if we failed to assume a failed verification, otherwise + # return the result of the verification + if isinstance(result, AssumptionFailed): + raise result.exception from None + + return result + @dataclass class LLVMModule: bitcode_file: str diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py index c6381186f5..89542c70c9 100644 --- a/saw-remote-api/python/saw_client/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -98,6 +98,59 @@ def __init__( def process_result(self, res : Any) -> Any: return res +class JVMLoadClass(SAWCommand): + def __init__(self, connection : argo.HasProtocolState, + name : str, + class_name : str) -> None: + super(JVMLoadClass, self).__init__( + 'SAW/JVM/load class', + {'name': name, 'class name': class_name}, + connection + ) + + def process_result(self, res : Any) -> Any: + return res + +class JVMAssume(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + module : str, + function : str, + setup : Any, + lemma_name : str) -> None: + params = {'module': module, + 'function': function, + 'contract': setup, + 'lemma name': lemma_name} + super(JVMAssume, self).__init__('SAW/JVM/assume', params, connection) + + def process_result(self, _res : Any) -> Any: + return None + +class JVMVerify(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + class_name : str, + method_name : str, + lemmas : List[str], + check_sat : bool, + setup : Any, + script : ProofScript, + lemma_name : str) -> None: + params = {'module': class_name, + 'function': method_name, + 'lemmas': lemmas, + 'check sat': check_sat, + 'contract': setup, + 'script': script, + 'lemma name': lemma_name} + super(JVMVerify, self).__init__('SAW/JVM/verify', params, connection) + + def process_result(self, res : Any) -> Any: + return res + class Prove(SAWCommand): def __init__( self, diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py index 78e8a75895..91d651110d 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -158,6 +158,43 @@ def create_ghost_variable(self, name: str, server_name: str) -> Command: self.most_recent_result = CreateGhostVariable(self, name, server_name) return self.most_recent_result + def jvm_load_class(self, name: str, class_name: str) -> Command: + """Create an instance of the `JVMLoadClass` command. Documentation on the purpose + and use of this command is associated with the top-level `jvm_load_class` + function. + """ + self.most_recent_result = JVMLoadClass(self, name, class_name) + return self.most_recent_result + + def jvm_verify(self, + class_name: str, + method_name: str, + lemmas: List[str], + check_sat: bool, + contract: Any, + script: ProofScript, + lemma_name: str) -> Command: + """Create an instance of the `JVMVerify` command. Documentation on the purpose + and use of this command is associated with the top-level `jvm_assume` + function. + """ + self.most_recent_result = \ + JVMVerify(self, class_name, method_name, lemmas, check_sat, contract, script, lemma_name) + return self.most_recent_result + + def jvm_assume(self, + class_name: str, + method_name: str, + contract: Any, + lemma_name: str) -> Command: + """Create an instance of the `JVMAssume` command. Documentation on the purpose + and use of this command is associated with the top-level `jvm_assume` + function. + """ + self.most_recent_result = \ + JVMAssume(self, class_name, method_name, contract, lemma_name) + return self.most_recent_result + def llvm_load_module(self, name: str, bitcode_file: str) -> Command: self.most_recent_result = LLVMLoadModule(self, name, bitcode_file) return self.most_recent_result diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index abe98b7ce5..f17ae1057d 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -87,7 +87,7 @@ def __to_cryptol__(self, ty : Any) -> Any: class FreshVar(NamedSetupVal): __name : Optional[str] - def __init__(self, spec : 'Contract', type : 'LLVMType', suggested_name : Optional[str] = None) -> None: + def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType'], suggested_name : Optional[str] = None) -> None: self.__name = suggested_name self.spec = spec self.type = type @@ -122,7 +122,7 @@ def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: class Allocated(NamedSetupVal): name : Optional[str] - def __init__(self, spec : 'Contract', type : 'LLVMType', *, + def __init__(self, spec : 'Contract', type : Union['LLVMType','JVMType'], *, mutable : bool = True, alignment : Optional[int] = None) -> None: self.name = None self.spec = spec @@ -250,7 +250,7 @@ class PointsTo: """The workhorse for ``points_to``. """ def __init__(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), + check_target_type : Union[PointerType, 'LLVMType', 'JVMType', None] = PointerType(), condition : Optional[Condition] = None) -> None: self.pointer = pointer self.target = target @@ -383,7 +383,7 @@ def get_fresh_name(self, hint : str = 'x') -> str: self.__used_names.add(new_name) return new_name - def fresh_var(self, type : 'LLVMType', suggested_name : Optional[str] = None) -> FreshVar: + def fresh_var(self, type : Union['LLVMType','JVMType'], suggested_name : Optional[str] = None) -> FreshVar: """Declares a fresh variable of type ``type`` (with name ``suggested_name`` if provided and available).""" fresh_name = self.get_fresh_name('x' if suggested_name is None else self.get_fresh_name(suggested_name)) v = FreshVar(self, type, fresh_name) @@ -395,7 +395,7 @@ def fresh_var(self, type : 'LLVMType', suggested_name : Optional[str] = None) -> raise Exception("wrong state") return v - def alloc(self, type : 'LLVMType', *, read_only : bool = False, + def alloc(self, type : Union['LLVMType', 'JVMType'], *, read_only : bool = False, alignment : Optional[int] = None, points_to : Optional[SetupVal] = None) -> SetupVal: """Allocates a pointer of type ``type``. @@ -424,7 +424,7 @@ def alloc(self, type : 'LLVMType', *, read_only : bool = False, return a def points_to(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', None] = PointerType(), + check_target_type : Union[PointerType, 'LLVMType', 'JVMType', None] = PointerType(), condition : Optional[Condition] = None) -> None: """Declare that the memory location indicated by the ``pointer`` contains the ``target``. diff --git a/saw-remote-api/python/saw_client/jvm.py b/saw-remote-api/python/saw_client/jvm.py new file mode 100644 index 0000000000..25851f8153 --- /dev/null +++ b/saw-remote-api/python/saw_client/jvm.py @@ -0,0 +1,5 @@ +from cryptol import cryptoltypes +from .utils import deprecated + +from .jvm_type import * +from .crucible import * diff --git a/saw-remote-api/python/saw_client/jvm_type.py b/saw-remote-api/python/saw_client/jvm_type.py index ba941f3c00..171682cdbf 100644 --- a/saw-remote-api/python/saw_client/jvm_type.py +++ b/saw-remote-api/python/saw_client/jvm_type.py @@ -53,3 +53,18 @@ def __init__(self, name: str) -> None: def to_json(self) -> Any: return { 'type': 'class type', 'class name': self.name } + +java_bool = JVMBooleanType() +java_byte = JVMByteType() +java_char = JVMCharType() +java_double = JVMDoubleType() +java_float = JVMFloatType() +java_int = JVMIntType() +java_long = JVMLongType() +java_short = JVMShortType() + +def java_array(size : int, element_type: 'JVMType'): + return JVMArrayType(element_type, size) + +def java_class(name: str): + return JVMClassType(name) diff --git a/saw-remote-api/python/tests/saw/test-files/Add.class b/saw-remote-api/python/tests/saw/test-files/Add.class new file mode 100644 index 0000000000000000000000000000000000000000..f834d518c7286dd623205a3384752c7e3fa7bcc2 GIT binary patch literal 436 zcmZ9H%}T>S6ot@&GxPQR@d@Avdp0DtZI~EX*s-uH&_2$JtU3`ez2QVap3jn0pc`gI zdbxOr((*<{Ih}qui&Z{RWv0)KDXaTzF3<{3lVnVUN)n#DAQ%P$;)zSwXLgb(C)}$W z_VsL0#_2_-xgCxkPSvAw&_dgRgEhu!3iPz?=c>5#ucB!hS2*CyC4T}|=sW~0DxXzo zXY>y7N@1YGUAMut!rfU0U}LrRcn=*te8#lKNq7JDh4t^OS7gGT1U6$N%W`; j>J9W8-k52Fd28glZ!rENtr|I4Mt+f2gA~}TpRn}<_0%*P literal 0 HcmV?d00001 diff --git a/saw-remote-api/python/tests/saw/test-files/Add.java b/saw-remote-api/python/tests/saw/test-files/Add.java new file mode 100644 index 0000000000..6dc4f499c5 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/Add.java @@ -0,0 +1,9 @@ +class Add { + public int add(int x, int y) { + return x + y; + } + + public int dbl(int x) { + return add(x, x); + } +} diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py new file mode 100644 index 0000000000..9015cba1c6 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_basic_java.py @@ -0,0 +1,33 @@ +import unittest +from pathlib import Path + +import saw_client as saw + +from saw_client.jvm import Contract, java_int, cryptol + +class Add(Contract): + def __init__(self) -> None: + super().__init__() + + def specification(self) -> None: + x = self.fresh_var(java_int, "x") + y = self.fresh_var(java_int, "y") + + self.execute_func(x, y) + + self.returns(cryptol("(+)")(x,y)) + +class SwapEasyTest(unittest.TestCase): + def test_swap(self): + saw.connect(reset_server=True) + + if __name__ == "__main__": saw.view(saw.LogResults()) + + cls = saw.jvm_load_class("Add") + + result = saw.jvm_verify(cls, 'add', Add()) + self.assertIs(result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 0b25d4b819..67454230d9 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -16,11 +16,12 @@ import SAWServer.CryptolSetup cryptolLoadModule, cryptolLoadFileDescr, cryptolLoadFile ) +import SAWServer.Data.JVMType() import SAWServer.Ghost ( createGhostVariableDescr, createGhostVariable ) ---import SAWServer.JVMCrucibleSetup ---import SAWServer.JVMVerify +import SAWServer.JVMCrucibleSetup +import SAWServer.JVMVerify import SAWServer.LLVMCrucibleSetup ( llvmLoadModuleDescr, llvmLoadModule ) import SAWServer.LLVMVerify @@ -74,11 +75,18 @@ sawMethods = saveTermDescr saveTerm -- JVM - {- - , Argo.command "SAW/JVM/load class" (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass - , Argo.command "SAW/JVM/verify" (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify - , Argo.command "SAW/JVM/assume" (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume - -} + , Argo.command + "SAW/JVM/load class" + (Doc.Paragraph [Doc.Text "TODO"]) + jvmLoadClass + , Argo.command + "SAW/JVM/verify" + (Doc.Paragraph [Doc.Text "TODO"]) + jvmVerify + , Argo.command + "SAW/JVM/assume" + (Doc.Paragraph [Doc.Text "TODO"]) + jvmAssume -- LLVM , Argo.command "SAW/LLVM/load module" diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 55e5a89d39..cd1dd7f760 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -191,7 +191,7 @@ data JVMLoadClassParams instance FromJSON JVMLoadClassParams where parseJSON = withObject "params for \"SAW/JVM/load class\"" $ \o -> - JVMLoadClassParams <$> o .: "name" <*> o .: "class" + JVMLoadClassParams <$> o .: "name" <*> o .: "class name" jvmLoadClass :: JVMLoadClassParams -> Argo.Command SAWState OK jvmLoadClass (JVMLoadClassParams serverName cname) = @@ -207,7 +207,7 @@ instance Doc.DescribedMethod JVMLoadClassParams OK where parameterFieldDescription = [ ("name", Doc.Paragraph [Doc.Text "The name of the class on the server."]) - , ("class", + , ("class name", Doc.Paragraph [Doc.Text "The java class to load."]) ] resultFieldDescription = [] From 598f151822381eac0ec38c0386b4e1437a5c65e9 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 26 Jul 2021 09:32:19 -0700 Subject: [PATCH 04/10] Update Java RPC add test to use static methods Also clean up test script --- .../python/tests/saw/test-files/Add.class | Bin 436 -> 303 bytes .../python/tests/saw/test-files/Add.java | 4 ++-- .../python/tests/saw/test_basic_java.py | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/saw-remote-api/python/tests/saw/test-files/Add.class b/saw-remote-api/python/tests/saw/test-files/Add.class index f834d518c7286dd623205a3384752c7e3fa7bcc2..32c128549dbe74ebc7ec9bd64fe79ae436bf02e1 100644 GIT binary patch delta 184 zcmZ9EOA5j;6h%*xwz08(s>_@<=(@) znoj%I`|$)0%pD06hhb_dEwkvW!W^4Mk#0iRhS=^*j*H#?v_c7xRyWi|f?^;y`<04Z laFVTbOSAxqU)1NGX~Y{+{LQs^-=~@PcXZ#ivW;Zbj6c*<5q$sv literal 436 zcmZ9H%}T>S6ot@&GxPQR@d@Avdp0DtZI~EX*s-uH&_2$JtU3`ez2QVap3jn0pc`gI zdbxOr((*<{Ih}qui&Z{RWv0)KDXaTzF3<{3lVnVUN)n#DAQ%P$;)zSwXLgb(C)}$W z_VsL0#_2_-xgCxkPSvAw&_dgRgEhu!3iPz?=c>5#ucB!hS2*CyC4T}|=sW~0DxXzo zXY>y7N@1YGUAMut!rfU0U}LrRcn=*te8#lKNq7JDh4t^OS7gGT1U6$N%W`; j>J9W8-k52Fd28glZ!rENtr|I4Mt+f2gA~}TpRn}<_0%*P diff --git a/saw-remote-api/python/tests/saw/test-files/Add.java b/saw-remote-api/python/tests/saw/test-files/Add.java index 6dc4f499c5..23eefba1e3 100644 --- a/saw-remote-api/python/tests/saw/test-files/Add.java +++ b/saw-remote-api/python/tests/saw/test-files/Add.java @@ -1,9 +1,9 @@ class Add { - public int add(int x, int y) { + public static int add(int x, int y) { return x + y; } - public int dbl(int x) { + public static int dbl(int x) { return add(x, x); } } diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py index 9015cba1c6..5fb60cac9b 100644 --- a/saw-remote-api/python/tests/saw/test_basic_java.py +++ b/saw-remote-api/python/tests/saw/test_basic_java.py @@ -17,8 +17,8 @@ def specification(self) -> None: self.returns(cryptol("(+)")(x,y)) -class SwapEasyTest(unittest.TestCase): - def test_swap(self): +class AddTest(unittest.TestCase): + def test_add(self): saw.connect(reset_server=True) if __name__ == "__main__": saw.view(saw.LogResults()) From 87da37012f40fef38065e980a8b814a6b33a59cb Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 26 Jul 2021 09:35:26 -0700 Subject: [PATCH 05/10] Add support for CLASSPATH Added to both `saw` and `saw-remote-api` --- saw-remote-api/scripts/run_rpc_tests.sh | 2 ++ saw-remote-api/src/SAWServer.hs | 10 ++++------ src/SAWScript/Options.hs | 7 +++++++ 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/saw-remote-api/scripts/run_rpc_tests.sh b/saw-remote-api/scripts/run_rpc_tests.sh index e48a2b3824..edcc35ed49 100755 --- a/saw-remote-api/scripts/run_rpc_tests.sh +++ b/saw-remote-api/scripts/run_rpc_tests.sh @@ -29,6 +29,8 @@ if [[ ! -x "$SAW_SERVER" ]]; then fi fi +export CLASSPATH=$(pwd)/tests/saw/test-files + echo "Running saw-remote-api tests..." echo "Using server $SAW_SERVER" run_test poetry run python -m unittest discover tests/saw diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index faac29ba6f..66c93c1e2d 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -49,7 +49,7 @@ import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType) import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign) import qualified SAWScript.Crucible.Common.MethodSpec as CMS (ProvedSpec, GhostGlobal) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule) -import SAWScript.Options (defaultOptions) +import SAWScript.Options (Options(..), processEnv, defaultOptions) import SAWScript.Position (Pos(..)) import SAWScript.Prover.Rewrite (basic_ss) import SAWScript.Proof (newTheoremDB) @@ -173,15 +173,13 @@ initialState readFileFn = -- warnings from the Cryptol type checker silence $ do sc <- mkSharedContext + opts <- processEnv defaultOptions CryptolSAW.scLoadPreludeModule sc CryptolSAW.scLoadCryptolModule sc let mn = mkModuleName ["SAWScript"] scLoadModule sc (emptyModule mn) ss <- basic_ss sc - let jarFiles = [] - classPaths = [] - javaBinDirs = [] - jcb <- JSS.loadCodebase jarFiles classPaths javaBinDirs + jcb <- JSS.loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts) let bic = BuiltinContext { biSharedContext = sc , biBasicSS = ss } @@ -193,7 +191,7 @@ initialState readFileFn = let ro = TopLevelRO { roSharedContext = sc , roJavaCodebase = jcb - , roOptions = defaultOptions + , roOptions = opts , roHandleAlloc = halloc , roPosition = PosInternal "SAWServer" #if USE_BUILTIN_ABC diff --git a/src/SAWScript/Options.hs b/src/SAWScript/Options.hs index 2f28e25815..ab22d815e0 100644 --- a/src/SAWScript/Options.hs +++ b/src/SAWScript/Options.hs @@ -12,6 +12,7 @@ Stability : provisional module SAWScript.Options where import Data.Char (toLower) +import Data.List (partition) import Data.Time import System.Console.GetOpt import System.Environment @@ -236,6 +237,12 @@ processEnv opts = do addSawOpt ("SAW_IMPORT_PATH", p) os = os { importPath = importPath os ++ splitSearchPath p } addSawOpt ("SAW_JDK_JAR", p) os = os { jarList = p : jarList os } + addSawOpt ("CLASSPATH", p) os = os { jarList = jarList os ++ jars + , classPath = classPath os ++ dirs + } + where + es = splitSearchPath p + (jars, dirs) = partition (".jar" `isExtensionOf`) es addSawOpt _ os = os pathDesc, pathDelim :: String From fecb0835561ffb0b85a3a7789bb5e26a3d144555 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 26 Jul 2021 10:34:55 -0700 Subject: [PATCH 06/10] Add built-in documentation for Java RPC methods --- saw-remote-api/saw-remote-api/Main.hs | 6 +++--- saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs | 5 +++++ saw-remote-api/src/SAWServer/JVMVerify.hs | 10 ++++++++++ 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 67454230d9..0b926e07d4 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -77,15 +77,15 @@ sawMethods = -- JVM , Argo.command "SAW/JVM/load class" - (Doc.Paragraph [Doc.Text "TODO"]) + jvmLoadClassDescr jvmLoadClass , Argo.command "SAW/JVM/verify" - (Doc.Paragraph [Doc.Text "TODO"]) + jvmVerifyDescr jvmVerify , Argo.command "SAW/JVM/assume" - (Doc.Paragraph [Doc.Text "TODO"]) + jvmAssumeDescr jvmAssume -- LLVM , Argo.command diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index cd1dd7f760..3aaf83b616 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -11,6 +11,7 @@ {-# LANGUAGE TupleSections #-} module SAWServer.JVMCrucibleSetup ( jvmLoadClass + , jvmLoadClassDescr , compileJVMContract ) where @@ -203,6 +204,10 @@ jvmLoadClass (JVMLoadClassParams serverName cname) = setServerVal serverName c ok +jvmLoadClassDescr :: Doc.Block +jvmLoadClassDescr = + Doc.Paragraph [Doc.Text "Load the JVM class with the given name for later verification."] + instance Doc.DescribedMethod JVMLoadClassParams OK where parameterFieldDescription = [ ("name", diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index 3e64fedfbf..f7c97654ed 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -2,7 +2,9 @@ module SAWServer.JVMVerify ( jvmVerify + , jvmVerifyDescr , jvmAssume + , jvmAssumeDescr ) where import Prelude hiding (mod) @@ -14,6 +16,7 @@ import SAWScript.JavaExpr (JavaType(..)) import SAWScript.Value (rwCryptol) import qualified Argo +import qualified Argo.Doc as Doc import SAWServer ( SAWState, SAWTask(JVMSetup), @@ -63,7 +66,14 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc jvmVerify :: VerifyParams JavaType -> Argo.Command SAWState OK jvmVerify = jvmVerifyAssume VerifyContract +jvmVerifyDescr :: Doc.Block +jvmVerifyDescr = + Doc.Paragraph [Doc.Text "Verify the named JVM method meets its specification."] jvmAssume :: AssumeParams JavaType -> Argo.Command SAWState OK jvmAssume (AssumeParams className fun contract lemmaName) = jvmVerifyAssume AssumeContract (VerifyParams className fun [] False contract (ProofScript []) lemmaName) + +jvmAssumeDescr :: Doc.Block +jvmAssumeDescr = + Doc.Paragraph [Doc.Text "Assume the named JVM method meets its specification."] From 1582cb9e3d6c23cfcf423b7716c76a7ae77e8080 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 26 Jul 2021 12:06:49 -0700 Subject: [PATCH 07/10] Remove optional list type from Python client --- saw-remote-api/python/saw_client/__init__.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index f566703aec..76f2d13dff 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -436,7 +436,7 @@ def jvm_assume(cls: JVMClass, def jvm_verify(cls: JVMClass, method_name: str, contract: llvm.Contract, - lemmas: Optional[List[VerificationResult]] = None, + lemmas: List[VerificationResult] = [], check_sat: bool = False, script: Optional[proofscript.ProofScript] = None, lemma_name_hint: Optional[str] = None) -> VerificationResult: @@ -445,8 +445,6 @@ def jvm_verify(cls: JVMClass, argument in further calls to `jvm_verify` """ - if lemmas is None: - lemmas = [] if script is None: script = proofscript.ProofScript([proofscript.z3([])]) if lemma_name_hint is None: @@ -561,13 +559,11 @@ def llvm_assume(module: LLVMModule, def llvm_verify(module: LLVMModule, function: str, contract: llvm.Contract, - lemmas: Optional[List[VerificationResult]] = None, + lemmas: List[VerificationResult] = [], check_sat: bool = False, script: Optional[proofscript.ProofScript] = None, lemma_name_hint: Optional[str] = None) -> VerificationResult: - if lemmas is None: - lemmas = [] if script is None: script = proofscript.ProofScript([proofscript.z3([])]) if lemma_name_hint is None: From 6c98f48acd3cc91faeee2d6e24784275eedbd1ea Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 26 Jul 2021 12:07:16 -0700 Subject: [PATCH 08/10] Test assumption, composition for RPC Java proofs --- .../python/tests/saw/test_basic_java.py | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py index 5fb60cac9b..066b78f0fe 100644 --- a/saw-remote-api/python/tests/saw/test_basic_java.py +++ b/saw-remote-api/python/tests/saw/test_basic_java.py @@ -17,6 +17,17 @@ def specification(self) -> None: self.returns(cryptol("(+)")(x,y)) +class Double(Contract): + def __init__(self) -> None: + super().__init__() + + def specification(self) -> None: + x = self.fresh_var(java_int, "x") + + self.execute_func(x) + + self.returns(cryptol("(+)")(x,x)) + class AddTest(unittest.TestCase): def test_add(self): saw.connect(reset_server=True) @@ -25,8 +36,15 @@ def test_add(self): cls = saw.jvm_load_class("Add") - result = saw.jvm_verify(cls, 'add', Add()) - self.assertIs(result.is_success(), True) + add_result1 = saw.jvm_verify(cls, 'add', Add()) + self.assertIs(add_result1.is_success(), True) + add_result2 = saw.jvm_assume(cls, 'add', Add()) + self.assertIs(add_result2.is_success(), True) + + dbl_result1 = saw.jvm_verify(cls, 'dbl', Double(), lemmas=[add_result1]) + self.assertIs(dbl_result1.is_success(), True) + dbl_result2 = saw.jvm_verify(cls, 'dbl', Double(), lemmas=[add_result2]) + self.assertIs(dbl_result2.is_success(), True) if __name__ == "__main__": From 53eb9e31d7d954ad5d589cc7875efcd9ba83aa87 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 13 Sep 2021 14:57:12 -0700 Subject: [PATCH 09/10] Update RPC docs to reflect current server output --- saw-remote-api/docs/SAW.rst | 114 ++++++++++++++++++++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 2454864ee6..07b640383d 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -1,3 +1,4 @@ +Up to date SAW RPC Server ============== @@ -132,6 +133,119 @@ No return fields +SAW/JVM/load class (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Load the JVM class with the given name for later verification. + +Parameter fields +++++++++++++++++ + + +``name`` + The name of the class on the server. + + + +``class name`` + The java class to load. + + + +Return fields ++++++++++++++ + +No return fields + + + +SAW/JVM/verify (command) +~~~~~~~~~~~~~~~~~~~~~~~~ + +Verify the named JVM method meets its specification. + +Parameter fields +++++++++++++++++ + + +``module`` + The module of the function being verified. + + + +``function`` + The function being verified. + + + +``lemmas`` + The specifications to use for other functions during this verification. + + + +``check sat`` + Whether or not to enable path satisfiability checking. + + + +``contract`` + The specification to verify for the function. + + + +``script`` + The script to use to prove the validity of the resulting verification conditions. + + + +``lemma name`` + The name to refer to this verification/contract by later. + + + +Return fields ++++++++++++++ + +No return fields + + + +SAW/JVM/assume (command) +~~~~~~~~~~~~~~~~~~~~~~~~ + +Assume the named JVM method meets its specification. + +Parameter fields +++++++++++++++++ + + +``module`` + The LLVM module containing the function. + + + +``function`` + The function we are assuming a contract for. + + + +``contract`` + The specification to assume for the function. + + + +``lemma name`` + The name to refer to this assumed contract by later. + + + +Return fields ++++++++++++++ + +No return fields + + + SAW/LLVM/load module (command) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From 41be183b5355ce79143c0a69d94feb4eb40fc774 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 13 Sep 2021 16:45:53 -0700 Subject: [PATCH 10/10] Remove Cabal message from SAW RPC docs --- saw-remote-api/docs/SAW.rst | 1 - 1 file changed, 1 deletion(-) diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 07b640383d..59521f8cfa 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -1,4 +1,3 @@ -Up to date SAW RPC Server ==============