GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 01:13:34 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into logic-class

Browse Source 
# Conflicts:
#	tests/mono-binds/test05.icry.stdout
This commit is contained in:
Brian Huffman 2017-09-26 16:50:53 -07:00
commit 1ed5640339
22 changed files with 295 additions and 3553 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
cryptol.cabal
View File

@ -76,6 +76,7 @@ library
mtl >= 2.2.1,
time >= 1.6.0.1
Build-tools: alex, happy
hs-source-dirs: src
@ -140,16 +141,8 @@ library
Cryptol.TypeCheck.Solver.Numeric,
Cryptol.TypeCheck.Solver.Improve,
Cryptol.TypeCheck.Solver.CrySAT,
Cryptol.TypeCheck.Solver.Numeric.AST,
Cryptol.TypeCheck.Solver.Numeric.ImportExport,
Cryptol.TypeCheck.Solver.Numeric.Defined,
Cryptol.TypeCheck.Solver.Numeric.Fin,
Cryptol.TypeCheck.Solver.Numeric.Interval,
Cryptol.TypeCheck.Solver.Numeric.Simplify,
Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr,
Cryptol.TypeCheck.Solver.Numeric.NonLin,
Cryptol.TypeCheck.Solver.Numeric.SMT,
Cryptol.Transform.MonoValues,
Cryptol.Transform.Specialize,

17
src/Cryptol/ModuleSystem/Env.hs
View File

@ -84,13 +84,7 @@ initialModuleEnv = do
let handle :: X.IOException -> IO String
handle _e = return ""
userDir <- X.catch (getAppUserDataDirectory "cryptol") handle
return ModuleEnv
{ meLoadedModules = mempty
, meNameSeeds = T.nameSeeds
, meEvalEnv = mempty
, meFocusedModule = Nothing
-- we search these in order, taking the first match
, meSearchPath = [ curDir
let searchPath = [ curDir
-- something like $HOME/.cryptol
, userDir
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
@ -109,12 +103,21 @@ initialModuleEnv = do
, dataDir
#endif
]
return ModuleEnv
{ meLoadedModules = mempty
, meNameSeeds = T.nameSeeds
, meEvalEnv = mempty
, meFocusedModule = Nothing
-- we search these in order, taking the first match
, meSearchPath = searchPath
, meDynEnv = mempty
, meMonoBinds = True
, meSolverConfig = T.SolverConfig
{ T.solverPath = "z3"
, T.solverArgs = [ "-smt2", "-in" ]
, T.solverVerbose = 0
, T.solverPreludePath = searchPath
}
, meCoreLint = NoCoreLint
, meSupply = emptySupply

12
src/Cryptol/Prelude.hs
View File

@ -16,7 +16,7 @@
module Cryptol.Prelude (
writePreludeContents,
writePreludeExtrasContents,
writeTcPreludeContents,
cryptolTcContents
) where
@ -51,12 +51,4 @@ writePreludeExtrasContents = do
cryptolTcContents :: String
cryptolTcContents = [there|lib/CryptolTC.z3|]
-- | Write the contents of the Prelude to a temporary file so that
-- Cryptol can load the module.
writeTcPreludeContents :: IO FilePath
writeTcPreludeContents = do
tmpdir <- getTemporaryDirectory
(path, h) <- openTempFile tmpdir "CryptolTC.z3"
hPutStr h cryptolTcContents
hClose h
return path

4
src/Cryptol/REPL/Command.hs
View File

@ -70,7 +70,7 @@ import qualified Cryptol.TypeCheck.Parseable as T
import qualified Cryptol.TypeCheck.Subst as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.TypeCheck.Solve(defaultReplExpr)
import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import Cryptol.TypeCheck.PP (dump,ppWithNames)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
@ -964,7 +964,7 @@ replEvalExpr expr =
me <- getModuleEnv
let cfg = M.meSolverConfig me
mbDef <- io $ CrySAT.withSolver cfg (\s -> defaultReplExpr s def sig)
mbDef <- io $ SMT.withSolver cfg (\s -> defaultReplExpr s def sig)
(def1,ty) <-
case mbDef of

27
src/Cryptol/TypeCheck/Infer.hs
View File

@ -27,7 +27,7 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
checkPropSyn,checkNewtype)
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Depends
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),emptySubst)
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@))
import Cryptol.TypeCheck.Solver.InfNat(genLog)
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
@ -686,15 +686,7 @@ generalize bs0 gs0 =
when (not (null ambig)) $ recordError $ AmbiguousType $ map dName bs
solver <- getSolver
(as0,here1,mb_defSu,ws) <- io $ improveByDefaultingWith solver maybeAmbig here0
defSu <- case mb_defSu of
Nothing -> do recordError $ UnsolvedGoals True here0
return emptySubst
Just s -> return s
let (as0,here1,defSu,ws) = improveByDefaultingWithPure maybeAmbig here0
mapM_ recordWarning ws
let here = map goal here1
@ -704,7 +696,7 @@ generalize bs0 gs0 =
totSu <- getSubst
let
su = listSubst (zip as (map (TVar . tpVar) asPs)) @@ defSu @@ totSu
qs = map (apSubst su) here
qs = concatMap (pSplitAnd . apSubst su) here
genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs
genB d = d { dDefinition = case dDefinition d of
@ -798,17 +790,12 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
when (not (null ambig)) $ recordError
$ AmbiguousType [ thing (P.bName b) ]
solver <- getSolver
(_,_,mb_defSu2,ws) <-
io $ improveByDefaultingWith solver maybeAmbig later
defSu2 <- case mb_defSu2 of
Nothing -> do recordError $ UnsolvedGoals True later
return emptySubst
Just s -> return s
-- XXX: Uhm, why are we defaulting that 'later' things here?
-- Surely this should be done later, when we solve them?
let (_,newGs,defSu2,ws) = improveByDefaultingWithPure maybeAmbig later
mapM_ recordWarning ws
extendSubst defSu2
addGoals later
addGoals newGs
su <- getSubst
let su' = defSu1 @@ su

2
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -41,6 +41,8 @@ data SolverConfig = SolverConfig
{ solverPath :: FilePath -- ^ The SMT solver to invoke
, solverArgs :: [String] -- ^ Additional arguments to pass to the solver
, solverVerbose :: Int -- ^ How verbose to be when type-checking
, solverPreludePath :: [FilePath]
-- ^ Look for the solver prelude in these locations.
} deriving (Show, Generic, NFData)
-- | The types of variables in the environment.

23
src/Cryptol/TypeCheck/Monad.hs
View File

@ -19,13 +19,12 @@ module Cryptol.TypeCheck.Monad
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import Cryptol.Prelude (writeTcPreludeContents)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
import Cryptol.TypeCheck.InferTypes
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import Cryptol.Utils.PP(pp, (<+>), Doc, text, quotes)
import Cryptol.Utils.Panic(panic)
@ -42,8 +41,6 @@ import MonadLib hiding (mapM)
import Data.IORef
import System.FilePath((</>))
import System.Directory(doesFileExist)
import GHC.Generics (Generic)
@ -102,9 +99,8 @@ bumpCounter = do RO { .. } <- IM ask
io $ modifyIORef' iSolveCounter (+1)
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
do loadCryTCPrel solver (inpSearchPath info)
coutner <- newIORef 0
runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
do coutner <- newIORef 0
rec ro <- return RO { iRange = inpRange info
, iVars = Map.map ExtVar (inpVars info)
, iTVars = []
@ -168,15 +164,6 @@ runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
-- The actual order does not matter
cmpRange (Range x y z) (Range a b c) = compare (x,y,z) (a,b,c)
loadCryTCPrel s [] =
do file <- writeTcPreludeContents
CrySAT.loadFile s file
loadCryTCPrel s (p : ps) =
do let file = p </> "CryptolTC.z3"
yes <- doesFileExist file
if yes then CrySAT.loadFile s file
else loadCryTCPrel s ps
@ -218,7 +205,7 @@ data RO = RO
-- in where-blocks will never be generalized. Bindings with type
-- signatures, and all bindings at top level are unaffected.
, iSolver :: CrySAT.Solver
, iSolver :: SMT.Solver
, iPrimNames :: !PrimMap
@ -309,7 +296,7 @@ recordWarning w =
do r <- curRange
IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s }
getSolver :: InferM CrySAT.Solver
getSolver :: InferM SMT.Solver
getSolver =
do RO { .. } <- IM ask
return iSolver

242
src/Cryptol/TypeCheck/Solve.hs
View File

@ -13,7 +13,7 @@ module Cryptol.TypeCheck.Solve
, proveImplication
, wfType
, wfTypeFunction
, improveByDefaultingWith
, improveByDefaultingWithPure
, defaultReplExpr
) where
@ -23,34 +23,28 @@ import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst
(apSubst, singleSubst, isEmptySubst, substToList,
emptySubst,Subst,listSubst, (@@), Subst,
apSubstMaybe, substBinds)
substBinds)
import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import Cryptol.TypeCheck.SimpType(tMax)
import Cryptol.TypeCheck.Solver.SMT(proveImp,checkUnsolvable)
import Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,tryGetModel)
import Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
import Cryptol.TypeCheck.Solver.Numeric.Interval
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
import Cryptol.TypeCheck.Solver.CrySAT
import Cryptol.Utils.PP (text,vcat,(<+>))
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Patterns(matchMaybe)
import Control.Monad (guard, mzero)
import Control.Applicative ((<|>))
import Data.Either(partitionEithers)
import Data.Maybe(catMaybes)
import Data.Map ( Map )
import Control.Monad(mzero,guard)
import qualified Data.Map as Map
import Data.Set ( Set )
import qualified Data.Set as Set
{- | Add additional constraints that ensure validity of type function.
Note that these constraints do not introduce additional malformed types,
so the well-formedness constraints are guaranteed to be well-formed.
@ -185,7 +179,7 @@ proveImplication lnam as ps gs =
return su
proveImplicationIO :: Num.Solver
proveImplicationIO :: Solver
-> Name -- ^ Checking this function
-> Set TVar -- ^ These appear in the env., and we should
-- not try to default the
@ -259,49 +253,6 @@ cleanupError err =
simpGoals' :: Num.Solver -> Ctxt -> [Goal] -> IO (Either [Goal] [Goal], Subst)
simpGoals' s asmps gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
where
-- Assumes that the well-formed constraints are themselves well-formed.
wellFormed gs = [ g { goal = p } | g <- gs, p <- wfType (goal g) ]
go su old [] = return (Right old, su)
go su old gs =
do res <- solveConstraints s asmps old gs
case res of
Left err -> return (Left err, su)
Right gs2 ->
do let gs3 = gs2 ++ old
mb <- computeImprovements s gs3
case mb of
Left err -> return (Left err, su)
Right impSu ->
let (unchanged,changed) =
partitionEithers (map (applyImp impSu) gs3)
new = wellFormed changed
in go (impSu @@ su) unchanged (new ++ changed)
applyImp su g = case apSubstMaybe su (goal g) of
Nothing -> Left g
Just p -> Right g { goal = p }
{- Note:
It is good to consider the other goals when evaluating terms.
For example, consider the constraints:
P (x * inf), x >= 1
We cannot simplify `x * inf` on its own, because we do not know if `x`
might be 0. However, in the contxt of `x >= 1`, we know that this is
impossible, and we can simplify the constraints to:
P inf, x >= 1
However, we should be careful to avoid circular reasoning, as we wouldn't
want to use the fact that `x >= 1` to simplify `x >= 1` to true.
-}
@ -314,110 +265,6 @@ assumptionIntervals as ps =
solveConstraints :: Num.Solver ->
Ctxt ->
[Goal] {- We may use these, but don't try to solve,
we already tried and failed. -} ->
[Goal] {- Need to solve these -} ->
IO (Either [Goal] [Goal])
-- ^ Left: contradiciting goals,
-- Right: goals that were not solved, or sub-goals
-- for solved goals. Does not include "old"
solveConstraints s asmps otherGs gs0 =
debugBlock s "Solving constraints" $ go ctxt0 [] gs0
where
ctxt0 = assumptionIntervals asmps (map goal otherGs)
go _ unsolved [] =
do let (cs,nums) = partitionEithers (map Num.numericRight unsolved)
nums' <- solveNumerics s otherNumerics nums
return (Right (cs ++ nums'))
go ctxt unsolved (g : gs) =
case Simplify.simplifyStep ctxt (goal g) of
Unsolvable _x -> return (Left [g]) -- maybe give error?
Unsolved -> go ctxt (g : unsolved) gs
SolvedIf subs ->
let cvt x = g { goal = x }
in go ctxt unsolved (map cvt subs ++ gs)
otherNumerics = [ g | Right g <- map Num.numericRight otherGs ]
solveNumerics :: Num.Solver ->
[(Goal,Num.Prop)] {- ^ Consult these -} ->
[(Goal,Num.Prop)] {- ^ Solve these -} ->
IO [Goal]
solveNumerics _ _ [] = return []
solveNumerics s consultGs solveGs =
Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) consultGs)
Num.simplifyProps s (map Num.knownDefined solveGs)
computeImprovements :: Num.Solver -> [Goal] -> IO (Either [Goal] Subst)
computeImprovements s gs =
debugBlock s "Computing improvements" $
do let nums = [ g | Right g <- map Num.numericRight gs ]
res <- Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) nums)
mb <- Num.check s
case mb of
Nothing -> return Nothing
Just (suish,_ps1) ->
do let (su,_ps2) = importSplitImps suish
-- Num.check has already checked that the intervals are sane,
-- so we don't need to check for a broken interval here
Right ints <- Num.getIntervals s
return (Just (ints,su))
case res of
Just (_ints, su) -> return (Right su) -- ?
{-
| isEmptySubst su
, (x,t) : _ <- mapMaybe (improveByDefn ints) gs ->
do let su' = singleSubst x t
debugLog s ("Improve by definition: " ++ show (pp su'))
return (Right su')
| otherwise -> return (Right su)
-}
Nothing ->
do bad <- Num.minimizeContradictionSimpDef s
(map Num.knownDefined nums)
return (Left bad)
-- | Import an improving substitutin (i.e., a bunch of equations)
-- into a Cryptol substitution (which is idempotent).
-- The substitution will contain only unification variables.
-- "Improvements" on skolem variables become additional constraints.
importSplitImps :: Map Num.Name Num.Expr -> (Subst, [Prop])
importSplitImps = mk . partitionEithers . map imp . Map.toList
where
mk (uni,props) = (listSubst (catMaybes uni), props)
imp (x,e) = case (x, Num.importType e) of
(Num.UserName tv, Just ty) ->
case tv of
TVFree {} -> Left (Just (tv,ty))
TVBound {} -> Right (TVar tv =#= ty)
{- This may happen if we are working on an implication,
and we have an improvement about a variable in the
assumptions that is not in any og the goals.
XXX: Perhaps, we should mark these variable, so we don't waste
time to "improve" them. -}
_ -> Left Nothing
@ -447,47 +294,6 @@ importSplitImps = mk . partitionEithers . map imp . Map.toList
3. a substitution which indicates what got defaulted.
-}
improveByDefaultingWith ::
Num.Solver ->
[TVar] -> -- candidates for defaulting
[Goal] -> -- constraints
IO ( [TVar] -- non-defaulted
, [Goal] -- new constraints
, Maybe Subst -- Nothing: improve to False
-- Just: improvements from defaulting
, [Warning] -- warnings about defaulting
)
-- XXX: Remove this
-- improveByDefaultingWith s as gs = return (as,gs,emptySubst,[])
improveByDefaultingWith s as gs =
do bad <- checkUnsolvable s gs
if bad
then return (as, gs, Nothing, [])
else tryImp
where
tryImp =
case improveByDefaultingWithPure as gs of
(xs,gs',su,ws) ->
do (res,su1) <- simpGoals' s Map.empty gs'
case res of
Left err ->
panic "improveByDefaultingWith"
$ [ "Defaulting resulted in unsolvable constraints."
, "Before:"
] ++ [ " " ++ show (pp (goal g)) | g <- gs ] ++
[ "After:"
] ++ [ " " ++ show (pp (goal g)) | g <- gs' ] ++
[ "Contradiction:" ] ++
[ " " ++ show (pp (goal g)) | g <- err ]
Right gs'' ->
do let su2 = su1 @@ su
isDef x = x `Set.member` substBinds su2
return ( filter (not . isDef) xs
, gs''
, Just su2
, ws
)
improveByDefaultingWithPure :: [TVar] -> [Goal] ->
@ -588,31 +394,19 @@ improveByDefaultingWithPure as ps =
-- | Try to pick a reasonable instantiation for an expression, with
-- the given type. This is useful when we do evaluation at the REPL.
-- The resulting types should satisfy the constraints of the schema.
defaultReplExpr :: Num.Solver -> Expr -> Schema
defaultReplExpr :: Solver -> Expr -> Schema
-> IO (Maybe ([(TParam,Type)], Expr))
-- defaultReplExpr _ _ _ = return Nothing
defaultReplExpr so e s =
defaultReplExpr sol e s =
if all (\v -> kindOf v == KNum) (sVars s)
then do let params = map tpVar (sVars s)
mbSubst <- tryGetModel so params (sProps s)
case mbSubst of
Just su ->
do (res,su1) <- simpGoals' so Map.empty (map (makeGoal su) (sProps s))
return $
case res of
Right [] | isEmptySubst su1 ->
do tys <- mapM (bindParam su) params
props = sProps s
mbSubst <- tryGetModel sol params props
return $ do su <- mbSubst
guard (null (concatMap pSplitAnd (apSubst su props)))
tys <- mapM (bindParam su) params
return (zip (sVars s) tys, appExpr tys)
_ -> Nothing
_ -> return Nothing
else return Nothing
where
makeGoal su p = Goal { goalSource = error "goal source"
, goalRange = error "goal range"
, goal = apSubst su p
}
bindParam su tp =
do let ty = TVar tp
ty' = apSubst su ty
@ -623,15 +417,5 @@ defaultReplExpr so e s =
-- | Attempt to default the given constraints by asserting them in the SMT
-- solver, and asking it for a model.
tryGetModel ::
Num.Solver ->
[TVar] -> -- variables to try defaulting
[Prop] -> -- constraints
IO (Maybe Subst)
tryGetModel s xs ps =
-- We are only interested in finite instantiations
Num.getModel s (map (pFin . TVar) xs ++ ps)

696
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -1,696 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2013-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.TypeCheck.Solver.CrySAT
( withScope, withSolver
, assumeProps, simplifyProps, getModel
, check
, Solver, logger, getIntervals
, DefinedProp(..)
, debugBlock
, DebugLog(..)
, knownDefined, numericRight
, minimizeContradictionSimpDef
, loadFile
, rawSolver
) where
import qualified Cryptol.TypeCheck.AST as Cry
import Cryptol.TypeCheck.InferTypes(Goal(..), SolverConfig(..))
import qualified Cryptol.TypeCheck.Subst as Cry
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.Fin
import Cryptol.TypeCheck.Solver.Numeric.ImportExport
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.TypeCheck.Solver.Numeric.Defined
import Cryptol.TypeCheck.Solver.Numeric.Simplify
import Cryptol.TypeCheck.Solver.Numeric.NonLin
import Cryptol.TypeCheck.Solver.Numeric.SMT
import Cryptol.Utils.PP -- ( Doc )
import Cryptol.Utils.Panic ( panic )
import MonadLib
import Data.Maybe ( fromMaybe )
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Char(isSpace)
import Data.Foldable ( any, all )
import qualified Data.Set as Set
import Data.IORef ( IORef, newIORef, readIORef, modifyIORef',
atomicModifyIORef' )
import Prelude hiding (any,all)
import qualified System.IO.Strict as StrictIO
import qualified SimpleSMT as SMT
-- | We use this to remember what we simplified
newtype SimpProp = SimpProp { unSimpProp :: Prop }
simpProp :: Prop -> SimpProp
simpProp p = SimpProp (crySimplify p)
class HasProp a where getProp :: a -> Cry.Prop
instance HasProp Cry.Prop where getProp = id
instance HasProp Goal where getProp = goal
-- | 'dpSimpProp' and 'dpSimpExprProp' should be logically equivalent,
-- to each other, and to whatever 'a' represents (usually 'a' is a 'Goal').
data DefinedProp a = DefinedProp
{ dpData :: a
-- ^ Optional data to associate with prop.
-- Often, the original `Goal` from which the prop was extracted.
, dpSimpProp :: SimpProp
{- ^ Fully simplified: may mention ORs, and named non-linear terms.
These are what we send to the prover, and we don't attempt to
convert them back into Cryptol types. -}
, dpSimpExprProp :: Prop
{- ^ A version of the proposition where just the expression terms
have been simplified. These should not contain ORs or named non-linear
terms because we want to import them back into Crytpol types. -}
}
knownDefined :: (a,Prop) -> DefinedProp a
knownDefined (a,p) = DefinedProp
{ dpData = a, dpSimpProp = simpProp p, dpSimpExprProp = p }
-- | Class goals go on the left, numeric goals go on the right.
numericRight :: Goal -> Either Goal (Goal, Prop)
numericRight g = case exportProp (goal g) of
Just p -> Right (g, p)
Nothing -> Left g
-- | Simplify a bunch of well-defined properties.
-- * Eliminates properties that are implied by the rest.
-- * Does not modify the set of assumptions.
simplifyProps :: Solver -> [DefinedProp Goal] -> IO [Goal]
simplifyProps s props =
debugBlock s "Simplifying properties" $
withScope s (go [] (eliminateSimpleGEQ props))
where
go survived [] = return survived
go survived (DefinedProp { dpSimpProp = SimpProp PTrue } : more) =
go survived more
go survived (p : more) =
case dpSimpProp p of
SimpProp PTrue -> go survived more
SimpProp p' ->
do mbProved <- withScope s $
do mapM_ (assert s) more
e <- getIntervals s
case e of
Left _ -> return Nothing
Right ints -> do b <- prove s p'
return (Just (ints,b))
case mbProved of
Just (_,True) -> go survived more
Just (ints,False) ->
debugLog s ("Using the fin solver:" ++ show (pp (goal (dpData p)))) >>
case cryIsFin ints (goal (dpData p)) of
SolvedIf ps' ->
do debugLog s "solved"
let gg = dpData p
gs' = [ gg { goal = pr } | pr <- ps' ]
let more' = [ knownDefined g | Right g <- map numericRight gs' ]
go survived (more' ++ more)
Unsolved ->
do debugLog s "unsolved"
assert s p
go (dpData p : survived) more
x@(Unsolvable {}) ->
do debugLog s (show (pp x))
go (dpData p:survived) more
Nothing -> go (dpData p:survived) more
{- | Simplify easy less-than-or-equal-to and equal-to goals.
Those are common with long lists of literals, so we have special handling
for them. In particular:
* Reduce goals of the form @(a >= k1, a >= k2, a >= k3, ...)@ to
@a >= max (k1, k2, k3, ...)@, when all the k's are constant.
* Eliminate goals of the form @ki >= k2@, when @k2@ is leq than @k1@.
* Eliminate goals of the form @a >= 0@.
NOTE: This assumes that the goals are well-defined.
-}
eliminateSimpleGEQ :: [DefinedProp a] -> [DefinedProp a]
eliminateSimpleGEQ = go Map.empty []
where
go geqs other (g : rest) =
case dpSimpExprProp g of
K a :== K b
| a == b -> go geqs other rest
_ :>= K (Nat 0) ->
go geqs other rest
K (Nat k1) :>= K (Nat k2)
| k1 >= k2 -> go geqs other rest
Var v :>= K (Nat k2) ->
go (addUpperBound v (k2,g) geqs) other rest
_ -> go geqs (g:other) rest
go geqs other [] = [ g | (_,g) <- Map.elems geqs ] ++ other
-- add in a possible upper bound for var
addUpperBound var g = Map.insertWith cmp var g
where
cmp a b | fst a > fst b = a
| otherwise = b
-- | Add the given constraints as assumptions.
-- * We assume that the constraints are well-defined.
-- * Modifies the set of assumptions.
assumeProps :: Solver -> [Cry.Prop] -> IO [SimpProp]
assumeProps s props =
do let ps = [ (p,p') | p <- props
, Just p' <- [exportProp p] ]
let defPs = [ (p,cryDefinedProp p') | (p,p') <- ps ]
let simpProps = map knownDefined (defPs ++ ps)
mapM_ (assert s) simpProps
return (map dpSimpProp simpProps)
-- XXX: Instead of asserting one at a time, perhaps we should
-- assert a conjunction. That way, we could simplify the whole thing
-- in one go, and would avoid having to assert 'true' many times.
-- | Given a list of propositions that together lead to a contradiction,
-- find a sub-set that still leads to a contradiction (but is smaller).
minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a]
minimizeContradictionSimpDef s ps = start [] ps
where
start bad todo =
do res <- SMT.check (solver s)
case res of
SMT.Unsat -> return (map dpData bad)
_ -> do solPush s
go bad [] todo
go _ _ [] = panic "minimizeContradiction"
$ ("No contradiction" : map (show . ppProp . dpSimpExprProp) ps)
go bad prev (d : more) =
do assert s d
res <- SMT.check (solver s)
case res of
SMT.Unsat -> do solPop s
assert s d
start (d : bad) prev
_ -> go bad (d : prev) more
{- | Attempt to find a substituion that, when applied, makes all of the
given properties hold. -}
getModel :: Solver -> [Cry.Prop] -> IO (Maybe Cry.Subst)
getModel s props = withScope s $
do ps <- assumeProps s props
res <- SMT.check (solver s)
let vars = Set.toList $ Set.unions $ map (cryPropFVS . unSimpProp) ps
case res of
SMT.Sat ->
do vs <- getVals (solver s) vars
-- This is guaranteed to be a model only for the *linear*
-- properties, so now we check if it works for the rest too.
let su1 = fmap K vs
ps1 = [ fromMaybe p (apSubst su1 p) | SimpProp p <- ps ]
ok p = case crySimplify p of
PTrue -> True
_ -> False
su2 = Cry.listSubst
[ (x, numTy v) | (UserName x, v) <- Map.toList vs ]
return (guard (all ok ps1) >> return su2)
_ -> return Nothing
where
numTy Inf = Cry.tInf
numTy (Nat k) = Cry.tNum k
--------------------------------------------------------------------------------
-- | An SMT solver, and some info about declared variables.
data Solver = Solver
{ solver :: SMT.Solver
-- ^ The actual solver
, declared :: IORef VarInfo
-- ^ Information about declared variables, and assumptions in scope.
, logger :: SMT.Logger
-- ^ For debugging
}
loadFile :: Solver -> FilePath -> IO ()
loadFile s file = go . dropComments =<< StrictIO.readFile file
where
go txt
| all isSpace txt = return ()
| otherwise = case SMT.readSExpr txt of
Just (e,rest) -> SMT.command (solver s) e >> go rest
Nothing -> panic "loadFile" [ "Failed to parse SMT file."
, txt
]
dropComments = unlines . map dropComment . lines
dropComment xs = case break (== ';') xs of
(as,_:_) -> as
_ -> xs
rawSolver :: Solver -> SMT.Solver
rawSolver = solver
-- | Keeps track of declared variables and non-linear terms.
data VarInfo = VarInfo
{ curScope :: Scope
, otherScopes :: [Scope]
} deriving Show
data Scope = Scope
{ scopeNames :: [Name]
-- ^ Variables declared in this scope (not counting the ones from
-- previous scopes).
, scopeNonLinS :: NonLinS
{- ^ These are the non-linear terms mentioned in the assertions
that are currently asserted (including ones from previous scopes). -}
, scopeIntervals :: Either Cry.TVar (Map.Map Cry.TVar Interval)
-- ^ Either a type variable that makes the asserted properties unsatisfiable
-- (due to a broken interval), or the current set of intervals for type
-- variables. If a variable is not in the interval map, its value can be
-- anything.
--
-- This includes all intervals from previous scopes.
, scopeAsserted :: [Cry.Prop]
-- ^ This is the set of currently-asserted cryptol properties only in this
-- scope.
--
-- This includes all asserted props from previous scopes.
} deriving Show
scopeEmpty :: Scope
scopeEmpty = Scope { scopeNames = [], scopeNonLinS = initialNonLinS
, scopeIntervals = Right Map.empty, scopeAsserted = [] }
scopeElem :: Name -> Scope -> Bool
scopeElem x Scope { .. } = x `elem` scopeNames
scopeInsert :: Name -> Scope -> Scope
scopeInsert x Scope { .. } = Scope { scopeNames = x : scopeNames, .. }
scopeAssertNew :: Cry.Prop -> Scope -> Scope
scopeAssertNew prop Scope { .. } =
Scope { scopeIntervals = ints'
, scopeAsserted = props
, .. }
where
props = prop : scopeAsserted
ints' = case scopeIntervals of
Left tv -> Left tv
Right ints -> case computePropIntervals ints props of
NoChange -> scopeIntervals
NewIntervals is -> Right is
InvalidInterval tv -> Left tv
-- | Given a *simplified* prop, separate linear and non-linear parts
-- and return the linear ones.
scopeAssertSimpProp :: SimpProp -> Scope -> ([SimpProp],Scope)
scopeAssertSimpProp (SimpProp p) Scope { .. } =
let (ps1,s1) = nonLinProp scopeNonLinS p
in (map SimpProp ps1, Scope { scopeNonLinS = s1, .. })
scopeAssert :: HasProp a => DefinedProp a -> Scope -> ([SimpProp],Scope)
scopeAssert DefinedProp { .. } s =
let (ps1,s1) = scopeAssertSimpProp dpSimpProp s
in (ps1,scopeAssertNew (getProp dpData) s1)
-- | No scopes.
viEmpty :: VarInfo
viEmpty = VarInfo { curScope = scopeEmpty, otherScopes = [] }
-- | Check if a name is any of the scopes.
viElem :: Name -> VarInfo -> Bool
viElem x VarInfo { .. } = any (x `scopeElem`) (curScope : otherScopes)
-- | Add a name to a scope.
viInsert :: Name -> VarInfo -> VarInfo
viInsert x VarInfo { .. } = VarInfo { curScope = scopeInsert x curScope, .. }
-- | Add an assertion to the current scope. Returns the linear part.
viAssertSimpProp :: SimpProp -> VarInfo -> (VarInfo, [SimpProp])
viAssertSimpProp p VarInfo { .. } = ( VarInfo { curScope = s1, .. }, p1)
where (p1, s1) = scopeAssertSimpProp p curScope
viAssert :: HasProp a => DefinedProp a -> VarInfo -> (VarInfo, [SimpProp])
viAssert d VarInfo { .. } = (VarInfo { curScope = s1, .. },p1)
where (p1, s1) = scopeAssert d curScope
-- | Enter a scope.
viPush :: VarInfo -> VarInfo
viPush VarInfo { .. } =
VarInfo { curScope = scopeEmpty { scopeNonLinS = scopeNonLinS curScope
, scopeAsserted = scopeAsserted curScope
, scopeIntervals = scopeIntervals curScope }
, otherScopes = curScope : otherScopes
}
-- | Exit a scope.
viPop :: VarInfo -> VarInfo
viPop VarInfo { .. } = case otherScopes of
c : cs -> VarInfo { curScope = c, otherScopes = cs }
_ -> panic "viPop" ["no more scopes"]
-- | All declared names, that have not been "marked".
-- These are the variables whose values we are interested in.
viUnmarkedNames :: VarInfo -> [ Name ]
viUnmarkedNames VarInfo { .. } = concatMap scopeNames scopes
where scopes = curScope : otherScopes
getIntervals :: Solver -> IO (Either Cry.TVar (Map Cry.TVar Interval))
getIntervals Solver { .. } =
do vi <- readIORef declared
return (scopeIntervals (curScope vi))
-- | All known non-linear terms.
getNLSubst :: Solver -> IO Subst
getNLSubst Solver { .. } =
do VarInfo { .. } <- readIORef declared
return $ nonLinSubst $ scopeNonLinS curScope
-- | Execute a computation with a fresh solver instance.
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver SolverConfig { .. } k =
do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
let smtDbg = if solverVerbose > 1 then Just logger else Nothing
solver <- SMT.newSolver solverPath solverArgs smtDbg
_ <- SMT.setOptionMaybe solver ":global-decls" "false"
-- SMT.setLogic solver "QF_LIA"
declared <- newIORef viEmpty
a <- k Solver { .. }
_ <- SMT.stop solver
return a
where
quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
, SMT.logLevel = return 0
, SMT.logSetLevel= \_ -> return ()
, SMT.logTab = return ()
, SMT.logUntab = return ()
}
solPush :: Solver -> IO ()
solPush Solver { .. } =
do SMT.push solver
SMT.logTab logger
modifyIORef' declared viPush
solPop :: Solver -> IO ()
solPop Solver { .. } =
do modifyIORef' declared viPop
SMT.logUntab logger
SMT.pop solver
-- | Execute a computation in a new solver scope.
withScope :: Solver -> IO a -> IO a
withScope s k =
do solPush s
a <- k
solPop s
return a
-- | Declare a variable.
declareVar :: Solver -> Name -> IO ()
declareVar s@Solver { .. } a =
do done <- fmap (a `viElem`) (readIORef declared)
unless done $
do e <- SMT.declare solver (smtName a) SMT.tInt
let fin_a = smtFinName a
fin <- SMT.declare solver fin_a SMT.tBool
SMT.assert solver (SMT.geq e (SMT.int 0))
nlSu <- getNLSubst s
modifyIORef' declared (viInsert a)
case Map.lookup a nlSu of
Nothing -> return ()
Just e' ->
do let finDef = crySimplify (Fin e')
mapM_ (declareVar s) (Set.toList (cryPropFVS finDef))
SMT.assert solver $
SMT.eq fin (ifPropToSmtLib (desugarProp finDef))
-- | Add an assertion to the current context.
-- INVARIANT: Assertion is simplified.
assert :: HasProp a => Solver -> DefinedProp a -> IO ()
assert _ DefinedProp { dpSimpProp = SimpProp PTrue } = return ()
assert s@Solver { .. } def@DefinedProp { dpSimpProp = p } =
do debugLog s ("Assuming: " ++ show (ppProp (unSimpProp p)))
a <- getIntervals s
debugLog s ("Intervals before:" ++ show (either pp ppIntervals a))
ps1' <- atomicModifyIORef' declared (viAssert def)
b <- getIntervals s
debugLog s ("Intervals after:" ++ show (either pp ppIntervals b))
let ps1 = map unSimpProp ps1'
vs = Set.toList $ Set.unions $ map cryPropFVS ps1
mapM_ (declareVar s) vs
mapM_ (SMT.assert solver . ifPropToSmtLib . desugarProp) ps1
-- | Add an assertion to the current context.
-- INVARIANT: Assertion is simplified.
assertSimpProp :: Solver -> SimpProp -> IO ()
assertSimpProp _ (SimpProp PTrue) = return ()
assertSimpProp s@Solver { .. } p@(SimpProp p0) =
do debugLog s ("Assuming: " ++ show (ppProp p0))
ps1' <- atomicModifyIORef' declared (viAssertSimpProp p)
let ps1 = map unSimpProp ps1'
vs = Set.toList $ Set.unions $ map cryPropFVS ps1
mapM_ (declareVar s) vs
mapM_ (SMT.assert solver . ifPropToSmtLib . desugarProp) ps1
-- | Try to prove a property. The result is 'True' when we are sure that
-- the property holds, and 'False' otherwise. In other words, getting `False`
-- *does not* mean that the proposition does not hold.
prove :: Solver -> Prop -> IO Bool
prove _ PTrue = return True
prove s@Solver { .. } p =
debugBlock s ("Proving: " ++ show (ppProp p)) $
withScope s $
do assertSimpProp s (simpProp (Not p))
res <- SMT.check solver
case res of
SMT.Unsat -> debugLog s "Proved" >> return True
SMT.Unknown -> debugLog s "Not proved" >> return False -- We are not sure
SMT.Sat -> debugLog s "Not proved" >> return False
-- XXX: If the answer is Sat, it is possible that this is a
-- a fake example, as we need to evaluate the nonLinear constraints.
-- If they are all satisfied, then we have a genuine counter example.
-- Otherwise, we could look for another one...
{- | Check if the current set of assumptions is satisfiable, and find
some facts that must hold in any models of the current assumptions.
Returns `Nothing` if the currently asserted constraints are known to
be unsatisfiable.
Returns `Just (su, sub-goals)` is the current set is satisfiable.
* The `su` is a substitution that may be applied to the current constraint
set without loosing generality.
* The `sub-goals` are additional constraints that must hold if the
constraint set is to be satisfiable.
-}
check :: Solver -> IO (Maybe (Subst, [Prop]))
check s@Solver { .. } =
do e <- getIntervals s
case e of
Left tv ->
do debugLog s ("Invalid interval: " ++ show (pp tv))
return Nothing
Right ints ->
do debugLog s ("Intervals:" ++ show (ppIntervals ints))
res <- SMT.check solver
case res of
SMT.Unsat ->
do debugLog s "Not satisfiable"
return Nothing
SMT.Unknown ->
do debugLog s "Unknown"
return (Just (Map.empty, []))
SMT.Sat ->
do debugLog s "Satisfiable"
(impMap,sideConds) <- debugBlock s "Computing improvements"
(getImpSubst s)
return (Just (impMap, sideConds))
{- | Assuming that we are in a satisfiable state, try to compute an
improving substitution. We also return additional constraints that must
hold for the currently asserted propositions to hold.
-}
getImpSubst :: Solver -> IO (Subst,[Prop])
getImpSubst s@Solver { .. } =
do names <- viUnmarkedNames `fmap` readIORef declared
m <- getVals solver names
(impSu,sideConditions) <- cryImproveModel solver logger m
nlSu <- getNLSubst s
let isNonLinName (SysName {}) = True
isNonLinName (UserName {}) = False
(nlFacts, vFacts) = Map.partitionWithKey (\k _ -> isNonLinName k) impSu
(vV, vNL) = Map.partition noNLVars vFacts
nlSu1 = fmap (doAppSubst vV) nlSu
(vNL_su,vNL_eqs) = Map.partitionWithKey goodDef
$ fmap (doAppSubst nlSu1) vNL
nlSu2 = fmap (doAppSubst vNL_su) nlSu1
nlLkp x = case Map.lookup x nlSu2 of
Just e -> e
Nothing -> panic "getImpSubst"
[ "Missing NL variable:", show x ]
allSides =
[ Var a :== e | (a,e) <- Map.toList vNL_eqs ] ++
[ nlLkp x :== doAppSubst nlSu2 e | (x,e) <- Map.toList nlFacts ] ++
[ doAppSubst nlSu2 si | si <- sideConditions ]
theImpSu = composeSubst vNL_su vV
debugBlock s "Improvments" $
do debugBlock s "substitution" $
mapM_ (debugLog s . dump) (Map.toList theImpSu)
debugBlock s "side-conditions" $ debugLog s allSides
return (theImpSu, allSides)
where
goodDef k e = not (k `Set.member` cryExprFVS e)
isNLVar (SysName _) = True
isNLVar _ = False
noNLVars e = all (not . isNLVar) (cryExprFVS e)
dump (x,e) = show (ppProp (Var x :== e))
--------------------------------------------------------------------------------
debugBlock :: Solver -> String -> IO a -> IO a
debugBlock s@Solver { .. } name m =
do debugLog s name
SMT.logTab logger
a <- m
SMT.logUntab logger
return a
class DebugLog t where
debugLog :: Solver -> t -> IO ()
debugLogList :: Solver -> [t] -> IO ()
debugLogList s ts = case ts of
[] -> debugLog s "(none)"
_ -> mapM_ (debugLog s) ts
instance DebugLog Char where
debugLog s x = SMT.logMessage (logger s) (show x)
debugLogList s x = SMT.logMessage (logger s) x
instance DebugLog a => DebugLog [a] where
debugLog = debugLogList
instance DebugLog a => DebugLog (Maybe a) where
debugLog s x = case x of
Nothing -> debugLog s "(nothing)"
Just a -> debugLog s a
instance DebugLog Doc where
debugLog s x = debugLog s (show x)
instance DebugLog Cry.Type where
debugLog s x = debugLog s (pp x)
instance DebugLog Goal where
debugLog s x = debugLog s (goal x)
instance DebugLog Cry.Subst where
debugLog s x = debugLog s (pp x)
instance DebugLog Prop where
debugLog s x = debugLog s (ppProp x)

425
src/Cryptol/TypeCheck/Solver/Numeric/AST.hs
View File

@ -1,425 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- The sytnax of numeric propositions.
{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.TypeCheck.Solver.Numeric.AST
( Name(..), ppName
, Prop(..), cryPropExprs, cryPropFVS
, ppProp, ppPropPrec
, Expr(..), zero, one, two, inf, cryAnds, cryOrs
, cryExprExprs, cryRebuildExpr
, cryExprFVS
, ppExpr, ppExprPrec
, Nat'(..)
, IfExpr, IfExpr'(..), ppIf, ppIfExpr
, Subst, HasVars(..), cryLet, composeSubst, doAppSubst
) where
import Cryptol.TypeCheck.AST(TVar)
import Cryptol.TypeCheck.PP(pp)
import Cryptol.TypeCheck.Solver.InfNat ( Nat'(..) )
import Cryptol.Utils.PP ( Doc, text, (<+>), hang, ($$), char, (<>)
, parens, integer, sep )
import Cryptol.Utils.Panic ( panic )
import Cryptol.Utils.Misc ( anyJust )
-- import Data.GenericTrie (TrieKey)
import GHC.Generics(Generic)
import Data.Maybe (fromMaybe)
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Set ( Set )
import qualified Data.Set as Set
import qualified Control.Applicative as A
import Control.Monad ( liftM, ap )
infixr 2 :||
infixr 3 :&&
infix 4 :==, :>, :>=, :==:, :>:
infixl 6 :+, :-
infixl 7 :*
infixr 8 :^^
data Name = UserName TVar | SysName Int
deriving (Show,Eq,Ord,Generic)
-- | Propopsitions, representing Cryptol's numeric constraints (and a bit more).
data Prop =
-- Preidcates on natural numbers with infinity.
-- After simplification, the only one of these should be `fin x`,
-- where `x` is a variable.
Fin Expr | Expr :== Expr | Expr :>= Expr | Expr :> Expr
-- Predicate on strict natural numbers (i.e., no infinities)
-- Should be introduced by 'cryNatOp', to eliminte 'inf'.
| Expr :==: Expr | Expr :>: Expr
-- Standard logical strucutre>
| Prop :&& Prop | Prop :|| Prop
| Not Prop
| PFalse | PTrue
deriving (Eq,Show,Generic)
-- | Expressions, representing Cryptol's numeric types.
data Expr = K Nat'
| Var Name
| Expr :+ Expr -- total
| Expr :- Expr -- partial: x >= y, fin y
| Expr :* Expr -- total
| Div Expr Expr -- partial: fin x, y >= 1
| Mod Expr Expr -- partial: fin x, y >= 1
| Expr :^^ Expr -- total
| Min Expr Expr -- total
| Max Expr Expr -- total
| Width Expr -- total
| LenFromThen Expr Expr Expr -- partial: x /= y, w >= width x
| LenFromThenTo Expr Expr Expr -- partial: x /= y
deriving (Eq,Show,Generic,Ord)
-- | The constant @0@.
zero :: Expr
zero = K (Nat 0)
-- | The constant @1@.
one :: Expr
one = K (Nat 1)
-- | The constant @2@.
two :: Expr
two = K (Nat 2)
-- | The constant @infinity@.
inf :: Expr
inf = K Inf
-- | Make a conjucntion of the given properties.
cryAnds :: [Prop] -> Prop
cryAnds [] = PTrue
cryAnds ps = foldr1 (:&&) ps
-- | Make a disjunction of the given properties.
cryOrs :: [Prop] -> Prop
cryOrs [] = PFalse
cryOrs ps = foldr1 (:||) ps
-- | Compute all expressions in a property.
cryPropExprs :: Prop -> [Expr]
cryPropExprs = go []
where
go es prop =
case prop of
PTrue -> es
PFalse -> es
Not p -> go es p
p :&& q -> go (go es q) p
p :|| q -> go (go es q) p
Fin x -> x : es
x :== y -> x : y : es
x :> y -> x : y : es
x :>= y -> x : y : es
x :==: y -> x : y : es
x :>: y -> x : y : es
-- | Compute the immediate sub-expressions of an expression.
cryExprExprs :: Expr -> [Expr]
cryExprExprs expr =
case expr of
K _ -> []
Var _ -> []
x :+ y -> [x,y]
x :- y -> [x,y]
x :* y -> [x,y]
Div x y -> [x,y]
Mod x y -> [x,y]
x :^^ y -> [x,y]
Min x y -> [x,y]
Max x y -> [x,y]
Width x -> [x]
LenFromThen x y z -> [x,y,z]
LenFromThenTo x y z -> [x,y,z]
-- | Rebuild an expression, using the top-level strucutre of the first
-- expression, but the second list of expressions as sub-expressions.
cryRebuildExpr :: Expr -> [Expr] -> Expr
cryRebuildExpr expr args =
case (expr,args) of
(K _, []) -> expr
(Var _, []) -> expr
(_ :+ _k, [x,y]) -> x :+ y
(_ :- _ , [x,y]) -> x :- y
(_ :* _ , [x,y]) -> x :* y
(Div _ _, [x,y]) -> Div x y
(Mod _ _, [x,y]) -> Mod x y
(_ :^^ _, [x,y]) -> x :^^ y
(Min _ _, [x,y]) -> Min x y
(Max _ _, [x,y]) -> Max x y
(Width _, [x]) -> Width x
(LenFromThen _ _ _ , [x,y,z]) -> LenFromThen x y z
(LenFromThenTo _ _ _ , [x,y,z]) -> LenFromThenTo x y z
_ -> panic "cryRebuildExpr" $ map show
$ text "expr:" <+> ppExpr expr
: [ text "arg:" <+> ppExpr a | a <- args ]
-- | Compute the free variables in an expression.
cryExprFVS :: Expr -> Set Name
cryExprFVS expr =
case expr of
Var x -> Set.singleton x
_ -> Set.unions (map cryExprFVS (cryExprExprs expr))
-- | Compute the free variables in a proposition.
cryPropFVS :: Prop -> Set Name
cryPropFVS = Set.unions . map cryExprFVS . cryPropExprs
data IfExpr' p a = If p (IfExpr' p a) (IfExpr' p a) | Return a | Impossible
deriving Eq
type IfExpr = IfExpr' Prop
instance Monad (IfExpr' p) where
return = Return
fail _ = Impossible
m >>= k = case m of
Impossible -> Impossible
Return a -> k a
If p t e -> If p (t >>= k) (e >>= k)
instance Functor (IfExpr' p) where
fmap = liftM
instance A.Applicative (IfExpr' p) where
pure = return
(<*>) = ap
--------------------------------------------------------------------------------
-- Substitution
--------------------------------------------------------------------------------
type Subst = Map Name Expr
composeSubst :: Subst -> Subst -> Subst
composeSubst g f = Map.union f' g
where
f' = fmap (\e -> fromMaybe e (apSubst g e)) f
cryLet :: HasVars e => Name -> Expr -> e -> Maybe e
cryLet x e = apSubst (Map.singleton x e)
doAppSubst :: HasVars a => Subst -> a -> a
doAppSubst su a = fromMaybe a (apSubst su a)
-- | Replaces occurances of the name with the expression.
-- Returns 'Nothing' if there were no occurances of the name.
class HasVars ast where
apSubst :: Subst -> ast -> Maybe ast
-- | This is used in the simplification to "apply" substitutions to Props.
instance HasVars Bool where
apSubst _ _ = Nothing
instance HasVars Expr where
apSubst su = go
where
go expr =
case expr of
K _ -> Nothing
Var b -> Map.lookup b su
x :+ y -> bin (:+) x y
x :- y -> bin (:-) x y
x :* y -> bin (:*) x y
x :^^ y -> bin (:^^) x y
Div x y -> bin Div x y
Mod x y -> bin Mod x y
Min x y -> bin Min x y
Max x y -> bin Max x y
Width x -> Width `fmap` go x
LenFromThen x y w -> three LenFromThen x y w
LenFromThenTo x y z -> three LenFromThen x y z
bin f x y = do [x',y'] <- anyJust go [x,y]
return (f x' y')
three f x y z = do [x',y',z'] <- anyJust go [x,y,z]
return (f x' y' z')
instance HasVars Prop where
apSubst su = go
where
go prop =
case prop of
PFalse -> Nothing
PTrue -> Nothing
Not p -> Not `fmap` go p
p :&& q -> bin (:&&) p q
p :|| q -> bin (:||) p q
Fin x -> Fin `fmap` apSubst su x
x :== y -> twoE (:==) x y
x :>= y -> twoE (:>=) x y
x :> y -> twoE (:>) x y
x :==: y -> twoE (:==:) x y
x :>: y -> twoE (:>) x y
bin f x y = do [x',y'] <- anyJust go [x,y]
return (f x' y')
twoE f x y = do [x',y'] <- anyJust (apSubst su) [x,y]
return (f x' y')
--------------------------------------------------------------------------------
-- Tries
--------------------------------------------------------------------------------
-- instance TrieKey Name
-- instance TrieKey Prop
-- instance TrieKey Expr
--------------------------------------------------------------------------------
-- Pretty Printing
--------------------------------------------------------------------------------
-- | Pretty print a name.
ppName :: Name -> Doc
ppName name =
case name of
UserName x -> pp x
SysName x -> char '_' <> text (names !! x)
-- | An infinite list of names, for pretty prinitng.
names :: [String]
names = concatMap gen [ 0 :: Integer .. ]
where
gen x = [ a : suff x | a <- [ 'a' .. 'z' ] ]
suff 0 = ""
suff x = show x
-- | Pretty print a top-level property.
ppProp :: Prop -> Doc
ppProp = ppPropPrec 0
-- | Pretty print a proposition, in the given precedence context.
ppPropPrec :: Int -> Prop -> Doc
ppPropPrec prec prop =
case prop of
Fin x -> fun "fin" ppExprPrec x
x :== y -> bin "==" 4 1 1 ppExprPrec x y
x :>= y -> bin ">=" 4 1 1 ppExprPrec x y
x :> y -> bin ">" 4 1 1 ppExprPrec x y
x :==: y -> bin "==#" 4 1 1 ppExprPrec x y
x :>: y -> bin ">#" 4 1 1 ppExprPrec x y
p :&& q -> bin "&&" 3 1 0 ppPropPrec p q
p :|| q -> bin "||" 2 1 0 ppPropPrec p q
Not p -> fun "not" ppPropPrec p
PTrue -> text "True"
PFalse -> text "False"
where
wrap p d = if prec > p then parens d else d
fun f how x = wrap 10 (text f <+> how 11 x)
bin op opP lMod rMod how x y =
wrap opP (sep [ how (opP + lMod) x, text op, how (opP + rMod) y ])
-- | Pretty print an expression at the top level.
ppExpr :: Expr -> Doc
ppExpr = ppExprPrec 0
-- | Pretty print an expression, in the given precedence context.
ppExprPrec :: Int -> Expr -> Doc
ppExprPrec prec expr =
case expr of
K Inf -> text "inf"
K (Nat n) -> integer n
Var a -> ppName a
x :+ y -> bin "+" 6 0 1 x y
x :- y -> bin "-" 6 0 1 x y
x :* y -> bin "*" 7 0 1 x y
Div x y -> fun "div" [x,y]
Mod x y -> fun "mod" [x,y]
x :^^ y -> bin "^^" 8 1 0 x y
Min x y -> fun "min" [x,y]
Max x y -> fun "max" [x,y]
Width x -> fun "width" [x]
LenFromThen x y w -> fun "lenFromThen" [x,y,w]
LenFromThenTo x y z -> fun "lenFromThenTo" [x,y,z]
where
wrap p d = if prec > p then parens d else d
fun f xs = wrap 10 (text f <+> sep (map (ppExprPrec 11) xs))
bin op opP lMod rMod x y =
wrap opP
(ppExprPrec (opP + lMod) x <+> text op <+> ppExprPrec (opP + rMod) y)
-- | Pretty print an experssion with ifs.
ppIfExpr :: IfExpr Expr -> Doc
ppIfExpr = ppIf ppProp ppExpr
-- | Pretty print an experssion with ifs.
ppIf :: (p -> Doc) -> (a -> Doc) -> IfExpr' p a -> Doc
ppIf ppAtom ppVal = go
where
go expr =
case expr of
If p t e -> hang (text "if" <+> ppAtom p) 2
( (text "then" <+> go t) $$
(text "else" <+> go e)
)
Return e -> ppVal e
Impossible -> text "<impossible>"

55
src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs
View File

@ -1,55 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.Numeric.Defined where
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.Utils.Panic ( panic )
-- | A condition ensure that the given *basic* proposition makes sense.
cryDefinedProp :: Prop -> Prop
cryDefinedProp prop =
case prop of
Fin x -> cryDefined x
x :== y -> cryDefined x :&& cryDefined y
x :>= y -> cryDefined x :&& cryDefined y
Not p -> cryDefinedProp p
_ -> panic "cryDefinedProp" [ "Not a simple property:"
, show (ppProp prop)
]
-- | Generate a property ensuring that the expression is well-defined.
-- This might be a bit too strict. For example, we reject things like
-- @max inf (0 - 1)@, which one might think would simplify to @inf@.
cryDefined :: Expr -> Prop
cryDefined expr =
case expr of
K _ -> PTrue
Var _ -> PTrue -- Variables are always assumed to be OK.
-- The idea is that we are going to check for
-- defined-ness before instantiating variables.
x :+ y -> cryDefined x :&& cryDefined y
x :- y -> cryDefined x :&& cryDefined y :&&
Fin y :&& x :>= y
x :* y -> cryDefined x :&& cryDefined y
Div x y -> cryDefined x :&& cryDefined y :&&
Fin x :&& y :>= K (Nat 1)
Mod x y -> cryDefined x :&& cryDefined y :&&
Fin x :&& y :>= K (Nat 1)
x :^^ y -> cryDefined x :&& cryDefined y
Min x y -> cryDefined x :&& cryDefined y
Max x y -> cryDefined x :&& cryDefined y
Width x -> cryDefined x
LenFromThen x y w ->
cryDefined x :&& cryDefined y :&& cryDefined w :&&
Fin x :&& Fin y :&& Fin w :&& Not (x :== y) :&& w :>= Width x
LenFromThenTo x y z ->
cryDefined x :&& cryDefined y :&& cryDefined z :&&
Fin x :&& Fin y :&& Fin z :&& Not (x :== y)

171
src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
View File

@ -1,171 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.Numeric.ImportExport
( ExportM
, exportProp
, exportType
, runExportM
, exportPropM
, exportTypeM
, importProp
, importType
) where
import Cryptol.TypeCheck.Solver.Numeric.AST
import qualified Cryptol.TypeCheck.AST as Cry
import qualified Cryptol.TypeCheck.SimpType as SCry
import MonadLib
exportProp :: Cry.Prop -> Maybe Prop
exportProp = runExportM . exportPropM
exportType :: Cry.Prop -> Maybe Expr
exportType = runExportM . exportTypeM
runExportM :: ExportM a -> Maybe a
runExportM = either (\_ -> Nothing) Just
. runId
. runExceptionT
type ExportM = ExceptionT () Id
exportPropM :: Cry.Prop -> ExportM Prop
exportPropM ty =
case ty of
Cry.TUser _ _ t -> exportPropM t
Cry.TRec {} -> raise ()
Cry.TVar {} -> raise ()
Cry.TCon (Cry.PC pc) ts ->
mapM exportTypeM ts >>= \ets ->
case (pc, ets) of
(Cry.PFin, [t]) -> return (Fin t)
(Cry.PEqual, [t1,t2]) -> return (t1 :== t2)
(Cry.PNeq, [t1,t2]) -> return (Not (t1 :== t2))
(Cry.PGeq, [t1,t2]) -> return (t1 :>= t2)
_ -> raise ()
Cry.TCon _ _ -> raise ()
exportTypeM :: Cry.Type -> ExportM Expr
exportTypeM ty =
case ty of
Cry.TUser _ _ t -> exportTypeM t
Cry.TRec {} -> raise ()
Cry.TVar x -> return $ Var $ UserName x
Cry.TCon tc ts ->
case tc of
Cry.TError {} -> raise ()
Cry.TC Cry.TCInf -> return (K Inf)
Cry.TC (Cry.TCNum x) -> return (K (Nat x))
Cry.TC _ -> raise ()
Cry.TF f ->
mapM exportTypeM ts >>= \ets ->
case (f, ets) of
(Cry.TCAdd, [t1,t2]) -> return (t1 :+ t2)
(Cry.TCSub, [t1,t2]) -> return (t1 :- t2)
(Cry.TCMul, [t1,t2]) -> return (t1 :* t2)
(Cry.TCDiv, [t1,t2]) -> return (Div t1 t2)
(Cry.TCMod, [t1,t2]) -> return (Mod t1 t2)
(Cry.TCExp, [t1,t2]) -> return (t1 :^^ t2)
(Cry.TCMin, [t1,t2]) -> return (Min t1 t2)
(Cry.TCMax, [t1,t2]) -> return (Max t1 t2)
(Cry.TCWidth, [t1]) -> return (Width t1)
(Cry.TCLenFromThen, [t1,t2,t3]) -> return (LenFromThen t1 t2 t3)
(Cry.TCLenFromThenTo, [t1,t2,t3]) -> return (LenFromThenTo t1 t2 t3)
_ -> raise ()
Cry.PC _ -> raise ()
importProp :: Prop -> Maybe [Cry.Prop]
importProp prop =
case prop of
PFalse -> Nothing
PTrue -> Just []
Not p -> importProp =<< pNot p
p1 :&& p2 -> do ps1 <- importProp p1
ps2 <- importProp p2
return (ps1 ++ ps2)
_ :|| _ -> Nothing
Fin expr -> do t <- importType expr
return [ Cry.pFin t ]
e1 :== e2 -> do t1 <- importType e1
t2 <- importType e2
return [t1 Cry.=#= t2]
e1 :>= e2 -> do t1 <- importType e1
t2 <- importType e2
return [t1 Cry.>== t2]
_ :> _ -> Nothing
e1 :==: e2 -> do t1 <- importType e1
t2 <- importType e2
-- XXX: Do we need to add fin?
return [t1 Cry.=#= t2]
_ :>: _ -> Nothing
where
pNot p =
case p of
PFalse -> Just PTrue
PTrue -> Nothing
Not a -> Just a
_ :&& _ -> Nothing
a :|| b -> Just (Not a :&& Not b)
Fin a -> Just (a :== K Inf)
_ :== _ -> Nothing
_ :>= _ -> Nothing
a :> b -> Just (b :>= a)
_ :==: _ -> Nothing
a :>: b -> Just (b :>= a)
-- XXX: Do we need to add Fin on `a` and 'b'?
importType :: Expr -> Maybe Cry.Type
importType = go
where
go expr =
case expr of
Var x -> case x of
UserName v -> return (Cry.TVar v)
_ -> Nothing
K n -> case n of
Nat x -> Just (Cry.tNum x)
Inf -> Just (Cry.tInf)
x :+ y -> op2 SCry.tAdd x y
x :- y -> op2 SCry.tSub x y
x :* y -> op2 SCry.tMul x y
Div x y -> op2 SCry.tDiv x y
Mod x y -> op2 SCry.tMod x y
x :^^ y -> op2 SCry.tExp x y
Min x y -> op2 SCry.tMin x y
Max x y -> op2 SCry.tMax x y
Width x -> op1 SCry.tWidth x
LenFromThen x y z -> op3 SCry.tLenFromThen x y z
LenFromThenTo x y z -> op3 SCry.tLenFromThenTo x y z
op1 f x =
do t <- go x
return (f t)
op2 f x y =
do t1 <- go x
t2 <- go y
return (f t1 t2)
op3 f x y z =
do t1 <- go x
t2 <- go y
t3 <- go z
return (f t1 t2 t3)

281
src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs
View File

@ -1,281 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Separate Non-Linear Constraints
-- When we spot a non-linear expression, we name it and add it to a map.
--
-- If we see the same expression multiple times, then we give it the same name.
--
-- The body of the non-linear expression is not processed further,
-- so the resulting map should not contain any of the newly minted names.
{-# LANGUAGE Safe, RecordWildCards #-}
module Cryptol.TypeCheck.Solver.Numeric.NonLin
( nonLinProp
, NonLinS, nonLinSubst
, initialNonLinS
, apSubstNL
, lookupNL
) where
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.Simplify
import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
import Cryptol.Utils.Panic(panic)
-- import Data.GenericTrie (Trie)
-- import qualified Data.GenericTrie as Trie
import Data.Maybe ( fromMaybe )
import MonadLib
import Data.Map (Map)
import qualified Data.Map as Map
type Trie = Map
trie_empty :: Map k a
trie_empty = Map.empty
trie_insert :: Expr -> a -> Map Expr a -> Map Expr a
trie_insert = Map.insert
trie_delete :: Expr -> Map Expr a -> Map Expr a
trie_delete = Map.delete
trie_lookup :: Expr -> Map Expr a -> Maybe a
trie_lookup = Map.lookup
-- | Factor-out non-linear terms, by naming them.
nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS)
nonLinProp s0 prop = (p : ps, s)
where ((p,ps),s) = runNL s0 (nonLinPropM prop)
{- | Apply a substituin to the non-linear expression database.
Returns `Nothing` if nothing was affected.
Otherwise returns `Just`, and a substitution for non-linear expressions
that became linear.
The definitions of NL terms do not contain other named NL terms,
so it does not matter if the substitution contains bindings like @_a = e@.
There should be no bindings that mention NL term names in the definitions
of the substition (i.e, things like @x = _a@ are NOT ok).
-}
apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS)
apSubstNL su s0 = case runNL s0 (mApSubstNL su) of
((Nothing,_),_) -> Nothing
((Just su1,ps),r) -> Just (su1,ps,r)
lookupNL :: Name -> NonLinS -> Maybe Expr
lookupNL x NonLinS { .. } = Map.lookup x nonLinExprs
runNL :: NonLinS -> NonLinM a -> ((a, [Prop]), NonLinS)
runNL s m = runId
$ runStateT s
$ do a <- m
ps <- finishTodos
return (a,ps)
-- | Get the known non-linear terms.
nonLinSubst :: NonLinS -> Subst
nonLinSubst = nonLinExprs
-- | The initial state for the linearization process.
initialNonLinS :: NonLinS
initialNonLinS = NonLinS
{ nextName = 0
, nonLinExprs = Map.empty
, nlKnown = trie_empty
, nlTodo = []
}
data SubstOneRes = NoChange
-- ^ Substitution does not affect the expression.
| Updated (Maybe (Name,Expr))
-- ^ The expression was updated and, maybe, it became linear.
{- | Apply the substituint to all non-linear bindings.
Returns `Nothing` if nothing was affected.
Otherwise returns `Just`, and a substituion mapping names that used
to be non-linear but became linear.
Note that we may return `Just empty`, indicating that some non-linear
expressions were updated, but they remained non-linear. -}
mApSubstNL :: Subst -> NonLinM (Maybe Subst)
mApSubstNL su =
do s <- get
answers <- mapM (mApSubstOneNL su) (Map.toList (nonLinExprs s))
return (foldr upd Nothing answers)
where
upd NoChange ch = ch
upd (Updated mb) ch = let lsu = fromMaybe Map.empty ch
in Just (case mb of
Nothing -> lsu
Just (x,e) -> Map.insert x e lsu)
mApSubstOneNL :: Subst -> (Name,Expr) -> NonLinM SubstOneRes
mApSubstOneNL su (x,e) =
case apSubst su e of
Nothing -> return NoChange
Just e1 ->
case crySimpExprMaybe e1 of
Nothing ->
sets $ \NonLinS { .. } ->
( Updated Nothing
, NonLinS { nonLinExprs = Map.insert x e1 nonLinExprs
, nlKnown = trie_insert e1 x (trie_delete e nlKnown)
, .. }
)
Just e2
| isNonLinOp e2 ->
sets $ \NonLinS { .. } ->
(Updated Nothing
, NonLinS { nonLinExprs = Map.insert x e2 nonLinExprs
, nlKnown = trie_insert e2 x (trie_delete e nlKnown)
, .. }
)
| otherwise ->
do sets_ $ \NonLinS { .. } ->
NonLinS { nonLinExprs = Map.delete x nonLinExprs
, nlKnown = trie_delete e nlKnown
, ..
}
es <- mapM nonLinExprM (cryExprExprs e2)
let e3 = cryRebuildExpr e2 es
return (Updated (Just (x,e3)))
-- | Is the top-level operator a non-linear one.
isNonLinOp :: Expr -> Bool
isNonLinOp expr =
case expr of
K _ -> False
Var _ -> False
_ :+ _ -> False
_ :- _ -> False
x :* y ->
case (x,y) of
(K _, _) -> False
(_, K _) -> False
_ -> True
Div _ y ->
case y of
K (Nat n) -> n == 0
_ -> True
Mod _ y ->
case y of
K (Nat n) -> n == 0
_ -> True
_ :^^ _ -> True
Min _ _ -> False
Max _ _ -> False
Width _ -> True
LenFromThen _ _ _ -> True -- See also comment on `LenFromThenTo`
LenFromThenTo x y _ ->
case (x,y) of
(K _, K _) -> False
_ -> True -- Actually, as long as the difference bettwen
-- `x` and `y` is constant we'd be OK, but not
-- sure how to do that...
nlImplied :: Expr -> Name -> [Prop]
nlImplied expr x =
map crySimplify $
case expr of
K (Nat n) :^^ e | n >= 2 -> [ Var x :>= one, Var x :>= e :+ one ]
Mod _ e -> [ e :>= Var x :+ one ]
_ -> []
nonLinPropM :: Prop -> NonLinM Prop
nonLinPropM prop =
case prop of
PFalse -> return PFalse
PTrue -> return PTrue
Not p -> Not `fmap` nonLinPropM p
p :&& q -> (:&&) `fmap` nonLinPropM p `ap` nonLinPropM q
p :|| q -> (:||) `fmap` nonLinPropM p `ap` nonLinPropM q
Fin (Var _) -> return prop
Fin _ -> unexpected
x :==: y -> (:==:) `fmap` nonLinExprM x `ap` nonLinExprM y
x :>: y -> (:>:) `fmap` nonLinExprM x `ap` nonLinExprM y
_ :== _ -> unexpected
_ :>= _ -> unexpected
_ :> _ -> unexpected
where
unexpected = panic "nonLinPropM" [ show (ppProp prop) ]
nonLinExprM :: Expr -> NonLinM Expr
nonLinExprM expr
| isNonLinOp expr = nameExpr expr
| otherwise = cryRebuildExpr expr `fmap` mapM nonLinExprM (cryExprExprs expr)
type NonLinM = StateT NonLinS Id
data NonLinS = NonLinS
{ nextName :: !Int
, nonLinExprs :: Subst
, nlKnown :: Trie Expr Name
, nlTodo :: [Prop]
} deriving Show
nameExpr :: Expr -> NonLinM Expr
nameExpr e = sets $ \s ->
case trie_lookup e (nlKnown s) of
Just x -> (Var x, s)
Nothing ->
let x = nextName s
n = SysName x
s1 = NonLinS { nextName = 1 + x
, nonLinExprs = Map.insert n e (nonLinExprs s)
, nlKnown = trie_insert e n (nlKnown s)
, nlTodo = nlImplied e n ++ nlTodo s
}
in (Var n, s1)
finishTodos :: NonLinM [Prop]
finishTodos =
do s <- get
case nlTodo s of
[] -> return []
p : ps ->
do set s { nlTodo = ps }
p' <- nonLinPropM p
ps' <- finishTodos
return (p' : ps')

517
src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
View File

@ -1,517 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Desugar into SMTLIB Terminology
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.Numeric.SMT
( desugarProp
, smtName
, smtFinName
, ifPropToSmtLib
, cryImproveModel
, getVal
, getVals
) where
import Cryptol.TypeCheck.AST (TVar(TVFree,TVBound))
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.Simplify(crySimplify)
import Cryptol.Utils.Misc ( anyJust )
import Cryptol.Utils.Panic ( panic )
import Data.List ( partition, unfoldr )
import Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.Set as Set
import SimpleSMT ( SExpr )
import qualified SimpleSMT as SMT
import MonadLib
--------------------------------------------------------------------------------
-- Desugar to SMT
--------------------------------------------------------------------------------
-- XXX: Expanding the if-then-elses could make things large.
-- Perhaps keep them as first class things, in hope that the solver
-- can do something more clever with that?
-- | Assumes simplified, linear, finite, defined expressions.
desugarExpr :: Expr -> IfExpr Expr
desugarExpr expr =
do es <- mapM desugarExpr (cryExprExprs expr)
case (expr,es) of
(Min {}, [x,y]) -> If (x :>: y) (return y) (return x)
(Max {}, [x,y]) -> If (x :>: y) (return x) (return y)
(LenFromThenTo {}, [ x@(K (Nat a)), K (Nat b), z ])
-- going down
| a > b -> If (z :>: x) (return zero)
(return (Div (x :- z) step :+ one))
-- goind up
| b > a -> If (x :>: z) (return zero)
(return (Div (z :- x) step :+ one))
where step = K (Nat (abs (a - b)))
_ -> return (cryRebuildExpr expr es)
-- | Assumes simplified, linear, defined.
desugarProp :: Prop -> IfExpr Prop
desugarProp prop =
case prop of
PFalse -> return PFalse
PTrue -> return PTrue
Not p -> Not `fmap` desugarProp p
p :&& q -> (:&&) `fmap` desugarProp p `ap` desugarProp q
p :|| q -> (:||) `fmap` desugarProp p `ap` desugarProp q
Fin (Var _) -> return prop
x :==: y -> (:==:) `fmap` desugarExpr x `ap` desugarExpr y
x :>: y -> (:>:) `fmap` desugarExpr x `ap` desugarExpr y
Fin _ -> unexpected
_ :== _ -> unexpected
_ :>= _ -> unexpected
_ :> _ -> unexpected
where
unexpected = panic "desugarProp" [ show (ppProp prop) ]
ifPropToSmtLib :: IfExpr Prop -> SExpr
ifPropToSmtLib ifProp =
case ifProp of
Impossible -> SMT.bool False -- Sholdn't really matter
Return p -> propToSmtLib p
If p q r -> SMT.ite (propToSmtLib p) (ifPropToSmtLib q) (ifPropToSmtLib r)
propToSmtLib :: Prop -> SExpr
propToSmtLib prop =
case prop of
PFalse -> SMT.bool False
PTrue -> SMT.bool True
Not p -> case p of
Fin _ -> SMT.not (propToSmtLib p)
-- It is IMPORTANT that the fin constraints are outside
-- the not.
x :>: y -> addFin $ SMT.geq (exprToSmtLib y)
(exprToSmtLib x)
_ -> unexpected
p :&& q -> SMT.and (propToSmtLib p) (propToSmtLib q)
p :|| q -> SMT.or (propToSmtLib p) (propToSmtLib q)
Fin (Var x) -> fin x
{- For the linear constraints, if the term is finite, then all of
its variables must have been finite.
XXX: Adding the `fin` decls at the leaves leads to some duplication:
We could add them just once for each conjunctoin of simple formulas,
but I am not sure how much this matters.
-}
x :==: y -> addFin $ SMT.eq (exprToSmtLib x) (exprToSmtLib y)
x :>: y -> addFin $ SMT.gt (exprToSmtLib x) (exprToSmtLib y)
Fin _ -> unexpected
_ :== _ -> unexpected
_ :>= _ -> unexpected
_ :> _ -> unexpected
where
unexpected = panic "propToSmtLib" [ show (ppProp prop) ]
fin x = SMT.const (smtFinName x)
addFin e = foldr (\x' e' -> SMT.and (fin x') e') e
(Set.toList (cryPropFVS prop))
exprToSmtLib :: Expr -> SExpr
exprToSmtLib expr =
case expr of
K (Nat n) -> SMT.int n
Var a -> SMT.const (smtName a)
x :+ y -> SMT.add (exprToSmtLib x) (exprToSmtLib y)
x :- y -> SMT.sub (exprToSmtLib x) (exprToSmtLib y)
x :* y -> SMT.mul (exprToSmtLib x) (exprToSmtLib y)
Div x y -> SMT.div (exprToSmtLib x) (exprToSmtLib y)
Mod x y -> SMT.mod (exprToSmtLib x) (exprToSmtLib y)
K Inf -> unexpected
_ :^^ _ -> unexpected
Min {} -> unexpected
Max {} -> unexpected
Width {} -> unexpected
LenFromThen {} -> unexpected
LenFromThenTo {} -> unexpected
where
unexpected = panic "exprToSmtLib" [ show (ppExpr expr) ]
-- | The name of a variable in the SMT translation.
smtName :: Name -> String
smtName a = case a of
SysName n -> name "s" n
UserName tv -> case tv of
TVFree n _ _ _ -> name "u" n
TVBound n _ -> name "k" n
where
name p n = case divMod n 26 of
(q,r) -> p ++ toEnum (fromEnum 'a' + r) :
(if q == 0 then "" else show q)
-- | The name of a boolean variable, representing `fin x`.
smtFinName :: Name -> String
smtFinName x = "fin_" ++ smtName x
--------------------------------------------------------------------------------
-- Models
--------------------------------------------------------------------------------
{- | Get the value for the given name.
* Assumes that we are in a SAT state (i.e., there is a model)
* Assumes that the name is in the model -}
getVal :: SMT.Solver -> Name -> IO Nat'
getVal s a =
do yes <- isInf a
if yes
then return Inf
else do v <- SMT.getConst s (smtName a)
case v of
SMT.Int x | x >= 0 -> return (Nat x)
_ -> panic "cryCheck.getVal" [ "Not a natural number", show v ]
where
isInf v = do yes <- SMT.getConst s (smtFinName v)
case yes of
SMT.Bool ans -> return (not ans)
_ -> panic "cryCheck.isInf"
[ "Not a boolean value", show yes ]
-- | Get the values for the given names.
getVals :: SMT.Solver -> [Name] -> IO (Map Name Nat')
getVals s xs =
do es <- mapM (getVal s) xs
return (Map.fromList (zip xs es))
-- | Convert a bunch of improving equations into an idempotent substitution.
-- Assumes that the equations don't have loops.
toSubst :: Map Name Expr -> Subst
toSubst m0 = last (m0 : unfoldr step m0)
where step m = do m1 <- anyJust (apSubst m) m
return (m1,m1)
{- | Given a model, compute an improving substitution, implied by the model.
The entries in the substitution look like this:
* @x = A@ variable @x@ must equal constant @A@
* @x = y@ variable @x@ must equal variable @y@
* @x = A * y + B@ (coming soon)
variable @x@ is a linear function of @y@,
@A@ and @B@ are natural numbers.
-}
{- | We are mostly interested in improving unification variables.
However, it is also useful to improve skolem variables, as this could
turn non-linear constraints into linear ones. For example, if we
have a constraint @x * y = z@, and we can figure out that @x@ must be 5,
then we end up with a linear constraint @5 * y = z@.
-}
cryImproveModel :: SMT.Solver -> SMT.Logger -> Map Name Nat'
-> IO (Map Name Expr, [Prop])
cryImproveModel solver logger model =
do (imps,subGoals) <- go Map.empty [] initialTodo
return (toSubst imps, subGoals)
where
-- Process unification variables first. That way, if we get `x = y`, we'd
-- prefer `x` to be a unification variable.
initialTodo = uncurry (++) $ partition (isUniVar . fst) $ Map.toList model
isUniVar x = case x of
UserName (TVFree {}) -> True
_ -> False
-- done: the set of known improvements
-- extra: the collection of inferred sub-goals
go done extra [] = return (done,extra)
go done extra ((x,e) : rest) =
-- x = K?
do mbCounter <- cryMustEqualK solver (Map.keys model) x e
case mbCounter of
Nothing -> go (Map.insert x (K e) done) extra rest
Just ce -> goV ce done extra [] x e rest
-- ce: a counter example to `x = e`
-- done: known improvements
-- extra: known sub-goals
-- todo: more work to process once we are done with `x`.
goV _ done extra todo _ _ [] = go done extra (reverse todo)
goV ce done extra todo x e ((y,e') : more)
-- x = y?
| e == e' = do yesK <- cryMustEqualV solver x y
if yesK then go (Map.insert x (Var y) done)
extra
(reverse todo ++ more)
else tryLR
| otherwise = tryLR
where
next = goV ce done extra ((y,e'):todo) x e more
tryLR =
do mb <- tryLR_with x e y e'
case mb of
Just (r,subGoals) -> go (Map.insert x r done)
(subGoals ++ extra)
(reverse todo ++ more)
Nothing ->
do mb1 <- tryLR_with y e' x e
case mb1 of
Nothing -> next
Just (r, subGoals) -> go (Map.insert y r done)
(subGoals ++ extra)
(reverse todo ++ more)
tryLR_with v1 v1Expr v2 v2Expr =
case ( isUniVar v1
, v1Expr
, v2Expr
, Map.lookup v1 ce
, Map.lookup v2 ce
) of
(True, x1, y1, Just x2, Just y2) ->
cryCheckLinRel solver logger v2 v1 (y1,x1) (y2,x2)
_ -> return Nothing
-- | Try to prove the given expression.
checkUnsat :: SMT.Solver -> SExpr -> IO Bool
checkUnsat s e =
do SMT.push s
SMT.assert s e
res <- SMT.check s
SMT.pop s
return (res == SMT.Unsat)
-- | Try to prove the given expression.
-- If we fail, we try to give a counter example.
-- If the answer is unknown, then we return an empty counter example.
getCounterExample :: SMT.Solver -> [Name] -> SExpr -> IO (Maybe (Map Name Nat'))
getCounterExample s xs e =
do SMT.push s
SMT.assert s e
res <- SMT.check s
ans <- case res of
SMT.Unsat -> return Nothing
SMT.Unknown -> return (Just Map.empty)
SMT.Sat -> Just `fmap` getVals s xs
SMT.pop s
return ans
-- | Is this the only possible value for the constant, under the current
-- assumptions.
-- Assumes that we are in a 'Sat' state.
-- Returns 'Nothing' if the variables must always match the given value.
-- Otherwise, we return a counter-example (which may be empty, if uniknown)
cryMustEqualK :: SMT.Solver -> [Name] ->
Name -> Nat' -> IO (Maybe (Map Name Nat'))
cryMustEqualK solver xs x val =
case val of
Inf -> getCounterExample solver xs (SMT.const (smtFinName x))
Nat n -> getCounterExample solver xs $
SMT.not $
SMT.and (SMT.const $ smtFinName x)
(SMT.eq (SMT.const (smtName x)) (SMT.int n))
-- | Do these two variables need to always be the same, under the current
-- assumptions.
-- Assumes that we are in a 'Sat' state.
cryMustEqualV :: SMT.Solver -> Name -> Name -> IO Bool
cryMustEqualV solver x y =
checkUnsat solver $
SMT.not $
SMT.or (SMT.not (fin x) `SMT.and` SMT.not (fin y))
(fin x `SMT.and` fin y `SMT.and` SMT.eq (var x) (var y))
where fin a = SMT.const (smtFinName a)
var a = SMT.const (smtName a)
-- | Try to find a linear relation between the two variables, based
-- on two observed data points.
-- NOTE: The variable being defined is the SECOND name.
cryCheckLinRel :: SMT.Solver -> SMT.Logger ->
{- x -} Name {- ^ Definition in terms of this variable. -} ->
{- y -} Name {- ^ Define this variable. -} ->
(Nat',Nat') {- ^ Values in one model (x,y) -} ->
(Nat',Nat') {- ^ Values in another model (x,y) -} ->
IO (Maybe (Expr,[Prop]))
{- ^ Either nothing, or an improving expression, and any
additional obligations -}
cryCheckLinRel s logger x y p1 p2 =
-- First, try to find a linear relation that holds in all finite cases.
do SMT.push s
SMT.assert s (isFin x)
SMT.assert s (isFin y)
ans <- case (p1,p2) of
((Nat x1, Nat y1), (Nat x2, Nat y2)) ->
checkLR x1 y1 x2 y2
((Inf, Inf), (Nat x2, Nat y2)) ->
mbGoOn (getFinPt x2) $ \(x1,y1) -> checkLR x1 y1 x2 y2
((Nat x1, Nat y1), (Inf, Inf)) ->
mbGoOn (getFinPt x1) $ \(x2,y2) -> checkLR x1 y1 x2 y2
_ -> return Nothing
SMT.pop s
-- Next, check the infinite cases: if @y = A * x + B@, then
-- either both @x@ and @y@ must be infinite or they both must be finite.
-- Note that we don't consider relations where A = 0: because they
-- would be handled when we checked that @y@ is a constant.
case ans of
Nothing -> return Nothing
Just e ->
do SMT.push s
SMT.assert s (SMT.not (SMT.eq (isFin x) (isFin y)))
c <- SMT.check s
SMT.pop s
case c of
SMT.Unsat -> return (Just e)
_ -> return Nothing
where
isFin a = SMT.const (smtFinName a)
-- XXX: Duplicates `cryDefined`
-- The constraints are always of the form: x >= K, or K >= x
wellDefined e =
case e of
(K (Nat a) :* t) :- K (Nat b) ->
let c = div (b + a - 1) a
in [ t :>= K (Nat c) ]
K (Nat b) :- (K (Nat a) :* t)
-> let c = div b a
in [ K (Nat c) :>= t ]
a :- b -> [ a :>= b ]
_ -> []
checkLR x1 y1 x2 y2 =
do SMT.logMessage logger ("checkLR: " ++ show (x1,y1) ++ " "
++ show (x2,y2))
mbGoOn (return (linRel (x1,y1) (x2,y2))) (\(a,b) ->
do let sumTerm v
| b == 0 = v
| b < 0 = v :- K (Nat (negate b))
| otherwise = v :+ K (Nat b)
expr
| a == 1 = sumTerm (Var x)
| a < 0 = K (Nat b) :- K (Nat (negate a)) :* Var x
| otherwise = sumTerm (K (Nat a) :* Var x)
SMT.logMessage logger ("candidate: " ++ show (ppProp (Var y :==: expr)))
proved <- checkUnsat s
$ propToSmtLib $ crySimplify
$ Not $ Var y :==: expr
if not proved
then SMT.logMessage logger "failed" >> return Nothing
else return (Just (expr,wellDefined expr)))
-- Try to get an example of another point, which is finite, and at
-- different @x@ coordinate.
getFinPt otherX =
do SMT.push s
SMT.assert s (SMT.not (SMT.eq (SMT.const (smtName x)) (SMT.int otherX)))
smtAns <- SMT.check s
ans <- case smtAns of
SMT.Sat ->
do vX <- SMT.getConst s (smtName x)
vY <- SMT.getConst s (smtName y)
case (vX, vY) of
(SMT.Int vx, SMT.Int vy)
| vx >= 0 && vy >= 0 -> return (Just (vx,vy))
_ -> return Nothing
_ -> return Nothing
SMT.pop s
return ans
mbGoOn m k = do ans <- m
case ans of
Nothing -> return Nothing
Just a -> k a
{- | Compute a linear relation through two concrete points.
Try to find a relation of the form @y = a * x + b@.
Depending on the signs of @a@ and @b@, we need additional checks,
to ensure tha @a * x + b@ is valid.
y1 = A * x1 + B
y2 = A * x2 + B
(y2 - y1) = A * (x2 - x1)
A = (y2 - y1) / (x2 - x1)
B = y1 - A * x1
-}
linRel :: (Integer,Integer) {- ^ First point -} ->
(Integer,Integer) {- ^ Second point -} ->
Maybe (Integer,Integer) {- ^ (A,B) -}
linRel (x1,y1) (x2,y2) =
do guard (x1 /= x2)
let (a,r) = divMod (y2 - y1) (x2 - x1)
guard (r == 0 && a /= 0) -- Not interested in A = 0
let b = y1 - a * x1
guard $ not $ a < 0 && b < 0 -- No way this will give a natural number.
return (a,b)

843
src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
View File

@ -1,843 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2014-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- TODO:
-- - Putting in a normal form to spot "prove by assumption"
-- - Additional simplification rules, namely various cancelation.
-- - Things like: lg2 e(x) = x, where we know thate is increasing.
{-# LANGUAGE Safe, PatternGuards, BangPatterns #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Cryptol.TypeCheck.Solver.Numeric.Simplify
(
-- * Simplify a property
crySimplify, crySimplifyMaybe
-- * Simplify expressions in a prop
, crySimpPropExpr, crySimpPropExprMaybe
) where
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
import Cryptol.TypeCheck.Solver.InfNat(genLog,genRoot,rootExact)
import Cryptol.Utils.Misc ( anyJust )
import Control.Monad ( mplus )
import Data.List ( sortBy )
import Data.Maybe ( fromMaybe )
import qualified Data.Set as Set
-- | Simplify a property, if possible.
crySimplify :: Prop -> Prop
crySimplify p = fromMaybe p (crySimplifyMaybe p)
-- | Simplify a property, if possible.
crySimplifyMaybe :: Prop -> Maybe Prop
crySimplifyMaybe p =
let mbSimpExprs = simpSubs p
exprsSimped = fromMaybe p mbSimpExprs
mbRearrange = tryRearrange exprsSimped
rearranged = fromMaybe exprsSimped mbRearrange
in crySimplify `fmap` (crySimpStep rearranged `mplus` mbRearrange
`mplus` mbSimpExprs)
where
tryRearrange q = case q of
_ :&& _ -> cryRearrangeAnd q
_ :|| _ -> cryRearrangeOr q
_ -> Nothing
simpSubs q = case q of
Not a -> Not `fmap` crySimplifyMaybe a
a :&& b -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
return (a' :&& b')
a :|| b -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
return (a' :|| b')
_ -> crySimpPropExprMaybe q
-- | A single simplification step.
crySimpStep :: Prop -> Maybe Prop
crySimpStep prop =
case prop of
Fin x -> cryIsFin x -- Fin only on variables.
x :== y -> Just (cryIsEq x y)
x :> y -> Just (cryIsGt x y)
x :>= y ->
case (x,y) of
-- XXX: DUPLICTION
(K (Nat 0), _) -> Just (y :== zero)
(K (Nat a), Width b) -> Just (K (Nat (2 ^ a)) :>= b)
(_, K (Nat 0)) -> Just PTrue
(Width e, K (Nat b)) -> Just (e :>= K (Nat (2^(b-1))))
(K Inf, _) -> Just PTrue
(_, K Inf) -> Just (x :== inf)
_ -> Just (x :== inf :|| one :+ x :> y)
x :==: y ->
case (x,y) of
(K a, K b) -> Just (if a == b then PTrue else PFalse)
(K (Nat n), _) | Just p <- cryIsNat True n y -> Just p
(_, K (Nat n)) | Just p <- cryIsNat True n x -> Just p
_ | x == y -> Just PTrue
| otherwise -> case (x,y) of
(Var _, _) -> Nothing
(_, Var _) -> Just (y :==: x)
_ -> Nothing
x :>: y ->
case (x,y) of
(K (Nat n),_) | Just p <- cryNatGt True n y -> Just p
(_, K (Nat n)) | Just p <- cryGtNat True n x -> Just p
_ | x == y -> Just PFalse
| otherwise -> Nothing
-- For :&& and :|| we assume that the props have been rearrnaged
p :&& q -> cryAnd p q
p :|| q -> cryOr p q
Not p -> cryNot p
PFalse -> Nothing
PTrue -> Nothing
-- | Rebalance parens, and arrange conjucts so that we can transfer
-- information left-to-right.
cryRearrangeAnd :: Prop -> Maybe Prop
cryRearrangeAnd prop =
case rebalance prop of
Just p -> Just p
Nothing -> cryAnds `fmap` cryRearrange cmpAnd (split prop)
where
rebalance (a :&& b) =
case a of
PFalse -> Just PFalse
PTrue -> Just b
a1 :&& a2 -> Just (a1 :&& (a2 :&& b))
_ -> fmap (a :&&) (rebalance b)
rebalance _ = Nothing
split (a :&& b) = a : split b
split a = [a]
-- | Rebalance parens, and arrange disjuncts so that we can transfer
-- information left-to-right.
cryRearrangeOr :: Prop -> Maybe Prop
cryRearrangeOr prop =
case rebalance prop of
Just p -> Just p
Nothing -> cryOrs `fmap` cryRearrange cmpOr (split prop)
where
rebalance (a :|| b) =
case a of
PFalse -> Just b
PTrue -> Just PTrue
a1 :|| a2 -> Just (a1 :|| (a2 :|| b))
_ -> fmap (a :||) (rebalance b)
rebalance _ = Nothing
split (a :|| b) = a : split b
split a = [a]
-- | Identify propositions that are suiatable for inlining.
cryIsDefn :: Prop -> Maybe (Name, Expr)
cryIsDefn (Var x :==: e) = if (x `Set.member` cryExprFVS e)
then Nothing
else Just (x,e)
cryIsDefn _ = Nothing
type PropOrdering = (Int,Prop) -> (Int,Prop) -> Ordering
{- | Rearrange proposition for conjuctions and disjunctions.
information left-to-right, so we put proposition with information content
on the left.
-}
cryRearrange :: PropOrdering -> [Prop] -> Maybe [Prop]
cryRearrange cmp ps = if ascending keys then Nothing else Just sortedProps
where
-- We tag each proposition with a number, so that later we can tell easily
-- if the propositions got rearranged.
(keys, sortedProps) = unzip (sortBy cmp (zip [ 0 :: Int .. ] ps))
ascending (x : y : zs) = x < y && ascending (y : zs)
ascending _ = True
cmpAnd :: PropOrdering
cmpAnd (k1,prop1) (k2,prop2) =
case (prop1, prop2) of
-- First comes PFalse, maybe we don't need to do anything
(PFalse, PFalse) -> compare k1 k2
(PFalse, _) -> LT
(_,PFalse) -> GT
-- Next comes PTrue
(PTrue, PTrue) -> compare k1 k2
(PTrue, _) -> LT
(_,PTrue) -> GT
-- Next come `not (fin a)` (i.e, a = inf)
(Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
(Not (Fin (Var _)), _) -> LT
(_, Not (Fin (Var _))) -> GT
-- Next come definitions: `x = e` (with `x` not in `fvs e`)
-- XXX: Inefficient, because we keep recomputing free variables
-- (here, and then when actually applying the substitution)
_ | Just (x,_) <- mbL
, Just (y,_) <- mbR -> cmpVars x y
| Just _ <- mbL -> LT
| Just _ <- mbR -> GT
where
mbL = cryIsDefn prop1
mbR = cryIsDefn prop2
-- Next come `fin a`
(Fin (Var x), Fin (Var y)) -> cmpVars x y
(Fin (Var _), _) -> LT
(_, Fin (Var _)) -> GT
-- Everything else stays as is
_ -> compare k1 k2
where
cmpVars x y
| x < y = LT
| x > y = GT
| otherwise = compare k1 k2
cmpOr :: PropOrdering
cmpOr (k1,prop1) (k2,prop2) =
case (prop1, prop2) of
-- First comes PTrue, maybe we don't need to do anything
(PTrue, PTrue) -> compare k1 k2
(PTrue, _) -> LT
(_,PTrue) -> GT
-- Next comes PFalse
(PFalse, PFalse) -> compare k1 k2
(PFalse, _) -> LT
(_,PFalse) -> GT
-- Next comes `fin a` (because we propagete `a = inf`)
(Fin (Var x), Fin (Var y)) -> cmpVars x y
(Fin (Var _), _) -> LT
(_, Fin (Var _)) -> GT
-- Next come `not (fin a)` (i.e, propagete (fin a))
(Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
(Not (Fin (Var _)), _) -> LT
(_, Not (Fin (Var _))) -> GT
-- we don't propagete (x /= e) for now.
-- Everything else stays as is
_ -> compare k1 k2
where
cmpVars x y
| x < y = LT
| x > y = GT
| otherwise = compare k1 k2
-- | Simplification of ':&&'.
-- Assumes arranged conjucntions.
-- See 'cryRearrangeAnd'.
cryAnd :: Prop -> Prop -> Maybe Prop
cryAnd p q =
case p of
PTrue -> Just q
PFalse -> Just PFalse
Not (Fin (Var x))
| Just q' <- cryKnownFin x False q -> Just (p :&& q')
Fin (Var x)
| Just q' <- cryKnownFin x True q -> Just (p :&& q')
_ | Just (x,e) <- cryIsDefn p
, Just q' <- cryLet x e q
-> Just (p :&& q')
_ -> Nothing
-- | Simplification of ':||'.
-- Assumes arranged disjunctions.
-- See 'cryRearrangeOr'
cryOr :: Prop -> Prop -> Maybe Prop
cryOr p q =
case p of
PTrue -> Just PTrue
PFalse -> Just q
Fin (Var x)
| Just q' <- cryKnownFin x False q -> Just (p :|| q')
Not (Fin (Var x))
| Just q' <- cryKnownFin x True q -> Just (p :|| q')
_ -> Nothing
-- | Propagate the fact that the variable is known to be finite ('True')
-- or not-finite ('False').
-- Note that this may introduce new expression redexes.
cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
cryKnownFin a isFin prop =
case prop of
Fin (Var a') | a == a' -> Just (if isFin then PTrue else PFalse)
p :&& q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
return (p' :&& q')
p :|| q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
return (p' :|| q')
Not p -> Not `fmap` cryKnownFin a isFin p
x :==: y
| not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-> Just (cryNatOp (:==:) x' y')
x :>: y
| not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-> Just (cryNatOp (:>:) x' y')
-- All the other cases should be simplified, eventually.
_ -> Nothing
-- | Negation.
cryNot :: Prop -> Maybe Prop
cryNot prop =
case prop of
Fin _ -> Nothing
x :== y -> Just (x :> y :|| y :> x)
x :>= y -> Just (y :> x)
x :> y -> Just (y :>= x)
x :==: y -> Just (x :>: y :|| y :>: x)
_ :>: _ -> Nothing
p :&& q -> Just (Not p :|| Not q)
p :|| q -> Just (Not p :&& Not q)
Not p -> Just p
PFalse -> Just PTrue
PTrue -> Just PFalse
-- | Simplificaiton for @:==@
cryIsEq :: Expr -> Expr -> Prop
cryIsEq l r =
case (l,r) of
(K m, K n) -> if m == n then PTrue else PFalse
(K Inf, _) -> Not (Fin r)
(_, K Inf) -> Not (Fin l)
(Div x y, z) -> x :>= z :* y :&& (one :+ z) :* y :> x
(K (Nat n),_) | Just p <- cryIsNat False n r -> p
(_,K (Nat n)) | Just p <- cryIsNat False n l -> p
_ -> Not (Fin l) :&& Not (Fin r)
:|| Fin l :&& Fin r :&& cryNatOp (:==:) l r
-- | Simplificatoin for @:>@
cryIsGt :: Expr -> Expr -> Prop
cryIsGt (K m) (K n) = if m > n then PTrue else PFalse
cryIsGt (K (Nat n)) e | Just p <- cryNatGt False n e = p
cryIsGt e (K (Nat n)) | Just p <- cryGtNat False n e = p
cryIsGt x y = Fin y :&& (x :== inf :||
Fin x :&& cryNatOp (:>:) x y)
-- | Attempt to simplify a @fin@ constraint.
-- Assumes a defined input.
cryIsFin :: Expr -> Maybe Prop
cryIsFin expr =
case expr of
K Inf -> Just PFalse
K (Nat _) -> Just PTrue
Var _ -> Nothing
t1 :+ t2 -> Just (Fin t1 :&& Fin t2)
t1 :- _ -> Just (Fin t1)
t1 :* t2 -> Just ( Fin t1 :&& Fin t2
:|| t1 :== zero :&& t2 :== inf
:|| t2 :== zero :&& t1 :== inf
)
Div t1 _ -> Just (Fin t1)
Mod _ _ -> Just PTrue
t1 :^^ t2 ->
Just ( Fin t1 :&& Fin t2
:|| t1 :== inf :&& t2 :== zero -- inf ^^ 0
:|| t2 :== inf :&& (t1 :== zero :|| t1 :== one)
-- 0 ^^ inf, 1 ^^ inf
)
Min t1 t2 -> Just (Fin t1 :|| Fin t2)
Max t1 t2 -> Just (Fin t1 :&& Fin t2)
Width t1 -> Just (Fin t1)
LenFromThen _ _ _ -> Just PTrue
LenFromThenTo _ _ _ -> Just PTrue
cryIsNat :: Bool -> Integer -> Expr -> Maybe Prop
cryIsNat useFinite n expr =
case expr of
K Inf -> Just PFalse
K (Nat m) -> Just (if m == n then PTrue else PFalse)
Var _ | useFinite -> Nothing
| otherwise -> Just (Fin expr :&& expr :==: K (Nat n))
K (Nat m) :+ e2 -> Just $ if m > n then PFalse
else eq e2 $ K $ Nat $ n - m
x :+ y
| n == 0 -> Just (eq x zero :&& eq y zero)
| n == 1 -> Just (eq x zero :&& eq y one :||
eq x one :&& eq y zero)
| otherwise -> Nothing
e1 :- e2 -> Just $ eq (K (Nat n) :+ e2) e1
K (Nat m) :* e2 ->
Just $ if m == 0
then if n == 0 then PTrue else PFalse
else case divMod n m of
(q,r) -> if r == 0 then eq e2 (K (Nat q))
else PFalse
e1 :* e2
| n == 0 -> Just (eq e1 zero :|| eq e2 zero)
| n == 1 -> Just (eq e1 one :&& eq e2 one)
| otherwise -> Nothing
-- (x >= n * y) /\ ((n+1) * y > x)
Div x y -> Just (gt (one :+ x) (K (Nat n) :* y) :&&
gt (K (Nat (n + 1)) :* y) x)
Mod _ _ | useFinite -> Nothing
| otherwise -> Just (cryNatOp (:==:) expr (K (Nat n)))
K (Nat m) :^^ y -> Just $ case genLog n m of
Just (a, exact)
| exact -> eq y (K (Nat a))
_ -> PFalse
x :^^ K (Nat m) -> Just $ case rootExact n m of
Just a -> eq x (K (Nat a))
Nothing -> PFalse
x :^^ y
| n == 0 -> Just (eq x zero :&& gt y zero)
| n == 1 -> Just (eq x one :|| eq y zero)
| otherwise -> Nothing
Min x y
| n == 0 -> Just (eq x zero :|| eq y zero)
| otherwise -> Just ( eq x (K (Nat n)) :&& gt y (K (Nat (n - 1)))
:|| eq y (K (Nat n)) :&& gt x (K (Nat (n - 1)))
)
Max x y -> Just ( eq x (K (Nat n)) :&& gt (K (Nat (n + 1))) y
:|| eq y (K (Nat n)) :&& gt (K (Nat (n + 1))) y
)
Width x
| n == 0 -> Just (eq x zero)
| otherwise -> Just (gt x (K (Nat (2^(n-1) - 1))) :&&
gt (K (Nat (2 ^ n))) x)
LenFromThen x y w
| n == 0 -> Just PFalse
-- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
| n == 1 -> Just (gt y x :&& gt (y :+ one) (two :^^ w))
| otherwise -> Nothing -- XXX: maybe some more?
-- See `nLenFromThenTo` in 'Cryptol.TypeCheck.Solver.InfNat'
LenFromThenTo x y z
| n == 0 -> Just ( gt x y :&& gt z x
:|| gt y x :&& gt x z
)
-- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
| n == 1 -> Just (gt z y :&& gt (x :+ one) z :||
gt y z :&& gt (z :+ one) x)
| otherwise -> Nothing -- XXX: maybe some more?
where
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
-- | Constant > expression
cryNatGt :: Bool -> Integer -> Expr -> Maybe Prop
cryNatGt useFinite n expr
| n == 0 = Just PFalse
| n == 1 = Just (eq expr zero)
| otherwise =
case expr of
K x -> Just $ if Nat n > x then PTrue else PFalse
Var _ -> Nothing
K (Nat m) :+ y -> Just $ if n >= m then gt (k (n - m)) y else PFalse
_ :+ _ -> Nothing
x :- y -> Just $ gt (k n :+ y) x
K (Nat m) :* y
| m == 0 -> Just PTrue -- because we know that n > 1
| otherwise -> Just $ case divMod n m of
(q,0) -> gt (k q) y
(0,_) -> eq y zero
(q,_) -> gt (k (q + 1)) y
_ :* _ -> Nothing
Div x y -> Just $ gt (k n :* y) x
Mod _ (K (Nat m))
| m <= n -> Just PTrue
Mod (K (Nat m)) _
| m < n -> Just PTrue
Mod _ _ -> Nothing
K (Nat m) :^^ y
| m == 0 -> Just PTrue -- because n > 1
| m == 1 -> Just PTrue -- ditto
| otherwise -> do (a,exact) <- genLog n m
return $ if exact
then gt (k a) y
else gt (k (a + 1)) y
x :^^ K (Nat m)
| m == 0 -> Just PTrue
| m == 1 -> Just (gt (k n) x)
| otherwise -> do (a,exact) <- genRoot n m
return $ if exact
then gt (k a) x
else gt (k (a + 1)) x
_ :^^ _ -> Nothing
Min x y -> Just $ gt (k n) x :|| gt (k n) y
Max x y -> Just $ gt (k n) x :&& gt (k n) y
Width x -> Just $ gt (k (2 ^ n)) x
LenFromThen _ _ _ -> Nothing -- Are there some rules?
LenFromThenTo _ _ _ -> Nothing -- Are there some rulesj
where
k x = K (Nat x)
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
-- | Expression > constant
cryGtNat :: Bool -> Integer -> Expr -> Maybe Prop
cryGtNat useFinite n expr =
case expr of
K x -> Just $ if x > Nat n then PTrue else PFalse
Var _ -> Nothing
K (Nat m) :+ y
| m > n -> Just PTrue
| otherwise -> Just (gt y (K (Nat (n - m))))
x :+ y
| n == 0 -> Just (gt x zero :|| gt y zero)
| otherwise -> Nothing
x :- y -> Just $ gt x (K (Nat n) :+ y)
K (Nat m) :* y
| m > 0 -> Just $ case divMod n m of
(a,_) -> gt y $ K $ Nat a
x :* y
| n == 0 -> Just (gt x zero :&& gt y zero)
| otherwise -> Nothing
Div x y -> Just $ gt (one :+ x) (K (Nat (n+1)) :* y)
Mod _ (K (Nat m))
| m <= n -> Just PFalse
Mod (K (Nat m)) _
| m < n -> Just PFalse
Mod _ _ -> Nothing
K (Nat m) :^^ y
| m == 0 -> Just $ if n == 0 then eq y zero else PFalse
| m == 1 -> Just $ if n == 0 then PTrue else PFalse
| otherwise -> do (a,_exact) <- genLog n m
Just (gt y (K (Nat a)))
x :^^ K (Nat m)
| m == 0 -> Just $ if n == 0 then PTrue else PFalse
| m == 1 -> Just $ gt x (K (Nat n))
| otherwise -> do (a,exact) <- genRoot n m
Just $ if exact
then gt x (K (Nat a))
else gt (one :+ x) (K (Nat (a+1)))
x :^^ y
| n == 0 -> Just (gt x zero :|| eq y zero)
| otherwise -> Nothing
Min x y -> Just $ gt x (K (Nat n)) :&& gt y (K (Nat n))
Max x y -> Just $ gt x (K (Nat n)) :|| gt y (K (Nat n))
Width x -> Just $ gt (one :+ x) (K (Nat (2 ^ n)))
LenFromThen _ _ _
| n == 0 -> Just PTrue
| otherwise -> Nothing -- Are there some rules?
LenFromThenTo x y z
| n == 0 -> Just (gt x y :&& gt z x :|| gt y x :&& gt x z)
| otherwise -> Nothing
where
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
-- | Simplify only the Expr parts of a Prop.
crySimpPropExpr :: Prop -> Prop
crySimpPropExpr p = fromMaybe p (crySimpPropExprMaybe p)
-- | Simplify only the Expr parts of a Prop.
-- Returns `Nothing` if there were no changes.
crySimpPropExprMaybe :: Prop -> Maybe Prop
crySimpPropExprMaybe prop =
case prop of
Fin e -> Fin `fmap` crySimpExprMaybe e
a :== b -> binop crySimpExprMaybe (:== ) a b
a :>= b -> binop crySimpExprMaybe (:>= ) a b
a :> b -> binop crySimpExprMaybe (:> ) a b
a :==: b -> binop crySimpExprMaybe (:==:) a b
a :>: b -> binop crySimpExprMaybe (:>: ) a b
a :&& b -> binop crySimpPropExprMaybe (:&&) a b
a :|| b -> binop crySimpPropExprMaybe (:||) a b
Not p -> Not `fmap` crySimpPropExprMaybe p
PFalse -> Nothing
PTrue -> Nothing
where
binop simp f l r =
case (simp l, simp r) of
(Nothing,Nothing) -> Nothing
(l',r') -> Just (f (fromMaybe l l') (fromMaybe r r'))
-- | Our goal is to bubble @inf@ terms to the top of @Return@.
cryNoInf :: Expr -> IfExpr Expr
cryNoInf expr =
case expr of
-- These are the interesting cases where we have to branch
x :* y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, K Inf) -> return inf
(K Inf, _) -> mkIf (y' :==: zero) (return zero) (return inf)
(_, K Inf) -> mkIf (x' :==: zero) (return zero) (return inf)
_ -> return (x' :* y')
x :^^ y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, K Inf) -> return inf
(K Inf, _) -> mkIf (y' :==: zero) (return one) (return inf)
(_, K Inf) -> mkIf (x' :==: zero) (return zero)
$ mkIf (x' :==: one) (return one)
$ return inf
_ -> return (x' :^^ y')
-- The rest just propagates
K _ -> return expr
Var _ -> return expr
x :+ y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> return inf
(_, K Inf) -> return inf
_ -> return (x' :+ y')
x :- y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(_, K Inf) -> Impossible
(K Inf, _) -> return inf
_ -> mkIf (x' :==: y)
(return zero)
(mkIf (x' :>: y) (return (x' :- y'))
Impossible)
Div x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> Impossible
(_, K Inf) -> return zero
_ -> mkIf (y' :>: zero) (return (Div x' y')) Impossible
Mod x y ->
do x' <- cryNoInf x
-- `Mod x y` is finite, even if `y` is `inf`, so first check
-- for finiteness.
mkIf (Fin y)
(do y' <- cryNoInf y
case (x',y') of
(K Inf, _) -> Impossible
(_, K Inf) -> Impossible
_ -> mkIf (y' :>: zero) (return (Mod x' y')) Impossible
)
(return x')
Min x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x',y') of
(K Inf, _) -> return y'
(_, K Inf) -> return x'
_ -> return (Min x' y')
Max x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> return inf
(_, K Inf) -> return inf
_ -> return (Max x' y')
Width x ->
do x' <- cryNoInf x
case x' of
K Inf -> return inf
_ -> return (Width x')
LenFromThen x y w -> fun3 LenFromThen x y w
LenFromThenTo x y z -> fun3 LenFromThenTo x y z
where
fun3 f x y z =
do x' <- cryNoInf x
y' <- cryNoInf y
z' <- cryNoInf z
case (x',y',z') of
(K Inf, _, _) -> Impossible
(_, K Inf, _) -> Impossible
(_, _, K Inf) -> Impossible
_ -> mkIf (x' :==: y') Impossible
(return (f x' y' z'))
mkIf p t e = case crySimplify p of
PTrue -> t
PFalse -> e
p' -> If p' t e
-- | Make an expression that should work ONLY on natural nubers.
-- Eliminates occurances of @inf@.
-- Assumes that the two input expressions are well-formed and finite.
-- The expression is constructed by the given function.
cryNatOp :: (Expr -> Expr -> Prop) -> Expr -> Expr -> Prop
cryNatOp op x y =
toProp $
do x' <- noInf x
y' <- noInf y
return (op x' y')
where
noInf a = do a' <- cryNoInf a
case a' of
K Inf -> Impossible
_ -> return a'
toProp ite =
case ite of
Impossible -> PFalse -- It doesn't matter, but @false@ might anihilate.
Return p -> p
If p t e -> p :&& toProp t :|| Not p :&& toProp e

213
src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs
View File

@ -1,213 +0,0 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2015-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Simplification of expressions.
-- The result of simplifying an expression `e`, is a new expression `e'`,
-- which satisfies the property:
--
-- if e is well-defined then e and e' will evaluate to the same type.
--
{-# LANGUAGE Safe, BangPatterns #-}
module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr where
import Cryptol.TypeCheck.Solver.Numeric.AST
import qualified Cryptol.TypeCheck.Solver.InfNat as IN
import Cryptol.Utils.Misc ( anyJust )
import Control.Monad ( guard )
import Data.Maybe ( fromMaybe, maybeToList )
import qualified Data.Map as Map
-- | Simplify an expression, if possible.
crySimpExpr :: Expr -> Expr
crySimpExpr expr = fromMaybe expr (crySimpExprMaybe expr)
-- | Perform simplification from the leaves up.
-- Returns `Nothing` if there were no changes.
crySimpExprMaybe :: Expr -> Maybe Expr
crySimpExprMaybe expr =
case crySimpExprStep (fromMaybe expr mbE1) of
Nothing -> mbE1
Just e2 -> Just (fromMaybe e2 (crySimpExprMaybe e2))
where
mbE1 = cryRebuildExpr expr `fmap` anyJust crySimpExprMaybe (cryExprExprs expr)
-- XXX: Add rules to group together occurances of variables
data Sign = Pos | Neg deriving Show
otherSign :: Sign -> Sign
otherSign s = case s of
Pos -> Neg
Neg -> Pos
signed :: Sign -> Integer -> Integer
signed s = case s of
Pos -> id
Neg -> negate
splitSum :: Expr -> [(Sign,Expr)]
splitSum e0 = go Pos e0 []
where go s (e1 :+ e2) es = go s e1 (go s e2 es)
go s (e1 :- e2) es = go s e1 (go (otherSign s) e2 es)
go s e es = (s,e) : es
normSum :: Expr -> Expr
normSum = posTerm . go 0 Map.empty Nothing . splitSum
where
-- constants, variables, other terms
go !_ !_ !_ ((Pos,K Inf) : _) = (Pos, K Inf)
go k xs t ((s, K (Nat n)) : es) = go (k + signed s n) xs t es
go k xs t ((s, Var x) : es) = go k (Map.insertWith (+) x (signed s 1) xs) t es
go k xs t ((s, K (Nat n) :* Var x) : es)
| n == 0 = go k xs t es
| otherwise = go k (Map.insertWith (+) x (signed s n) xs) t es
go k xs Nothing (e : es) = go k xs (Just e) es
go k xs (Just e1) (e2 : es) = go k xs (Just (add e1 e2)) es
go k xs t [] =
let terms = constTerm k
++ concatMap varTerm (Map.toList xs)
++ maybeToList t
in case terms of
[] -> (Pos, K (Nat 0))
ts -> foldr1 add ts
constTerm k
| k == 0 = []
| k > 0 = [ (Pos, K (Nat k)) ]
| otherwise = [ (Neg, K (Nat (negate k))) ]
varTerm (x,k)
| k == 0 = []
| k == 1 = [ (Pos, Var x) ]
| k > 0 = [ (Pos, K (Nat k) :* Var x) ]
| k == (-1) = [ (Neg, Var x) ]
| otherwise = [ (Neg, K (Nat (negate k)) :* Var x) ]
add (s1,t1) (s2,t2) =
case (s1,s2) of
(Pos,Pos) -> (Pos, t1 :+ t2)
(Pos,Neg) -> (Pos, t1 :- t2)
(Neg,Pos) -> (Pos, t2 :- t1)
(Neg,Neg) -> (Neg, t1 :+ t2)
posTerm (Pos,x) = x
posTerm (Neg,x) = K (Nat 0) :- x
crySimpExprStep :: Expr -> Maybe Expr
crySimpExprStep e =
case crySimpExprStep1 e of
Just e1 -> Just e1
Nothing -> do let e1 = normSum e
guard (e /= e1)
return e1
-- | Make a simplification step, assuming the expression is well-formed.
crySimpExprStep1 :: Expr -> Maybe Expr
crySimpExprStep1 expr =
case expr of
K _ -> Nothing
Var _ -> Nothing
_ :+ _ -> Nothing
_ :- _ -> Nothing
x :* y ->
case (x,y) of
(K (Nat 0), _) -> Just zero
(K (Nat 1), _) -> Just y
(K a, K b) -> Just (K (IN.nMul a b))
(_, K _) -> Just (y :* x)
(K a, K b :* z) -> Just (K (IN.nMul a b) :* z)
-- Normalize, somewhat
(a :* b, _) -> Just (a :* (b :* y))
(Var a, Var b)
| b > a -> Just (y :* x)
_ -> Nothing
Div x y ->
case (x,y) of
(K (Nat 0), _) -> Just zero
(_, K (Nat 1)) -> Just x
(_, K Inf) -> Just zero
(K a, K b) -> K `fmap` IN.nDiv a b
_ | x == y -> Just one
_ -> Nothing
Mod x y ->
case (x,y) of
(K (Nat 0), _) -> Just zero
(_, K Inf) -> Just x
(_, K (Nat 1)) -> Just zero
(K a, K b) -> K `fmap` IN.nMod a b
_ -> Nothing
x :^^ y ->
case (x,y) of
(_, K (Nat 0)) -> Just one
(_, K (Nat 1)) -> Just x
(K (Nat 1), _) -> Just one
(K a, K b) -> Just (K (IN.nExp a b))
_ -> Nothing
Min x y ->
case (x,y) of
(K (Nat 0), _) -> Just zero
(K Inf, _) -> Just y
(_, K (Nat 0)) -> Just zero
(_, K Inf) -> Just x
(K a, K b) -> Just (K (IN.nMin a b))
_ | x == y -> Just x
_ -> Nothing
Max x y ->
case (x,y) of
(K (Nat 0), _) -> Just y
(K Inf, _) -> Just inf
(_, K (Nat 0)) -> Just x
(_, K Inf) -> Just inf
(K a, K b) -> Just (K (IN.nMax a b))
_ | x == y -> Just x
_ -> Nothing
Width x ->
case x of
K a -> Just (K (IN.nWidth a))
K (Nat 2) :^^ e -> Just (one :+ e)
K (Nat 2) :^^ e :- K (Nat 1) -> Just e
_ -> Nothing
LenFromThen x y w ->
case (x,y,w) of
(K a, K b, K c) -> K `fmap` IN.nLenFromThen a b c
_ -> Nothing
LenFromThenTo x y z ->
case (x,y,z) of
(K a, K b, K c) -> K `fmap` IN.nLenFromThenTo a b c
_ -> Nothing

257
src/Cryptol/TypeCheck/Solver/SMT.hs
View File

@ -1,5 +1,31 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2013-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
{-# Language FlexibleInstances #-}
module Cryptol.TypeCheck.Solver.SMT (proveImp,checkUnsolvable) where
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.TypeCheck.Solver.SMT
( -- * Setup
Solver
, withSolver
-- * Debugging
, debugBlock
, debugLog
-- * Proving stuff
, proveImp
, checkUnsolvable
, tryGetModel
) where
import SimpleSMT (SExpr)
import qualified SimpleSMT as SMT
@ -9,64 +35,229 @@ import qualified Data.Set as Set
import Data.Maybe(catMaybes)
import Data.List(partition)
import Control.Monad(msum,zipWithM)
import Data.Char(isSpace)
import Text.Read(readMaybe)
import qualified System.IO.Strict as StrictIO
import System.FilePath((</>))
import System.Directory(doesFileExist)
import Cryptol.Prelude(cryptolTcContents)
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.CrySAT
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
import Cryptol.TypeCheck.Subst(Subst, emptySubst, listSubst)
import Cryptol.Utils.Panic
import Cryptol.Utils.PP -- ( Doc )
-- | An SMT solver packed with a logger for debugging.
data Solver = Solver
{ solver :: SMT.Solver
-- ^ The actual solver
, logger :: SMT.Logger
-- ^ For debugging
}
-- | Execute a computation with a fresh solver instance.
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver SolverConfig { .. } k =
do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
let smtDbg = if solverVerbose > 1 then Just logger else Nothing
solver <- SMT.newSolver solverPath solverArgs smtDbg
_ <- SMT.setOptionMaybe solver ":global-decls" "false"
-- SMT.setLogic solver "QF_LIA"
let sol = Solver { .. }
loadTcPrelude sol solverPreludePath
a <- k sol
_ <- SMT.stop solver
return a
where
quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
, SMT.logLevel = return 0
, SMT.logSetLevel= \_ -> return ()
, SMT.logTab = return ()
, SMT.logUntab = return ()
}
-- | Load the definitions used for type checking.
loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()
loadTcPrelude s [] = loadString s cryptolTcContents
loadTcPrelude s (p : ps) =
do let file = p </> "CryptolTC.z3"
yes <- doesFileExist file
if yes then loadFile s file
else loadTcPrelude s ps
loadFile :: Solver -> FilePath -> IO ()
loadFile s file = loadString s =<< StrictIO.readFile file
loadString :: Solver -> String -> IO ()
loadString s str = go (dropComments str)
where
go txt
| all isSpace txt = return ()
| otherwise =
case SMT.readSExpr txt of
Just (e,rest) -> SMT.command (solver s) e >> go rest
Nothing -> panic "loadFile" [ "Failed to parse SMT file."
, txt
]
dropComments = unlines . map dropComment . lines
dropComment xs = case break (== ';') xs of
(as,_:_) -> as
_ -> xs
--------------------------------------------------------------------------------
-- Debugging
debugBlock :: Solver -> String -> IO a -> IO a
debugBlock s@Solver { .. } name m =
do debugLog s name
SMT.logTab logger
a <- m
SMT.logUntab logger
return a
class DebugLog t where
debugLog :: Solver -> t -> IO ()
debugLogList :: Solver -> [t] -> IO ()
debugLogList s ts = case ts of
[] -> debugLog s "(none)"
_ -> mapM_ (debugLog s) ts
instance DebugLog Char where
debugLog s x = SMT.logMessage (logger s) (show x)
debugLogList s x = SMT.logMessage (logger s) x
instance DebugLog a => DebugLog [a] where
debugLog = debugLogList
instance DebugLog a => DebugLog (Maybe a) where
debugLog s x = case x of
Nothing -> debugLog s "(nothing)"
Just a -> debugLog s a
instance DebugLog Doc where
debugLog s x = debugLog s (show x)
instance DebugLog Type where
debugLog s x = debugLog s (pp x)
instance DebugLog Goal where
debugLog s x = debugLog s (goal x)
instance DebugLog Subst where
debugLog s x = debugLog s (pp x)
--------------------------------------------------------------------------------
-- | Returns goals that were not proved
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp sol ps gs0 =
debugBlock sol "PROVE IMP" $
do let s = rawSolver sol
let (gs,rest) = partition (isNumeric . goal) gs0
numAsmp = filter isNumeric ps
do let gs1 = concatMap flatGoal gs0
(gs,rest) = partition (isNumeric . goal) gs1
numAsmp = filter isNumeric (concatMap pSplitAnd ps)
vs = Set.toList (fvs (numAsmp, map goal gs))
tvs <- debugBlock sol "VARIABLES" $
do SMT.push s
Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
do SMT.push (solver sol)
Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] vs
debugBlock sol "ASSUMPTIONS" $
mapM_ (assume s tvs) numAsmp
mapM_ (assume sol tvs) numAsmp
gs' <- mapM (prove sol tvs) gs
SMT.pop s
SMT.pop (solver sol)
return (catMaybes gs' ++ rest)
-- | Check if the given goals are known to be unsolvable.
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable sol gs0 =
debugBlock sol "CHECK UNSOLVABLE" $
do let s = rawSolver sol
ps = filter isNumeric (map goal gs0)
do let ps = filter isNumeric
$ map goal
$ concatMap flatGoal gs0
vs = Set.toList (fvs ps)
tvs <- debugBlock sol "VARIABLES" $
do SMT.push s
Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
do push sol
Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] vs
ans <- unsolvable sol tvs ps
SMT.pop s
pop sol
return ans
tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe Subst)
tryGetModel sol as ps =
do push sol
tvs <- Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] as
mapM_ (assume sol tvs) ps
sat <- SMT.check (solver sol)
su <- case sat of
SMT.Sat ->
case as of
[] -> return (Just emptySubst)
_ -> do res <- SMT.getExprs (solver sol) (Map.elems tvs)
let parse x = do e <- Map.lookup x tvs
t <- parseNum =<< lookup e res
return (x, t)
return (listSubst <$> mapM parse as)
_ -> return Nothing
pop sol
return su
where
parseNum a
| SMT.Other s <- a
, SMT.List [con,val,isFin,isErr] <- s
, SMT.Atom "mk-infnat" <- con
, SMT.Atom "false" <- isErr
, SMT.Atom fin <- isFin
, SMT.Atom v <- val
, Just n <- readMaybe v
= Just (if fin == "false" then tInf else tNum (n :: Integer))
parseNum _ = Nothing
--------------------------------------------------------------------------------
declareVar :: SMT.Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar s x v = do let name = (if isFreeTV v then "fv" else "kv") ++ show x
e <- SMT.declare s name cryInfNat
SMT.assert s (SMT.fun "cryVar" [ e ])
push :: Solver -> IO ()
push sol = SMT.push (solver sol)
pop :: Solver -> IO ()
pop sol = SMT.pop (solver sol)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar s x v =
do let name = (if isFreeTV v then "fv" else "kv") ++ show x
e <- SMT.declare (solver s) name cryInfNat
SMT.assert (solver s) (SMT.fun "cryVar" [ e ])
return (v,e)
assume :: SMT.Solver -> TVars -> Prop -> IO ()
assume s tvs p = SMT.assert s (SMT.fun "cryAssume" [ toSMT tvs p ])
assume :: Solver -> TVars -> Prop -> IO ()
assume s tvs p = SMT.assert (solver s) (SMT.fun "cryAssume" [ toSMT tvs p ])
prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
prove sol tvs g =
debugBlock sol "PROVE" $
do let s = rawSolver sol
SMT.push s
do let s = solver sol
push sol
SMT.assert s (SMT.fun "cryProve" [ toSMT tvs (goal g) ])
res <- SMT.check s
SMT.pop s
pop sol
case res of
SMT.Unsat -> return Nothing
_ -> return (Just g)
@ -76,11 +267,10 @@ prove sol tvs g =
unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
unsolvable sol tvs ps =
debugBlock sol "UNSOLVABLE" $
do let s = rawSolver sol
SMT.push s
mapM_ (assume s tvs) ps
res <- SMT.check s
SMT.pop s
do SMT.push (solver sol)
mapM_ (assume sol tvs) ps
res <- SMT.check (solver sol)
SMT.pop (solver sol)
case res of
SMT.Unsat -> return True
_ -> return False
@ -89,13 +279,18 @@ unsolvable sol tvs ps =
--------------------------------------------------------------------------------
-- | Split up the 'And' in a goal
flatGoal :: Goal -> [Goal]
flatGoal g = [ g { goal = p } | p <- pSplitAnd (goal g) ]
-- | Assumes no 'And'
isNumeric :: Prop -> Bool
isNumeric ty = matchDefault False
$ msum [ is (|=|), is (|>=|), is aFin, is aTrue, andNum ty ]
isNumeric ty = matchDefault False $ msum [ is (|=|), is (|>=|), is aFin ]
where
andNum t = anAdd t >>= \(x,y) -> return (isNumeric x && isNumeric y)
is f = f ty >> return True
--------------------------------------------------------------------------------
type TVars = Map TVar SExpr

6
tests/issues/issue002.icry.stdout
View File

@ -1,4 +1,4 @@
Loading module Cryptol
(5, True).0 : {a} (fin a, a >= 3) => [a]
((5, True), False).0 : {a} (fin a, a >= 3) => ([a], Bit)
(((5, True), False).0).0 : {a} (fin a, a >= 3) => [a]
(5, True).0 : {a} (a >= 3, fin a) => [a]
((5, True), False).0 : {a} (a >= 3, fin a) => ([a], Bit)
(((5, True), False).0).0 : {a} (a >= 3, fin a) => [a]

4
tests/issues/padding.icry.stdout
View File

@ -1,6 +1,6 @@
Loading module Cryptol
Assuming a = 5
Assuming a = inf
Assuming b = 5
[[0x01, 0x02, 0x03, 0x04, 0x05], [0x06, 0x07, 0x08, 0x09, 0x0a],
[0x0b, 0x0c, 0x0d, 0x0e, 0x0f], [0x10, 0x11, 0x12, 0x13, 0x14],
[0x15, 0x16, 0x17, 0x18, 0x00]]
[0x15, 0x16, 0x17, 0x18, 0x00], ...]

4
tests/mono-binds/test03.icry.stdout
View File

@ -9,8 +9,8 @@ test03::test = \{a} (fin a, a >= width a) ->
test03::foo a <> <>
where
/* Not recursive */
test03::foo : {b} (fin b, b >= width a) => [b]
test03::foo = \{b} (fin b, b >= width a) ->
test03::foo : {b} (b >= width a, fin b) => [b]
test03::foo = \{b} (b >= width a, fin b) ->
Cryptol::demote a b <> <> <>

4
tests/mono-binds/test04.icry.stdout
View File

@ -4,8 +4,8 @@ Loading module test04
module test04
import Cryptol
/* Not recursive */
test04::test : {a, b} (fin b, b >= 4) => a -> ((a, ()), (a, [b]))
test04::test = \{a, b} (fin b, b >= 4) (a : a) ->
test04::test : {a, b} (b >= 4, fin b) => a -> ((a, ()), (a, [b]))
test04::test = \{a, b} (b >= 4, fin b) (a : a) ->
(test04::f () (), test04::f [b] (Cryptol::demote 10 b <> <> <>))
where
/* Not recursive */

8
tests/mono-binds/test05.icry.stdout
View File

@ -14,8 +14,8 @@ test05::foo : [10]
test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */
test05::test : {a, b, c} (Zero b, fin c, c >= 4) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, fin c, c >= 4) (a : [a]b) ->
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
Cryptol::demote 10 c <> <> <>
where
/* Not recursive */
@ -60,8 +60,8 @@ test05::foo : [10]
test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */
test05::test : {a, b, c} (Zero b, fin c, c >= 4) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, fin c, c >= 4) (a : [a]b) ->
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
Cryptol::demote 10 c <> <> <>
where
/* Not recursive */