From fcf1abf246dc1613a786f261b0bb1f8aa06bb987 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 31 Jan 2025 10:25:23 -0500 Subject: [PATCH] crucible-saw: rm Fixes #1281 --- .github/workflows/lint.yml | 1 - README.md | 2 - crucible-saw/LICENSE | 30 - crucible-saw/Setup.hs | 2 - crucible-saw/crucible-saw.cabal | 34 - .../src/Lang/Crucible/Backend/SAWCore.hs | 1296 ----------------- .../Lang/Crucible/Solver/ExtractSAWCore.hs | 495 ------- 7 files changed, 1860 deletions(-) delete mode 100644 crucible-saw/LICENSE delete mode 100644 crucible-saw/Setup.hs delete mode 100644 crucible-saw/crucible-saw.cabal delete mode 100644 crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs delete mode 100644 crucible-saw/src/Lang/Crucible/Solver/ExtractSAWCore.hs diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index c477f4f0d..03bc52f85 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -29,7 +29,6 @@ jobs: (cd crucible-llvm-cli/; ../hlint-3.8/hlint src test) (cd crucible-llvm-syntax/; ../hlint-3.8/hlint src test) (cd crucible-mir/; ../hlint-3.8/hlint src) - (cd crucible-saw/; ../hlint-3.8/hlint src) (cd crucible-symio/; ../hlint-3.8/hlint src tests) (cd crucible-syntax/; ../hlint-3.8/hlint src test) (cd crucible-wasm/; ../hlint-3.8/hlint src test) diff --git a/README.md b/README.md index ed7f055c2..8083bd9a4 100644 --- a/README.md +++ b/README.md @@ -24,8 +24,6 @@ Currently, the repository consists of the following Haskell packages: executing LLVM assembly programs in the Crucible symbolic simulator. * **`crucible-jvm`** provides translation and runtime support for executing JVM bytecode programs in the Crucible symbolic simulator. - * **`crucible-saw`** provides functionality for generating - SAW Core terms from Crucible Control-Flow-Graphs. * **`crux`** provides common support libraries for running the crucible simulator in a basic "all-at-once" use mode for simulation and verification. This includes most of the setup steps required diff --git a/crucible-saw/LICENSE b/crucible-saw/LICENSE deleted file mode 100644 index 0b558b495..000000000 --- a/crucible-saw/LICENSE +++ /dev/null @@ -1,30 +0,0 @@ -Copyright (c) 2013-2018 Galois Inc. -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in - the documentation and/or other materials provided with the - distribution. - - * Neither the name of Galois, Inc. nor the names of its contributors - may be used to endorse or promote products derived from this - software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS -IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED -TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A -PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER -OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/crucible-saw/Setup.hs b/crucible-saw/Setup.hs deleted file mode 100644 index 9a994af67..000000000 --- a/crucible-saw/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/crucible-saw/crucible-saw.cabal b/crucible-saw/crucible-saw.cabal deleted file mode 100644 index bfff84487..000000000 --- a/crucible-saw/crucible-saw.cabal +++ /dev/null @@ -1,34 +0,0 @@ -Name: crucible-saw -Version: 0.1 -Author: Galois Inc. -Maintainer: rdockins@galois.com -License: BSD3 -License-file: LICENSE -Build-type: Simple -Cabal-version: >= 1.9.2 -Category: Language -Synopsis: Crucible bindings to SAW -Description: - This package provides a Crucible solver backend that produces - SAWCore terms. - -library - build-depends: - base >= 4.7 && < 4.15, - bv-sized >= 1.0.0, - containers, - crucible >= 0.1, - what4 >= 0.4, - lens, - text, - parameterized-utils, - saw-core >= 0.1 - - hs-source-dirs: src - - exposed-modules: - Lang.Crucible.Backend.SAWCore --- Lang.Crucible.Solver.ExtractSAWCore - - ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns - ghc-prof-options: -O2 -fprof-auto-top diff --git a/crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs b/crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs deleted file mode 100644 index f04f1605a..000000000 --- a/crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs +++ /dev/null @@ -1,1296 +0,0 @@ ------------------------------------------------------------------------ --- | --- Module : Lang.Crucible.Backend.SAWCore --- Description : Crucible interface for generating SAWCore --- Copyright : (c) Galois, Inc 2014-2016 --- License : BSD3 --- Maintainer : Rob Dockins --- Stability : provisional --- --- This module provides a Crucible backend that produces SAWCore terms. ------------------------------------------------------------------------- -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ViewPatterns #-} - -module Lang.Crucible.Backend.SAWCore where - -import Control.Exception ( bracket ) -import Control.Lens -import Control.Monad -import qualified Data.BitVector.Sized as BV -import Data.IORef -import Data.List (elemIndex) -import Data.Foldable (toList) -import Data.IntMap (IntMap) -import qualified Data.IntMap as IntMap -import Data.List.NonEmpty (NonEmpty(..)) -import Data.Map ( Map ) -import qualified Data.Map as Map -import qualified Data.Parameterized.Context as Ctx -import Data.Parameterized.Nonce -import Data.Parameterized.Some -import Data.Parameterized.TraversableFC -import Data.Ratio -import Data.Sequence (Seq) -import qualified Data.Sequence as Seq -import Data.Word(Word64) -import qualified Data.Text as Text - -import Numeric.Natural - -import What4.BaseTypes -import What4.Config -import What4.Interface -import qualified What4.Expr.ArrayUpdateMap as AUM -import qualified What4.Expr.Builder as B -import qualified What4.Expr.BoolMap as BM -import qualified What4.Expr.WeightedSum as WSum -import What4.ProgramLoc -import What4.Protocol.Online -import What4.Protocol.SMTWriter as SMT -import What4.SatResult -import qualified What4.SemiRing as B -import qualified What4.Solver.Yices as Yices -import What4.Symbol - -import Lang.Crucible.Panic(panic) -import Lang.Crucible.Backend -import Lang.Crucible.Backend.Online hiding (withSolverProcess) -import qualified Lang.Crucible.Backend.AssumptionStack as AS -import Lang.Crucible.Simulator.SimError - -import qualified Verifier.SAW.SharedTerm as SC -import qualified Verifier.SAW.TypedAST as SC - -data SAWCruciblePersonality sym = SAWCruciblePersonality - --- | The SAWCoreBackend is a crucible backend that represents symbolic values --- as SAWCore terms. -data SAWCoreState solver fs n - = SAWCoreState - { saw_ctx :: SC.SharedContext -- ^ the main SAWCore datastructure for building shared terms - , saw_inputs :: IORef (Seq (SC.ExtCns SC.Term )) - -- ^ a record of all the symbolic input variables created so far, - -- in the order they were created - - , saw_symMap :: !(Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term)) - -- ^ What to do with uninterpreted functions. - -- The key is the "indexValue" of the "symFunId" for the function - - , saw_elt_cache :: B.IdxCache n SAWExpr - -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term. - - , saw_elt_cache_r :: IORef (IntMap (Some (B.SymExpr (SAWCoreBackend n solver fs)))) - -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable. - -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between - -- SAWCore terms and What4 variables. - - , saw_online_state :: OnlineBackendState solver n - } - -data SAWExpr (bt :: BaseType) where - SAWExpr :: !SC.Term -> SAWExpr bt - - -- This is a term that represents an integer, but has an - -- implicit integer-to-real conversion. - IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType - -- This is a SAWCore term that represents a natural number, but has an - -- implicit nat-to-integer conversion. - NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType - -type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs - - --- | Run the given IO action with the given SAW backend. --- While while running the action, the SAW backend is --- set up with a fresh naming context. This means that all --- symbolic inputs, symMap entries, element cache entires, --- assertions and proof obligations start empty while --- running the action. After the action completes, the --- state of these fields is restored. -inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a -inFreshNamingContext sym f = - do old <- readIORef (B.sbStateManager sym) - bracket (mkNew (B.exprCounter sym) old) (restore old) action - - where - action new = - do writeIORef (B.sbStateManager sym) new - f - - restore old _new = - do writeIORef (B.sbStateManager sym) old - - mkNew _gen old = - do ch <- B.newIdxCache - ch_r <- newIORef IntMap.empty - iref <- newIORef mempty - let new = SAWCoreState - { saw_ctx = saw_ctx old - , saw_inputs = iref - , saw_symMap = mempty - , saw_elt_cache = ch - , saw_elt_cache_r = ch_r - , saw_online_state = saw_online_state old - } - return new - -getInputs :: SAWCoreBackend n solver fs -> IO (Seq (SC.ExtCns SC.Term)) -getInputs sym = - do st <- readIORef (B.sbStateManager sym) - readIORef (saw_inputs st) - -baseSCType :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - BaseTypeRepr tp -> - IO SC.Term -baseSCType sym sc bt = - case bt of - BaseBoolRepr -> SC.scBoolType sc - BaseBVRepr w -> SC.scBitvector sc $ fromIntegral (natValue w) - BaseNatRepr -> SC.scNatType sc - BaseIntegerRepr -> SC.scIntegerType sc - BaseArrayRepr indexTypes range - | Ctx.Empty Ctx.:> idx_type <- indexTypes -> - do sc_idx_type <- baseSCType sym sc idx_type - sc_elm_type <- baseSCType sym sc range - SC.scArrayType sc sc_idx_type sc_elm_type - | otherwise -> - unsupported sym "SAW backend does not support multidimensional Arrays: baseSCType" - BaseFloatRepr _ -> - unsupported sym "SAW backend does not support IEEE-754 floating point values: baseSCType" - BaseStringRepr _ -> - unsupported sym "SAW backend does not support string values: baseSCType" - BaseComplexRepr -> - unsupported sym "SAW backend does not support complex values: baseSCType" - BaseRealRepr -> - unsupported sym "SAW backend does not support real values: baseSCType" - BaseStructRepr ts -> - SC.scTupleType sc =<< baseSCTypes ts - where - baseSCTypes :: Ctx.Assignment BaseTypeRepr args -> IO [SC.Term] - baseSCTypes Ctx.Empty = return [] - baseSCTypes (xs Ctx.:> x) = - do ts <- baseSCTypes xs - t <- baseSCType sym sc x - return (ts ++ [t]) - --- | Create a new symbolic variable. -sawCreateVar :: SAWCoreBackend n solver fs - -> String -- ^ the name of the variable - -> SC.Term - -> IO SC.Term -sawCreateVar sym nm tp = do - st <- readIORef (B.sbStateManager sym) - let sc = saw_ctx st - ec <- SC.scFreshEC sc nm tp - t <- SC.scFlatTermF sc (SC.ExtCns ec) - modifyIORef (saw_inputs st) (\xs -> xs Seq.|> ec) - return t - -bindSAWTerm :: SAWCoreBackend n solver fs - -> BaseTypeRepr bt - -> SC.Term - -> IO (B.Expr n bt) -bindSAWTerm sym bt t = do - st <- readIORef $ B.sbStateManager sym - ch_r <- readIORef $ saw_elt_cache_r st - let midx = - case t of - SC.STApp { SC.stAppIndex = idx } -> Just idx - SC.Unshared _ -> Nothing - case midx >>= flip IntMap.lookup ch_r of - Just (Some var) -> do - Just Refl <- return $ testEquality bt (B.exprType var) - return var - Nothing -> do - sbVar@(B.BoundVarExpr bv) <- freshConstant sym emptySymbol bt - B.insertIdxValue (saw_elt_cache st) (B.bvarId bv) (SAWExpr t) - case midx of - Just i -> modifyIORef' (saw_elt_cache_r st) $ IntMap.insert i (Some sbVar) - Nothing -> pure () - return sbVar - -newSAWCoreBackend :: - FloatModeRepr fm -> - SC.SharedContext -> - NonceGenerator IO s -> - IO (SAWCoreBackend s Yices.Connection (Flags fm)) -newSAWCoreBackend fm sc gen = do - inpr <- newIORef Seq.empty - ch <- B.newIdxCache - ch_r <- newIORef IntMap.empty - let feats = Yices.yicesDefaultFeatures - ob_st0 <- initialOnlineBackendState gen feats - let st0 = SAWCoreState - { saw_ctx = sc - , saw_inputs = inpr - , saw_symMap = Map.empty - , saw_elt_cache = ch - , saw_elt_cache_r = ch_r - , saw_online_state = ob_st0 - } - sym <- B.newExprBuilder fm st0 gen - let options = backendOptions ++ onlineBackendOptions ob_st0 ++ Yices.yicesOptions - extendConfig options (getConfiguration sym) - - enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) - let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } - - writeIORef (B.sbStateManager sym) st - return sym - --- | Register an interpretation for a symbolic function. This is not --- used during simulation, but rather, when we translate Crucible --- values back into SAW. The interpretation function takes a list of --- arguments in regular (left-to-right) order. -sawRegisterSymFunInterp :: - SAWCoreBackend n solver fs -> - B.ExprSymFn n (B.Expr n) args ret -> - (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> - IO () -sawRegisterSymFunInterp sym f i = - modifyIORef (B.sbStateManager sym) $ \s -> - s { saw_symMap = Map.insert (indexValue (B.symFnId f)) i (saw_symMap s) } - - -sawBackendSharedContext :: SAWCoreBackend n solver fs -> IO SC.SharedContext -sawBackendSharedContext sym = - saw_ctx <$> readIORef (B.sbStateManager sym) - - -toSC :: OnlineSolver solver => - SAWCoreBackend n solver fs -> B.Expr n tp -> IO SC.Term -toSC sym elt = - do st <- readIORef $ B.sbStateManager sym - evaluateExpr sym (saw_ctx st) (saw_elt_cache st) elt - - --- | Return a shared term with type nat from a SAWExpr. -scAsIntExpr :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - IO SC.Term -scAsIntExpr _ sc (IntToRealSAWExpr (NatToIntSAWExpr (SAWExpr t))) = SC.scNatToInt sc t -scAsIntExpr _ _ (IntToRealSAWExpr (SAWExpr t)) = return t -scAsIntExpr sym _ SAWExpr{} = unsupported sym - "SAWbackend does not support real values." - --- | Create a Real SAWELT value from a Rational. --- --- This fails on non-integer expressions. -scRealLit :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - Rational -> - IO (SAWExpr BaseRealType) -scRealLit sym sc r - | denominator r /= 1 = - unsupported sym "SAW backend does not support real values" - | r >= 0 = - IntToRealSAWExpr . NatToIntSAWExpr . SAWExpr <$> SC.scNat sc (fromInteger (numerator r)) - | otherwise = - IntToRealSAWExpr <$> scIntLit sc (numerator r) - --- | Create a SAWCore term with type 'Integer' from a Haskell Integer. -scIntLit :: SC.SharedContext -> Integer -> IO (SAWExpr BaseIntegerType) -scIntLit sc i - | i >= 0 = - SAWExpr <$> (SC.scNatToInt sc =<< SC.scNat sc (fromInteger i)) - | otherwise = - SAWExpr <$> (SC.scIntNeg sc =<< SC.scNatToInt sc =<< SC.scNat sc (fromInteger (negate i))) - --- | Create a SAWCore term with type 'Nat' from a Haskell Nat. -scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) -scNatLit sc n = SAWExpr <$> SC.scNat sc n - -scBvLit :: SC.SharedContext -> NatRepr w -> BV.BV w -> IO (SAWExpr (BaseBVType w)) -scBvLit sc w bv = SAWExpr <$> SC.scBvConst sc (natValue w) (BV.asUnsigned bv) - - -scRealCmpop :: - OnlineSolver solver => - (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseBoolType)) -> - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseBoolType) -scRealCmpop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = - intOp sc x y -scRealCmpop _ sym _ _ _ = - unsupported sym "SAW backend does not support real values" - -scRealBinop :: - OnlineSolver solver => - (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseIntegerType)) -> - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseRealType) -scRealBinop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = - IntToRealSAWExpr <$> intOp sc x y -scRealBinop _ sym _ _ _ = - unsupported sym "SAW backend does not support real values" - - -scIntBinop :: - (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType)) - {- ^ operation on naturals -} -> - (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> - SC.SharedContext -> - SAWExpr BaseIntegerType -> - SAWExpr BaseIntegerType -> - IO (SAWExpr BaseIntegerType) -scIntBinop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = - NatToIntSAWExpr <$> natOp sc x y -scIntBinop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = - SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) -scIntBinop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = - SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) -scIntBinop _natOp intOp sc (SAWExpr x) (SAWExpr y) = - SAWExpr <$> intOp sc x y - -scIntCmpop :: - (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType)) - {- ^ operation on naturals -} -> - (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> - SC.SharedContext -> - SAWExpr BaseIntegerType -> - SAWExpr BaseIntegerType -> - IO (SAWExpr BaseBoolType) -scIntCmpop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = - natOp sc x y -scIntCmpop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = - SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) -scIntCmpop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = - SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) -scIntCmpop _natOp intOp sc (SAWExpr x) (SAWExpr y) = - SAWExpr <$> intOp sc x y - -scAddReal :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseRealType) -scAddReal = scRealBinop scAddInt - -scAddInt :: SC.SharedContext - -> SAWExpr BaseIntegerType - -> SAWExpr BaseIntegerType - -> IO (SAWExpr BaseIntegerType) -scAddInt = scIntBinop scAddNat SC.scIntAdd - -scAddNat :: SC.SharedContext - -> SAWExpr BaseNatType - -> SAWExpr BaseNatType - -> IO (SAWExpr BaseNatType) -scAddNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scAddNat sc x y - - -scMulReal :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseRealType) -scMulReal = scRealBinop scMulInt - -scMulInt :: SC.SharedContext - -> SAWExpr BaseIntegerType - -> SAWExpr BaseIntegerType - -> IO (SAWExpr BaseIntegerType) -scMulInt = scIntBinop scMulNat SC.scIntMul - -scMulNat :: SC.SharedContext - -> SAWExpr BaseNatType - -> SAWExpr BaseNatType - -> IO (SAWExpr BaseNatType) -scMulNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scMulNat sc x y - -scIteReal :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SC.Term -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseRealType) -scIteReal sym sc p = scRealBinop (\sc' -> scIteInt sc' p) sym sc - -scIteInt :: SC.SharedContext - -> SC.Term - -> SAWExpr BaseIntegerType - -> SAWExpr BaseIntegerType - -> IO (SAWExpr BaseIntegerType) -scIteInt sc p = scIntBinop - (\sc' -> scIteNat sc' p) - (\sc' x y -> SC.scIntegerType sc >>= \tp -> SC.scIte sc' tp p x y) - sc - -scIteNat :: SC.SharedContext - -> SC.Term - -> SAWExpr BaseNatType - -> SAWExpr BaseNatType - -> IO (SAWExpr BaseNatType) -scIteNat sc p (SAWExpr x) (SAWExpr y) = - SAWExpr <$> (SC.scNatType sc >>= \tp -> SC.scIte sc tp p x y) - -scIte :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - BaseTypeRepr tp -> - SAWExpr BaseBoolType -> - SAWExpr tp -> - SAWExpr tp -> - IO (SAWExpr tp) -scIte sym sc tp (SAWExpr p) x y = - case tp of - BaseRealRepr -> scIteReal sym sc p x y - BaseNatRepr -> scIteNat sc p x y - BaseIntegerRepr -> scIteInt sc p x y - _ -> - do tp' <- baseSCType sym sc tp - x' <- termOfSAWExpr sym sc x - y' <- termOfSAWExpr sym sc y - SAWExpr <$> SC.scIte sc tp' p x' y' - - -scRealEq :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseBoolType) -scRealEq = scRealCmpop scIntEq - -scIntEq :: SC.SharedContext - -> SAWExpr BaseIntegerType - -> SAWExpr BaseIntegerType - -> IO (SAWExpr BaseBoolType) -scIntEq = scIntCmpop scNatEq SC.scIntEq - -scNatEq :: SC.SharedContext - -> SAWExpr BaseNatType - -> SAWExpr BaseNatType - -> IO (SAWExpr BaseBoolType) -scNatEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scEqualNat sc x y - -scBoolEq :: - SC.SharedContext -> - SAWExpr BaseBoolType -> - SAWExpr BaseBoolType -> - IO (SAWExpr BaseBoolType) -scBoolEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scBoolEq sc x y - -scEq :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - BaseTypeRepr tp -> - SAWExpr tp -> - SAWExpr tp -> - IO (SAWExpr BaseBoolType) -scEq sym sc tp x y = - case tp of - BaseBoolRepr -> scBoolEq sc x y - BaseRealRepr -> scRealEq sym sc x y - BaseNatRepr -> scNatEq sc x y - BaseIntegerRepr -> scIntEq sc x y - BaseBVRepr w -> - do let SAWExpr x' = x - let SAWExpr y' = y - w' <- SC.scNat sc $ fromIntegral (natValue w) - SAWExpr <$> SC.scBvEq sc w' x' y' - _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" ++ show tp) - - -scAllEq :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - Ctx.Assignment BaseTypeRepr ctx -> - Ctx.Assignment SAWExpr ctx -> - Ctx.Assignment SAWExpr ctx -> - IO (SAWExpr BaseBoolType) -scAllEq _sym sc Ctx.Empty _ _ = SAWExpr <$> SC.scBool sc True -scAllEq sym sc (ctx Ctx.:> tp) (xs Ctx.:> x) (ys Ctx.:> y) - | Ctx.null ctx = scEq sym sc tp x y - | otherwise = - do SAWExpr p <- scAllEq sym sc ctx xs ys - SAWExpr q <- scEq sym sc tp x y - SAWExpr <$> SC.scAnd sc p q - -scRealLe, scRealLt :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr BaseRealType -> - SAWExpr BaseRealType -> - IO (SAWExpr BaseBoolType) -scRealLe = scRealCmpop scIntLe -scRealLt = scRealCmpop scIntLt - -scIntLe, scIntLt :: - SC.SharedContext -> - SAWExpr BaseIntegerType -> - SAWExpr BaseIntegerType -> - IO (SAWExpr BaseBoolType) -scIntLe = scIntCmpop scNatLe SC.scIntLe -scIntLt = scIntCmpop scNatLt SC.scIntLt - -scNatLe, scNatLt :: - SC.SharedContext -> - SAWExpr BaseNatType -> - SAWExpr BaseNatType -> - IO (SAWExpr BaseBoolType) -scNatLe sc (SAWExpr x) (SAWExpr y) = - do lt <- SC.scLtNat sc x y - eq <- SC.scEqualNat sc x y - SAWExpr <$> SC.scOr sc lt eq -scNatLt sc (SAWExpr x) (SAWExpr y) = - SAWExpr <$> SC.scLtNat sc x y - -scBvAdd :: - SC.SharedContext -> - NatRepr w -> - SAWExpr (BaseBVType w) -> - SAWExpr (BaseBVType w) -> - IO (SAWExpr (BaseBVType w)) -scBvAdd sc w (SAWExpr x) (SAWExpr y) = - do n <- SC.scNat sc (natValue w) - SAWExpr <$> SC.scBvAdd sc n x y - -scBvNot :: - SC.SharedContext -> - NatRepr w -> - SAWExpr (BaseBVType w) -> - IO (SAWExpr (BaseBVType w)) -scBvNot sc w (SAWExpr x) = - do n <- SC.scNat sc (natValue w) - SAWExpr <$> SC.scBvNot sc n x - -scBvMul :: - SC.SharedContext -> - NatRepr w -> - SAWExpr (BaseBVType w) -> - SAWExpr (BaseBVType w) -> - IO (SAWExpr (BaseBVType w)) -scBvMul sc w (SAWExpr x) (SAWExpr y) = - do n <- SC.scNat sc (natValue w) - SAWExpr <$> SC.scBvMul sc n x y - -scBvAnd :: - SC.SharedContext -> - NatRepr w -> - SAWExpr (BaseBVType w) -> - SAWExpr (BaseBVType w) -> - IO (SAWExpr (BaseBVType w)) -scBvAnd sc w (SAWExpr x) (SAWExpr y) = - do n <- SC.scNat sc (natValue w) - SAWExpr <$> SC.scBvAnd sc n x y - -scBvXor :: - SC.SharedContext -> - NatRepr w -> - SAWExpr (BaseBVType w) -> - SAWExpr (BaseBVType w) -> - IO (SAWExpr (BaseBVType w)) -scBvXor sc w (SAWExpr x) (SAWExpr y) = - do n <- SC.scNat sc (natValue w) - SAWExpr <$> SC.scBvXor sc n x y - -termOfSAWExpr :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - SAWExpr tp -> IO SC.Term -termOfSAWExpr sym sc expr = - case expr of - SAWExpr t -> return t - NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t - IntToRealSAWExpr _ - -> unsupported sym "SAW backend does not support real values" - -applyExprSymFn :: - forall n solver fs args ret. - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - B.ExprSymFn n (B.Expr n) args ret -> - Ctx.Assignment SAWExpr args -> - IO (SAWExpr ret) -applyExprSymFn sym sc fn args = - do st <- readIORef (B.sbStateManager sym) - mk <- - case Map.lookup (indexValue (B.symFnId fn)) (saw_symMap st) of - Nothing -> panic "SAWCore.applyExprSymFn" - [ "Unknown symbolic function." - , "*** Name: " ++ show fn - ] - Just mk -> return mk - ts <- evaluateAsgn args - SAWExpr <$> mk sc (reverse ts) - where - evaluateAsgn :: Ctx.Assignment SAWExpr args' -> IO [SC.Term] - evaluateAsgn Ctx.Empty = return [] - evaluateAsgn (xs Ctx.:> x) = - do vs <- evaluateAsgn xs - v <- termOfSAWExpr sym sc x - return (v : vs) - - -considerSatisfiability :: - OnlineSolver solver => - SAWCoreBackend n solver fs -> - Maybe ProgramLoc -> - B.BoolExpr n -> - IO BranchResult -considerSatisfiability sym mbPloc p = - withSolverProcess' - (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) sym - (pure IndeterminateBranchResult) - $ \proc -> - do pnot <- notPred sym p - let locDesc = case mbPloc of - Just ploc -> show (plSourceLoc ploc) - Nothing -> "(unknown location)" - let rsn = "branch sat: " ++ locDesc - p_res <- checkSatisfiable proc rsn p - pnot_res <- checkSatisfiable proc rsn pnot - case (p_res, pnot_res) of - (Unsat{}, Unsat{}) -> return UnsatisfiableContext - (_ , Unsat{}) -> return (NoBranch True) - (Unsat{}, _ ) -> return (NoBranch False) - _ -> return IndeterminateBranchResult - -{- | Declare that we don't support something or other. -This aborts the current path of execution, and adds a proof -obligation to ensure that we won't get there. -These proof obligations are all tagged with "Unsupported", so that -users of the library can choose if they will try to discharge them, -fail in some other way, or just ignore them. -} -unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> String -> IO a -unsupported sym x = addFailedAssertion sym (Unsupported x) - -evaluateExpr :: forall n solver tp fs. - OnlineSolver solver => - SAWCoreBackend n solver fs -> - SC.SharedContext -> - B.IdxCache n SAWExpr -> - B.Expr n tp -> - IO SC.Term -evaluateExpr sym sc cache = f [] - where - -- Evaluate the element, and expect the result to have the same type. - f :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO SC.Term - f env elt = termOfSAWExpr sym sc =<< eval env elt - - eval :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') - eval env elt = B.idxCacheEval cache elt (go env elt) - - realFail :: IO a - realFail = unsupported sym "SAW backend does not support real values" - - cplxFail :: IO a - cplxFail = unsupported sym "SAW backend does not support complex values" - - floatFail :: IO a - floatFail = unsupported sym "SAW backend does not support floating-point values" - - stringFail :: IO a - stringFail = unsupported sym "SAW backend does not support string values" - - unimplemented :: String -> IO a - unimplemented x = unsupported sym $ "SAW backend: not implemented: " ++ x - - go :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') - - go _ (B.BoolExpr b _) = SAWExpr <$> SC.scBool sc b - - go _ (B.SemiRingLiteral sr x _) = - case sr of - B.SemiRingNatRepr -> scNatLit sc x - B.SemiRingBVRepr _ w -> scBvLit sc w x - B.SemiRingIntegerRepr -> scIntLit sc x - B.SemiRingRealRepr -> scRealLit sym sc x - - go _ (B.StringExpr{}) = - unsupported sym "SAW backend does not support string values" - - go env (B.BoundVarExpr bv) = - case B.bvarKind bv of - B.UninterpVarKind -> do - tp <- baseSCType sym sc (B.bvarType bv) - SAWExpr <$> sawCreateVar sym nm tp - where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv - B.LatchVarKind -> - unsupported sym "SAW backend does not support latch variables" - B.QuantifierVarKind -> do - case elemIndex (Just $ B.bvarName bv) env of - Nothing -> unsupported sym $ "unbound quantifier variable " <> nm - Just idx -> SAWExpr <$> SC.scLocalVar sc idx - where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv - - go env (B.NonceAppExpr p) = - case B.nonceExprApp p of - B.Annotation _tpr _n x -> - eval env x - - B.Forall bvar body -> - case B.bvarType bvar of - BaseBVRepr wrepr -> do - w <- SC.scNat sc $ natValue wrepr - ty <- SC.scVecType sc w =<< SC.scBoolType sc - SAWExpr <$> - (SC.scBvForall sc w - =<< SC.scLambda sc nm ty =<< f (Just (B.bvarName bvar):env) body) - where nm = solverSymbolAsText $ B.bvarName bvar - _ -> unsupported sym "SAW backend only supports universal quantifiers over bitvectors" - B.Exists{} -> - unsupported sym "SAW backend does not support existential quantifiers" - B.ArrayFromFn{} -> unimplemented "ArrayFromFn" - B.MapOverArrays{} -> unimplemented "MapOverArrays" - B.ArrayTrueOnEntries{} -> unimplemented "ArrayTrueOnEntries" - B.FnApp fn asgn -> - do args <- traverseFC (eval env) asgn - applyExprSymFn sym sc fn args - - go env a0@(B.AppExpr a) = - let nyi = unsupported sym $ - "Expression form not yet implemented in SAWCore backend:\n" - ++ show a0 - in - case B.appExprApp a of - B.BaseIte bt _ c xe ye -> join (scIte sym sc bt <$> eval env c <*> eval env xe <*> eval env ye) - B.BaseEq bt xe ye -> join (scEq sym sc bt <$> eval env xe <*> eval env ye) - - B.SemiRingLe sr xe ye -> - case sr of - B.OrderedSemiRingRealRepr -> join (scRealLe sym sc <$> eval env xe <*> eval env ye) - B.OrderedSemiRingIntegerRepr -> join (scIntLe sc <$> eval env xe <*> eval env ye) - B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) - - B.NotPred x -> - goNeg env x - - B.ConjPred xs -> - case BM.viewBoolMap xs of - BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True - BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False - BM.BoolMapTerms (t:|ts) -> - let pol (x,BM.Positive) = f env x - pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x - in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts) - - B.SemiRingProd pd -> - case WSum.prodRepr pd of - B.SemiRingRealRepr -> - do pd' <- WSum.prodEvalM (scMulReal sym sc) (eval env) pd - maybe (scRealLit sym sc 1) return pd' - B.SemiRingIntegerRepr -> - do pd' <- WSum.prodEvalM (scMulInt sc) (eval env) pd - maybe (scIntLit sc 1) return pd' - B.SemiRingNatRepr -> - do pd' <- WSum.prodEvalM (scMulNat sc) (eval env) pd - maybe (scNatLit sc 1) return pd' - B.SemiRingBVRepr B.BVArithRepr w -> - do n <- SC.scNat sc (natValue w) - pd' <- WSum.prodEvalM (SC.scBvMul sc n) (f env) pd - maybe (scBvLit sc w (BV.one w)) (return . SAWExpr) pd' - B.SemiRingBVRepr B.BVBitsRepr w -> - do n <- SC.scNat sc (natValue w) - pd' <- WSum.prodEvalM (SC.scBvAnd sc n) (f env) pd - maybe (scBvLit sc w (BV.maxUnsigned w)) (return . SAWExpr) pd' - - B.SemiRingSum ss -> - case WSum.sumRepr ss of - B.SemiRingRealRepr -> WSum.evalM add smul (scRealLit sym sc) ss - where add x y = scAddReal sym sc x y - smul 1 e = eval env e - smul sm e = join $ scMulReal sym sc <$> scRealLit sym sc sm <*> eval env e - B.SemiRingIntegerRepr -> WSum.evalM add smul (scIntLit sc) ss - where add x y = scAddInt sc x y - smul 1 e = eval env e - smul sm e = join $ scMulInt sc <$> scIntLit sc sm <*> eval env e - B.SemiRingNatRepr -> WSum.evalM add smul (scNatLit sc) ss - where add x y = scAddNat sc x y - smul 1 e = eval env e - smul sm e = join $ scMulNat sc <$> scNatLit sc sm <*> eval env e - B.SemiRingBVRepr B.BVArithRepr w -> WSum.evalM add smul (scBvLit sc w) ss - where add x y = scBvAdd sc w x y - smul (BV.BV 1) e = eval env e - smul sm e = join (scBvMul sc w <$> scBvLit sc w sm <*> eval env e) - B.SemiRingBVRepr B.BVBitsRepr w - | ss^.WSum.sumOffset == one -> scBvNot sc w =<< bitwise_eval (ss & WSum.sumOffset .~ BV.zero w) - | otherwise -> bitwise_eval ss - - where one = BV.maxUnsigned w - bitwise_eval = WSum.evalM add smul (scBvLit sc w) - add x y = scBvXor sc w x y - smul sm e - | sm == one = eval env e - | otherwise = join (scBvAnd sc w <$> scBvLit sc w sm <*> eval env e) - - B.RealIsInteger{} -> unsupported sym "SAW backend does not support real values" - - B.BVOrBits w bs -> - do n <- SC.scNat sc (natValue w) - bs' <- traverse (f env) (B.bvOrToList bs) - case bs' of - [] -> scBvLit sc w (BV.zero w) - x:xs -> SAWExpr <$> foldM (SC.scBvOr sc n) x xs - - B.BVFill w p -> - do bit <- SC.scBoolType sc - n <- SC.scNat sc (natValue w) - x <- f env p - SAWExpr <$> SC.scGlobalApply sc (SC.mkIdent SC.preludeName "replicate") [n, bit, x] - - B.BVTestBit i bv -> fmap SAWExpr $ do - w <- SC.scNat sc (natValue (bvWidth bv)) - bit <- SC.scBoolType sc - -- NB, SAWCore's `scAt` is big endian - let j = natValue (bvWidth bv) - i - 1 - join (SC.scAt sc w bit <$> f env bv <*> SC.scNat sc j) - - B.BVSlt x y -> fmap SAWExpr $ do - w <- SC.scNat sc (natValue (bvWidth x)) - join (SC.scBvSLt sc w <$> f env x <*> f env y) - B.BVUlt x y -> fmap SAWExpr $ do - w <- SC.scNat sc (natValue (bvWidth x)) - join (SC.scBvULt sc w <$> f env x <*> f env y) - - B.BVUnaryTerm{} -> unsupported sym "SAW backend does not support the unary bitvector representation" - - B.BVUdiv _ x y -> fmap SAWExpr $ do - n <- SC.scNat sc (natValue (bvWidth x)) - join (SC.scBvUDiv sc n <$> f env x <*> f env y) - B.BVUrem _ x y -> fmap SAWExpr $ do - n <- SC.scNat sc (natValue (bvWidth x)) - join (SC.scBvURem sc n <$> f env x <*> f env y) - B.BVSdiv _ x y -> fmap SAWExpr $ do - -- NB: bvSDiv applies 'Succ' to its width argument, so we - -- need to subtract 1 to make the types match. - n <- SC.scNat sc (natValue (bvWidth x) - 1) - join (SC.scBvSDiv sc n <$> f env x <*> f env y) - B.BVSrem _ x y -> fmap SAWExpr $ do - -- NB: bvSDiv applies 'Succ' to its width argument, so we - -- need to subtract 1 to make the types match. - n <- SC.scNat sc (natValue (bvWidth x) - 1) - join (SC.scBvSRem sc n <$> f env x <*> f env y) - B.BVShl _ x y -> fmap SAWExpr $ do - let w = natValue (bvWidth x) - n <- SC.scNat sc w - join (SC.scBvShl sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) - B.BVLshr _ x y -> fmap SAWExpr $ do - let w = natValue (bvWidth x) - n <- SC.scNat sc w - join (SC.scBvShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) - B.BVAshr _ x y -> fmap SAWExpr $ do - let w = natValue (bvWidth x) - -- NB: bvSShr applies a `Succ` to its width argument, so we subtract - -- 1 here to make things match up. - n <- SC.scNat sc (w - 1) - join (SC.scBvSShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) - B.BVRol w x y -> fmap SAWExpr $ do - n <- SC.scNat sc (natValue w) - bit <- SC.scBoolType sc - x' <- f env x - y' <- SC.scBvToNat sc (natValue w) =<< f env y - SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateL") [n,bit,x',y'] - B.BVRor w x y -> fmap SAWExpr $ do - n <- SC.scNat sc (natValue w) - bit <- SC.scBoolType sc - x' <- f env x - y' <- SC.scBvToNat sc (natValue w) =<< f env y - SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateR") [n,bit,x',y'] - B.BVConcat _ x y -> fmap SAWExpr $ do - n <- SC.scNat sc (natValue (bvWidth x)) - m <- SC.scNat sc (natValue (bvWidth y)) - t <- SC.scBoolType sc - join (SC.scAppend sc t n m <$> f env x <*> f env y) - B.BVSelect start num x -> fmap SAWExpr $ do - i <- SC.scNat sc (natValue (bvWidth x) - natValue num - natValue start) - n <- SC.scNat sc (natValue num) - o <- SC.scNat sc (natValue start) - t <- SC.scBoolType sc - x' <- f env x - SC.scSlice sc t i n o x' - B.BVZext w' x -> fmap SAWExpr $ do - let w = bvWidth x - n <- SC.scNat sc (natValue w) - m <- SC.scNat sc (natValue w' - natValue w) - x' <- f env x - SC.scBvUExt sc m n x' - B.BVSext w' x -> fmap SAWExpr $ do - let w = bvWidth x - -- NB: width - 1 to make SAWCore types work out - n <- SC.scNat sc (natValue w - 1) - m <- SC.scNat sc (natValue w' - natValue w) - x' <- f env x - SC.scBvSExt sc m n x' - B.BVPopcount w x -> - do n <- SC.scNat sc (natValue w) - x' <- f env x - SAWExpr <$> SC.scBvPopcount sc n x' - B.BVCountLeadingZeros w x -> - do n <- SC.scNat sc (natValue w) - x' <- f env x - SAWExpr <$> SC.scBvCountLeadingZeros sc n x' - B.BVCountTrailingZeros w x -> - do n <- SC.scNat sc (natValue w) - x' <- f env x - SAWExpr <$> SC.scBvCountTrailingZeros sc n x' - - -- Note: SAWCore supports only unidimensional arrays. As a result, What4 multidimensional - -- arrays cannot be translated to SAWCore. - B.ArrayMap indexTypes range updates arr - | Ctx.Empty Ctx.:> idx_type <- indexTypes -> - do sc_idx_type <- baseSCType sym sc idx_type - sc_elm_type <- baseSCType sym sc range - sc_arr <- f env arr - SAWExpr <$> foldM - (\sc_acc_arr (Ctx.Empty Ctx.:> idx_lit, elm) -> - do sc_idx <- f env =<< indexLit sym idx_lit - sc_elm <- f env elm - SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_acc_arr sc_idx sc_elm) - sc_arr - (AUM.toList updates) - | otherwise -> unimplemented "multidimensional ArrayMap" - - B.ConstantArray indexTypes range v - | Ctx.Empty Ctx.:> idx_type <- indexTypes -> - do sc_idx_type <- baseSCType sym sc idx_type - sc_elm_type <- baseSCType sym sc range - sc_elm <- f env v - SAWExpr <$> SC.scArrayConstant sc sc_idx_type sc_elm_type sc_elm - | otherwise -> unimplemented "multidimensional ConstantArray" - - B.SelectArray range arr indexTerms - | Ctx.Empty Ctx.:> idx <- indexTerms - , idx_type <- exprType idx -> - do sc_idx_type <- baseSCType sym sc idx_type - sc_elm_type <- baseSCType sym sc range - sc_arr <- f env arr - sc_idx <- f env idx - SAWExpr <$> SC.scArrayLookup sc sc_idx_type sc_elm_type sc_arr sc_idx - | otherwise -> unimplemented "multidimensional SelectArray" - - B.UpdateArray range indexTypes arr indexTerms v - | Ctx.Empty Ctx.:> idx_type <- indexTypes - , Ctx.Empty Ctx.:> idx <- indexTerms -> - do sc_idx_type <- baseSCType sym sc idx_type - sc_elm_type <- baseSCType sym sc range - sc_arr <- f env arr - sc_idx <- f env idx - sc_elm <- f env v - SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm - | otherwise -> unimplemented "multidimensional UpdateArray" - - B.CopyArray w a_repr dest_arr dest_idx src_arr src_idx len -> - do sc_w <- SC.scNat sc (natValue w) - sc_a <- baseSCType sym sc a_repr - sc_dest_arr <- f env dest_arr - sc_dest_idx <- f env dest_idx - sc_src_arr <- f env src_arr - sc_src_idx <- f env src_idx - sc_len <- f env len - SAWExpr <$> SC.scArrayCopy sc sc_w sc_a sc_dest_arr sc_dest_idx sc_src_arr sc_src_idx sc_len - - B.SetArray w a_repr arr idx val len -> - do sc_w <- SC.scNat sc (natValue w) - sc_a <- baseSCType sym sc a_repr - sc_arr <- f env arr - sc_idx <- f env idx - sc_val <- f env val - sc_len <- f env len - SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len - - B.NatToInteger x -> NatToIntSAWExpr <$> eval env x - B.IntegerToNat x -> - eval env x >>= \case - NatToIntSAWExpr z -> return z - SAWExpr z -> SAWExpr <$> (SC.scIntToNat sc z) - - B.NatDiv x y -> - do x' <- f env x - y' <- f env y - SAWExpr <$> SC.scDivNat sc x' y' - - B.NatMod x y -> - do x' <- f env x - y' <- f env y - SAWExpr <$> SC.scModNat sc x' y' - - B.IntDiv x y -> - do x' <- f env x - y' <- f env y - SAWExpr <$> SC.scIntDiv sc x' y' - B.IntMod x y -> - do x' <- f env x - y' <- f env y - SAWExpr <$> SC.scIntMod sc x' y' - B.IntAbs x -> - eval env x >>= \case - NatToIntSAWExpr z -> return (NatToIntSAWExpr z) - SAWExpr z -> SAWExpr <$> (SC.scIntAbs sc z) - - B.IntDivisible x 0 -> - do x' <- f env x - SAWExpr <$> (SC.scIntEq sc x' =<< SC.scIntegerConst sc 0) - B.IntDivisible x k -> - do x' <- f env x - k' <- SC.scIntegerConst sc (toInteger k) - z <- SC.scIntMod sc x' k' - SAWExpr <$> (SC.scIntEq sc z =<< SC.scIntegerConst sc 0) - - B.BVToNat x -> - let n = natValue (bvWidth x) in - SAWExpr <$> (SC.scBvToNat sc n =<< f env x) - - B.IntegerToBV x w -> - do n <- SC.scNat sc (natValue w) - SAWExpr <$> (SC.scIntToBv sc n =<< f env x) - - B.BVToInteger x -> - do n <- SC.scNat sc (natValue (bvWidth x)) - SAWExpr <$> (SC.scBvToInt sc n =<< f env x) - - B.SBVToInteger x -> - do n <- SC.scNat sc (natValue (bvWidth x)) - SAWExpr <$> (SC.scSbvToInt sc n =<< f env x) - - -- Proper support for real and complex numbers will require additional - -- work on the SAWCore side - B.IntegerToReal x -> IntToRealSAWExpr . SAWExpr <$> f env x - B.RealToInteger x -> - eval env x >>= \case - IntToRealSAWExpr x' -> return x' - _ -> realFail - - ------------------------------------------------------------------------ - -- Floating point operations - - B.FloatPZero{} -> floatFail - B.FloatNZero{} -> floatFail - B.FloatNaN{} -> floatFail - B.FloatPInf{} -> floatFail - B.FloatNInf{} -> floatFail - B.FloatNeg{} -> floatFail - B.FloatAbs{} -> floatFail - B.FloatSqrt{} -> floatFail - B.FloatAdd{} -> floatFail - B.FloatSub{} -> floatFail - B.FloatMul{} -> floatFail - B.FloatDiv{} -> floatFail - B.FloatRem{} -> floatFail - B.FloatMin{} -> floatFail - B.FloatMax{} -> floatFail - B.FloatFMA{} -> floatFail - B.FloatFpEq{} -> floatFail - B.FloatFpNe{} -> floatFail - B.FloatLe{} -> floatFail - B.FloatLt{} -> floatFail - B.FloatIsNaN{} -> floatFail - B.FloatIsInf{} -> floatFail - B.FloatIsZero{} -> floatFail - B.FloatIsPos{} -> floatFail - B.FloatIsNeg{} -> floatFail - B.FloatIsSubnorm{} -> floatFail - B.FloatIsNorm{} -> floatFail - B.FloatCast{} -> floatFail - B.FloatRound{} -> floatFail - B.FloatFromBinary{} -> floatFail - B.BVToFloat{} -> floatFail - B.SBVToFloat{} -> floatFail - B.RealToFloat{} -> floatFail - B.FloatToBV{} -> floatFail - B.FloatToSBV{} -> floatFail - B.FloatToReal{} -> floatFail - B.FloatToBinary{} -> floatFail - - B.RoundReal{} -> realFail - B.RoundEvenReal{} -> realFail - B.FloorReal{} -> realFail - B.CeilReal{} -> realFail - B.RealDiv{} -> realFail - B.RealSqrt{} -> realFail - B.Pi{} -> realFail - B.RealSin{} -> realFail - B.RealCos{} -> realFail - B.RealSinh{} -> realFail - B.RealCosh{} -> realFail - B.RealExp{} -> realFail - B.RealLog{} -> realFail - B.RealATan2{} -> realFail - - B.Cplx{} -> cplxFail - B.RealPart{} -> cplxFail - B.ImagPart{} -> cplxFail - - B.StringLength{} -> stringFail - B.StringAppend{} -> stringFail - B.StringContains{} -> stringFail - B.StringIsPrefixOf{} -> stringFail - B.StringIsSuffixOf{} -> stringFail - B.StringIndexOf{} -> stringFail - B.StringSubstring{} -> stringFail - - B.StructCtor{} -> nyi -- FIXME - B.StructField{} -> nyi -- FIXME - - -- returns the logical negation of the result of 'go' - -- negations are pushed inside conjunctions and less-than-or-equal - goNeg :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) - goNeg env expr = - case expr of - -- negation of (x /\ y) becomes (~x \/ ~y) - B.AppExpr (B.appExprApp -> B.ConjPred xs) -> - case BM.viewBoolMap xs of - BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False - BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True - BM.BoolMapTerms (t:|ts) -> - let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x - pol (x, BM.Negative) = f env x - in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts) - _ -> goNegAtom env expr - - -- returns the logical negation of the result of 'go' - -- negations are pushed inside less-than-or-equal - goNegAtom :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) - goNegAtom env expr = - case expr of - -- negation of (x <= y) becomes (y < x) - B.AppExpr (B.appExprApp -> B.SemiRingLe sr xe ye) -> - case sr of - B.OrderedSemiRingRealRepr -> join (scRealLt sym sc <$> eval env ye <*> eval env xe) - B.OrderedSemiRingIntegerRepr -> join (scIntLt sc <$> eval env ye <*> eval env xe) - B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) - _ -> SAWExpr <$> (SC.scNot sc =<< f env expr) - -withSolverProcess :: - OnlineSolver solver => - SAWCoreBackend scope solver fs -> - IO a -> - (SolverProcess scope solver -> IO a) -> - IO a -withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) - -withSolverConn :: - OnlineSolver solver => - SAWCoreBackend scope solver fs -> - (WriterConn scope solver -> IO ()) -> - IO () -withSolverConn sym k = withSolverProcess sym (pure ()) (k . solverConn) - - -getAssumptionStack :: - SAWCoreBackend s solver fs -> - IO (AssumptionStack (B.BoolExpr s) AssumptionReason SimError) -getAssumptionStack sym = - (assumptionStack . saw_online_state) <$> readIORef (B.sbStateManager sym) - - --- TODO! we should find a better way to share implementations with `OnlineBackend` -instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where - - addDurableProofObligation sym a = - AS.addProofObligation a =<< getAssumptionStack sym - - addAssumption sym a = - let cond = asConstantPred (a^.labeledPred) - in case cond of - Just False -> abortExecBecause (AssumedFalse (a^.labeledPredMsg)) - _ -> -- Send assertion to the solver, unless it is trivial. - -- NB, don't add the assumption to the assumption stack unless - -- the solver assumptions succeeded - do withSolverConn sym $ \conn -> - case cond of - Just True -> return () - _ -> SMT.assume conn (a^.labeledPred) - - -- Record assumption, even if trivial. - -- This allows us to keep track of the full path we are on. - AS.assume a =<< getAssumptionStack sym - - addAssumptions sym a = - -- NB, don't add the assumption to the assumption stack unless - -- the solver assumptions succeeded - do withSolverConn sym $ \conn -> - -- Tell the solver of assertions - mapM_ (SMT.assume conn . view labeledPred) (toList a) - -- Add assertions to list - stk <- getAssumptionStack sym - AS.appendAssumptions a stk - - getPathCondition sym = - do stk <- getAssumptionStack sym - ps <- AS.collectAssumptions stk - andAllOf sym (folded.labeledPred) ps - - collectAssumptions sym = - AS.collectAssumptions =<< getAssumptionStack sym - - pushAssumptionFrame sym = - do -- NB, don't push a frame in the assumption stack unless - -- pushing to the solver succeeded - withSolverProcess sym (pure ()) push - AS.pushFrame =<< getAssumptionStack sym - - popAssumptionFrame sym ident = - -- NB, pop the frame whether or not the solver pop succeeds - do frm <- AS.popFrame ident =<< getAssumptionStack sym - withSolverProcess sym (pure ()) pop - return frm - - popUntilAssumptionFrame sym ident = - -- NB, pop the frames whether or not the solver pop succeeds - do n <- AS.popFramesUntil ident =<< getAssumptionStack sym - withSolverProcess sym (pure ()) $ \proc -> - forM_ [0..(n-1)] $ \_ -> pop proc - - popAssumptionFrameAndObligations sym ident = do - -- NB, pop the frames whether or not the solver pop succeeds - do frmAndGls <- AS.popFrameAndGoals ident =<< getAssumptionStack sym - withSolverProcess sym (pure ()) pop - return frmAndGls - - getProofObligations sym = - do stk <- getAssumptionStack sym - AS.getProofObligations stk - - clearProofObligations sym = - do stk <- getAssumptionStack sym - AS.clearProofObligations stk - - saveAssumptionState sym = - do stk <- getAssumptionStack sym - AS.saveAssumptionStack stk - - restoreAssumptionState sym gc = - do st <- saw_online_state <$> readIORef (B.sbStateManager sym) - restoreSolverState gc st - - -- restore the previous assumption stack - stk <- getAssumptionStack sym - AS.restoreAssumptionStack gc stk diff --git a/crucible-saw/src/Lang/Crucible/Solver/ExtractSAWCore.hs b/crucible-saw/src/Lang/Crucible/Solver/ExtractSAWCore.hs deleted file mode 100644 index 9feae1887..000000000 --- a/crucible-saw/src/Lang/Crucible/Solver/ExtractSAWCore.hs +++ /dev/null @@ -1,495 +0,0 @@ ------------------------------------------------------------------------ --- | --- Module : Lang.Crucible.Solver.ExtractSAWCore --- Copyright : (c) Galois, Inc 2014-2016 --- Maintainer : Rob Dockins --- Stability : provisional --- License : BSD3 --- --- Some experimental, and currently bitrotted code for extracting --- recursive functional representations from Crucible programs. ------------------------------------------------------------------------- - -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE DoAndIfThenElse #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE RankNTypes #-} - - -module Lang.Crucible.Solver.ExtractSAWCore where - -import Control.Monad.ST -import qualified Data.Text as Text -import qualified Data.Set as Set -import qualified Data.Map as Map -import Control.Monad.IO.Class -import Control.Lens -import Control.Monad -import qualified Data.Vector as V -import Control.Monad.Writer -import Data.IORef - -import Prettyprinter - -import qualified Lang.MATLAB.MultiDimArray as MDA -import qualified Text.LLVM.AST as L - -import Data.Parameterized.TraversableFC -import qualified Data.Parameterized.Context as Ctx - -import Lang.Crucible.Analysis.DFS -import Lang.Crucible.Analysis.Shape -import Lang.Crucible.Analysis.ForwardDataflow -import Lang.Crucible.Core -import Lang.Crucible.FunctionHandle -import Lang.Crucible.Simulator.ExecutionTree -import Lang.Crucible.Simulator.MSSim -import Lang.Crucible.Solver.PartExpr -import Lang.Crucible.Solver.Interface -import Lang.Crucible.Analysis.Postdom -import Lang.Crucible.FunctionName( functionNameFromText ) -import Lang.Crucible.ProgramLoc -import Lang.Crucible.Simulator.RegMap -import Lang.Crucible.Simulator.CallFns - -import qualified Lang.Crucible.Solver.SAWCoreBackend as SAW -import qualified Verifier.SAW.SharedTerm as SC -import qualified Verifier.SAW.Rewriter as SC -import qualified Verifier.SAW.TypedAST as SC -import qualified Verifier.SAW.ExternalFormat as SC ---import qualified Verifier.SAW.Prelude.Constants as SC -import Lang.Crucible.LLVM.Translation - - -data RedirectInfo s (ret :: CrucibleType) (init :: Ctx CrucibleType) - = NoRedirectInfo - | RedirectInfo - String - (Lang.Crucible.FunctionHandle.FnHandle init ret) - (SC.ExtCns (SC.SharedTerm s)) - (Override (SAW.SAWCoreBackend s) init ret) - (Ctx.Assignment ShapeDom init) - -findSymbolicBackEdges - :: ModuleTranslation - -> String - -> (forall blocks init ret - . CFG blocks init ret - -> Ctx.Assignment (KildallPair (Ctx.Assignment ShapeDom) SymDom) blocks - -> Set.Set (Some (BlockID blocks)) - -> a) - -> a -findSymbolicBackEdges mt nm k = - -- FIXME, this is all pretty bogus... - let f :: TypeRepr tp -> ShapeDom tp - f (BVRepr _) = SymbolicShape - f (BoolRepr) = LitShape True - f (StructRepr ctx) = StructShape $ Ctx.generate (Ctx.size ctx) $ \i -> f (ctx Ctx.! i) - f _ = ConcreteShape - - in case Map.lookup (L.Symbol nm) (cfgMap mt) of - Nothing -> error $ unwords ["symbol", nm, "not found"] - Just (AnyCFG (cfg :: CFG blocks init ret)) -> - let begin = Ctx.generate (Ctx.size (cfgArgTypes cfg)) (\i -> f (cfgArgTypes cfg Ctx.! i)) - (asgn, _r, _rc) = kildall_forward shapeAnalysis cfg (begin, Concrete) - bkset = dfs_backedge_targets cfg - - isSymbolicBlock :: Some (BlockID blocks) -> Bool - isSymbolicBlock (Some (BlockID bid)) = - case asgn Ctx.! bid of - KP _ Symbolic -> True - _ -> False - - in k cfg asgn $ Set.filter isSymbolicBlock bkset - - -------------------------------------- - -{- -llvmShapeResults - :: ModuleTranslation - -> String -llvmShapeResults mt = - let nm = "factorial" -- "main" -- - f :: TypeRepr tp -> ShapeDom tp - f (BVRepr _) = SymbolicShape - f (BoolRepr) = LitShape True - f (StructRepr ctx) = StructShape $ ctxReprGenerate ctx $ \_i tp -> f tp - f _ = ConcreteShape - - in case Map.lookup (L.Symbol nm) (cfgMap mt) of - Nothing -> error $ unwords ["symbol", nm, "not found"] - Just (AnyCFG cfg) -> - shapeResults (ctxReprGenerate (cfgArgTypes cfg) (\_ tp -> f tp)) cfg --} - - -doExtractSAWCore - :: HandleAllocator RealWorld - -> SAW.SAWCoreBackend s - -> (MSSim (SAW.SAWCoreBackend s) () (OverrideLang EmptyCtx UnitType) EmptyCtx () -> IO (SimResult (SAW.SAWCoreBackend s) ())) - -> ModuleTranslation - -> String - -> IO () -doExtractSAWCore halloc sym runOverride mt fnname = do - -- we use this IORef to "leak" some additional information from the following "run" call, - -- which has a constrained type that makes it difficult to pass this information out otherwise - defRef <- newIORef Nothing - - rr <- runOverride $ do - -- Build a crucible CFG for the given LLVM function. Compute - -- the shape analysis for the given function and find which - -- control-flow edges in the graph are back-edges under the - -- influence of a symbolic branch. - findSymbolicBackEdges mt fnname $ \(cfg :: CFG blocks init ret) shapes bk -> do - - -- Allocate new Crucible handles and SAW external constants to stand in for the - -- symbolic back-edge targets. Also build a crucible override function that - -- constructs a SAWCore term corresponding to a recursive call. Save all the - -- relevant information in a RedirectInfo. - redirInfo <- Ctx.generateM (Ctx.size (cfgBlockMap cfg)) (\i -> do - if Set.member (Some (BlockID i)) bk - then do let nm = fnname ++ "_" ++ show (Ctx.indexVal i) - h <- liftIO $ stToIO $ mkHandle' halloc (functionNameFromText $ Text.pack nm) - (blockInputs (cfgBlockMap cfg Ctx.! i)) - (cfgReturnType cfg) - let (KP shape _) = shapes Ctx.! i - (ec, ovr) <- liftIO $ buildSAWInterface sym nm - (blockInputs (cfgBlockMap cfg Ctx.! i)) - (cfgReturnType cfg) - shape - return $ RedirectInfo nm h ec ovr shape - else return NoRedirectInfo) - - -- Build a new block map where those basic blocks that are the target of symbolic - -- back edges are replaced by tail calls to the new functions we just allocated - let blockMap' = Ctx.generate (Ctx.size (cfgBlockMap cfg)) (\i -> - let block = (cfgBlockMap cfg) Ctx.! i in - case redirInfo Ctx.! i of - NoRedirectInfo -> block - RedirectInfo nm h _ _ _ -> - Block (BlockID i) - (blockInputs block) - (ConsStmt (mkProgramLoc (functionNameFromText $ Text.pack nm) InternalPos) - (SetReg (handleType h) (App (HandleLit h))) - (TermStmt (mkProgramLoc (functionNameFromText $ Text.pack nm) InternalPos) - (TailCall (Reg (Ctx.nextIndex (Ctx.size (blockInputs block)))) - (blockInputs block) - (Ctx.generate (Ctx.size (blockInputs block)) - (\idx -> Reg (Ctx.skip idx))) - ))) - Ctx.noDiff - Nothing) - - -- populate the simulator's handleMap with our custom overrides - sequence_ [ - do let RedirectInfo _nm h _ex ovr _shape = redirInfo Ctx.! i - stateContext . functionBindings %= insertHandleMap h (UseOverride ovr) - | Some (BlockID i) <- Set.toList bk - ] - - -- For each branch of the reclet we want to build, symbolically simulate from - -- the the beginning of related basic block with symbolic arguments. - (branches :: [(SC.ExtCns (SC.SharedTerm s), SC.SharedTerm s)]) <- sequence [ - do let block = (cfgBlockMap cfg) Ctx.! i - let RedirectInfo _nm h ex _ovr shape = redirInfo Ctx.! i - let freshId = BlockID $ Ctx.nextIndex (Ctx.size blockMap') - let block' = Block freshId - (blockInputs block) - (blockStmts block) - (Ctx.extendRight Ctx.noDiff) - Nothing - let bm' = Ctx.extend (extendBlockMap blockMap') block' - let branch_cfg = fillPostdomFields $ CFG h bm' freshId - - (args,sawECs) <- liftIO $ buildBranchArgs sym (blockInputs block) shape - - out <- callCFG branch_cfg args - v <- liftIO $ sawMarshalValue sym (cfgReturnType cfg) out - def <- liftIO $ SC.scAbstractExts (SAW.saw_ctx sym) sawECs v - return (ex, def) - - | Some (BlockID i) <- Set.toList bk - ] - - -- Simulate from the original function entry point to build the body of the reclet. - let (KP mainshape _) = shapes Ctx.! (blockIDIndex (cfgEntryBlockID cfg)) - (mainArgs,mainSawECs) <- liftIO $ buildBranchArgs sym (cfgArgTypes cfg) mainshape - let maincfg = fillPostdomFields $ cfg{ cfgBlockMap = blockMap' } - out <- callCFG maincfg mainArgs - - -- Now stitch the pieces togeter to get the final SAWCore definition. - liftIO $ do - body <- sawMarshalValue sym (cfgReturnType cfg) out - def <- scReclet (SAW.saw_ctx sym) branches body - def' <- simplifySAW (SAW.saw_ctx sym) def - def'' <- SC.scAbstractExts (SAW.saw_ctx sym) mainSawECs def' - writeIORef defRef (Just def'') - - -- We are done inside the simulator - return () - - putStrLn "" - case rr of - FinishedExecution _ (TotalRes _) -> do - Just v <- readIORef defRef - -- putStrLn $ SC.scPrettyTerm v - putStrLn $ SC.scWriteExternal v - - _ -> putStrLn "Execution failed!" - -simplifySAW - :: SC.SharedContext s - -> SC.SharedTerm s - -> IO (SC.SharedTerm s) -simplifySAW s t = do - rs <- tupleRules s - let simpset = SC.addRules rs SC.emptySimpset - -- putStrLn $ show simpset - SC.rewriteSharedTerm s simpset t - -tupleRules - :: SC.SharedContext s - -> IO [SC.RewriteRule (SC.SharedTerm s)] -tupleRules _sc = return [] -{- -tupleRules sc = do -{- - r <- SC.scEqRewriteRule sc (SC.mkIdent SC.preludeModuleName "tuple2_eta") - return [r] --} - srt <- SC.scSort sc (SC.mkSort 0) - ty1 <- SC.scLocalVar sc 1 - ty2 <- SC.scLocalVar sc 0 - tty <- SC.scTupleType sc [ty1, ty2] - x <- SC.scLocalVar sc 0 - x0 <- SC.scTupleSelector sc x 1 - x1 <- SC.scTupleSelector sc x 2 - x' <- SC.scTuple sc [x0,x1] - let ctx = [srt, srt, tty] - let r2 = SC.mkRewriteRule ctx x' x - return [r2] --} - -scReclet - :: SC.SharedContext s - -> [(SC.ExtCns (SC.SharedTerm s), SC.SharedTerm s)] - -> SC.SharedTerm s - -> IO (SC.SharedTerm s) -scReclet _sc [] body = return body -scReclet sc [(ec,def)] body = - do def' <- SC.scAbstractExts sc [ec] def - fx <- SC.scGlobalApply sc "Cryptol.fix" [SC.ecType ec, def'] - SC.scInstantiateExt sc (Map.singleton (SC.ecVarIndex ec) fx) body -scReclet _sc _xs _body = error "FIXME mutual reclet..." - - -newtype MoF m f a = MoF { unMoF :: m (f a) } - -buildBranchArgs :: forall s args - . SAW.SAWCoreBackend s - -> CtxRepr args - -> Ctx.Assignment ShapeDom args - -> IO (RegMap (SAW.SAWCoreBackend s) args, [SC.ExtCns (SC.SharedTerm s)]) -buildBranchArgs sym args shape = do - let mp :: Ctx.Assignment (MoF (WriterT [SC.ExtCns (SC.SharedTerm s)] IO) (RegEntry (SAW.SAWCoreBackend s))) args - mp = Ctx.generate (Ctx.size args) (\i -> MoF $ do - let tp = args Ctx.! i - cty <- liftIO $ crucibleToSawType sym tp (shape Ctx.! i) - var <- liftIO $ SC.scFreshGlobalVar (SAW.saw_ctx sym) - let ec = SC.EC var ("arg_"++(show $ Ctx.indexVal i)) cty - tell [ec] - v <- liftIO (sawUnmarshalValue sym tp =<< SC.scFlatTermF (SAW.saw_ctx sym) (SC.ExtCns ec)) - return (RegEntry tp v)) - - (mp',ecs) <- runWriterT $ traverseFC unMoF mp - return (RegMap mp', ecs) - -buildSAWInterface - :: SAW.SAWCoreBackend s - -> String - -> CtxRepr args - -> TypeRepr ret - -> Ctx.Assignment ShapeDom args - -> IO (SC.ExtCns (SC.SharedTerm s), Override (SAW.SAWCoreBackend s) args ret) -buildSAWInterface sym nm args ret shape = do - sawGlobal <- SC.scFreshGlobalVar (SAW.saw_ctx sym) - sc_ty <- crucibleSigToSawType sym args ret shape - let ec = SC.EC sawGlobal nm sc_ty - return (ec - , Override - (functionNameFromText $ Text.pack nm) - (sawInterfaceOverrideHandler sym args ret shape ec) - ) - - -sawInterfaceOverrideHandler :: forall s args ret rtp - . SAW.SAWCoreBackend s - -> CtxRepr args - -> TypeRepr ret - -> Ctx.Assignment ShapeDom args - -> SC.ExtCns (SC.SharedTerm s) - -> MSS_State (SAW.SAWCoreBackend s) rtp (OverrideLang args ret) EmptyCtx - -> IO (SimResult (SAW.SAWCoreBackend s) rtp) -sawInterfaceOverrideHandler sym args ret _shape ex mss_state = do - base <- SC.scFlatTermF (SAW.saw_ctx sym) $ SC.ExtCns ex - tm <- go args base - v <- sawUnmarshalValue sym ret tm - returnValue mss_state v - - where go :: CtxRepr args - -> SC.SharedTerm s - -> IO (SC.SharedTerm s) - go ctx base = foldlFC fld (return base) $ Ctx.generate (Ctx.size ctx) (\i -> mkArg i (ctx Ctx.! i)) - - fld :: IO (SC.SharedTerm s) - -> Ignore (IO (SC.SharedTerm s)) tp - -> IO (SC.SharedTerm s) - fld base (Ignore x) = join $ pure (SC.scApply (SAW.saw_ctx sym)) <*> base <*> x - - mkArg :: Ctx.Index args tp - -> TypeRepr tp - -> Ignore (IO (SC.SharedTerm s)) tp - mkArg i tp = Ignore $ do - let mp = overrideRegMap $ mss_state ^. stateOverrideFrame - let arg = regVal mp (Reg i) - sawMarshalValue sym tp arg - -sawUnmarshalValue - :: SAW.SAWCoreBackend s - -> TypeRepr tp - -> SC.SharedTerm s - -> IO (RegValue (SAW.SAWCoreBackend s) tp) -sawUnmarshalValue sym tpr tm = - case tpr of - BVRepr w | Just LeqProof <- isPosNat w -> return $ SAW.SC (BaseBVRepr w) tm - NatRepr -> return $ SAW.SC baseTypeRepr tm - BoolRepr -> return $ SAW.SC baseTypeRepr tm - -- NB: structures with exactly one element are treated as a special case - StructRepr ctx - | Ctx.AssignExtend ctx' tp <- Ctx.view ctx - , Ctx.AssignEmpty <- Ctx.view ctx' -> do - x <- sawUnmarshalValue sym tp tm - return $ Ctx.extend Ctx.empty $ RV $ x - StructRepr ctx -> - Ctx.generateM (Ctx.size ctx) $ \idx -> do - let tp = ctx Ctx.! idx - -- NB: SAWCore tuple selectors are 1-based! - tm' <- SC.scTupleSelector (SAW.saw_ctx sym) tm (Ctx.indexVal idx + 1) - RV <$> sawUnmarshalValue sym tp tm' - _ -> fail $ unwords ["Crucible type cannot be mapped onto a SAW type:", show tpr] - -sawMarshalValue - :: SAW.SAWCoreBackend s - -> TypeRepr tp - -> RegValue (SAW.SAWCoreBackend s) tp - -> IO (SC.SharedTerm s) -sawMarshalValue sym tpr expr = - case tpr of - BVRepr _w -> SAW.toSC sym expr - NatRepr -> SAW.toSC sym expr - BoolRepr -> SAW.toSC sym expr - -- NB: structures with exactly one element are treated as a special case - StructRepr ctx - | Ctx.AssignExtend ctx' tp <- Ctx.view ctx - , Ctx.AssignEmpty <- Ctx.view ctx' -> - sawMarshalValue sym tp (unRV $ expr Ctx.! Ctx.base) - StructRepr ctx -> do - xs <- toListFC ignoreOut <$> - Ctx.zipWithM (\tp ex -> Ignore <$> sawMarshalValue sym tp (unRV ex)) ctx expr - SC.scTuple (SAW.saw_ctx sym) xs - _ -> fail $ unwords ["Crucible type cannot be mapped onto a SAW type:", show tpr] - - -crucibleSigToSawType - :: forall s args tp - . SAW.SAWCoreBackend s - -> CtxRepr args - -> TypeRepr tp - -> Ctx.Assignment ShapeDom args - -> IO (SC.SharedTerm s) -crucibleSigToSawType sym args ret shape = do - xs <- Ctx.generateM (Ctx.size args) (\i -> - Ignore <$> crucibleToSawType sym (args Ctx.! i) (shape Ctx.! i)) - ret' <- crucibleToSawType sym ret SymbolicShape - foldrFC (\(Ignore t) m -> m >>= SC.scFun (SAW.saw_ctx sym) t) (return ret') xs - -{- -crucibleSigToSawType sym args ret shape = go args =<< crucibleToSawType sym ret - where go :: CtxRepr tps -> SC.SharedTerm s -> IO (SC.SharedTerm s) - go EmptyCtxRepr tp = return tp - go (ConsCtxRepr ctx x) shs tp = do - x' <- crucibleToSawType sym x - tp' <- SC.scFun (SAW.saw_ctx sym) x' tp - go ctx tp' --} - -crucibleToSawType :: forall s tp - . SAW.SAWCoreBackend s - -> TypeRepr tp - -> ShapeDom tp - -> IO (SC.SharedTerm s) -crucibleToSawType sym tp sh = - let sc = SAW.saw_ctx sym in - case tp of - BVRepr w -> SC.scBitvector sc (fromIntegral (widthVal w)) - NatRepr -> SC.scNatType sc - BoolRepr -> SC.scBoolType sc - StructRepr ctx -> do - xs <- Ctx.generateM (Ctx.size ctx) (\i -> do - let tp' = ctx Ctx.! i - let sh' = case sh of - StructShape ss -> ss Ctx.! i - ConcreteShape -> ConcreteShape - _ -> SymbolicShape - Ignore <$> crucibleToSawType sym tp' sh') - let xs' = toListFC ignoreOut xs - case xs' of - -- NB: structures with exactly one element are treated as a special case - [x] -> return x - _ -> SC.scTupleType sc xs' - -{- - StructRepr ctx -> go ctx [] - where go :: CtxRepr ctx -> [SC.SharedTerm s] -> IO (SC.SharedTerm s) - go EmptyCtxRepr [] = SC.scTupleType sc [] - -- NB: structures with exactly one element are treated as a special case - go EmptyCtxRepr [x] = return x - go EmptyCtxRepr xs = SC.scTupleType sc xs - go (ConsCtxRepr c t) xs = do - t' <- crucibleToSawType sym t (error "FIXME") - go c (t':xs) --} - - _ -> fail $ unwords ["Crucible type cannot be mapped ont a SAW type:", show tp] - - -printSAWValues - :: forall s - . SAW.SAWCoreBackend s - -> V.Vector (PartExpr (Pred (SAW.SAWCoreBackend s)) (Value (SAW.SAWCoreBackend s))) - -> IO () -printSAWValues sc = V.ifoldl' (\m i x -> m >> printPart i x) (return ()) - where printPart i Unassigned = putStrLn $ unlines [ "Result "++show i, " UNASSIGNED",""] - printPart i (PE _ v) = printVal i v >>= print - - printVal :: Int -> Value (SAW.SAWCoreBackend s) -> IO Doc - printVal i (UIntArray (SomeBVArray _ a)) = do - a' <- traverse (ppSAWCore sc) a - return $ MDA.ppVector ("Result "++ show i) id a' - - printVal _ (RealArray _) = return $ text "No printing for real arrays" - printVal _ (IntArray _) = return $ text "No printing for int arrays" - printVal _ (CharArray _) = return $ text "No printing for char arrays" - printVal _ (LogicArray _) = return $ text "No printing for bool arrays" - printVal _ (CellArray _) = return $ text "No printing for cell arrays" - printVal _ (MatlabStructArray _) = return $ text "No printing for struct arrays" - printVal _ (FunctionHandle _) = return $ text "No printing for function handles" - printVal _ (SymLogicArray _) = return $ text "No printing for symbolic logical arrays" - -ppSAWCore :: forall s tp. SAW.SAWCoreBackend s -> SymExpr (SAW.SAWCoreBackend s) tp -> IO String -ppSAWCore sc t = SC.scPrettyTerm <$> SAW.toSC sc t