mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Improve non-linear story a bit; eliminate SMTProp
This commit is contained in:
Iavor S. Diatchki
parent
a595948099
commit
b9bdc391b4
@ -30,9 +30,10 @@ library
|
||||
directory >= 1.2,
|
||||
executable-path >= 0.0.3,
|
||||
filepath >= 1.3,
|
||||
generic-trie >= 0.2,
|
||||
GraphSCC >= 1.0.4,
|
||||
monadLib >= 3.7.2,
|
||||
mtl >= 2.2.1,
|
||||
mtl,
|
||||
old-time >= 1.1,
|
||||
presburger >= 1.1,
|
||||
pretty >= 1.1,
|
||||
|
||||
@ -158,13 +158,13 @@ simpGoals s gs0 =
|
||||
do debugBlock s "possibly not defined" $
|
||||
mapM_ (debugLog s . show . pp . goal . fst) nonDef
|
||||
debugBlock s "defined" $
|
||||
mapM_ (debugLog s . ($ "") . SMT.showsSExpr . Num.smtpLinPart) def
|
||||
mapM_ (debugLog s . show . Num.ppProp . Num.dpSimpExprProp) def
|
||||
|
||||
let (su,extraProps) = importSplitImps varMap imps
|
||||
|
||||
let def1 = eliminateSimpleGEQ def
|
||||
toGoal =
|
||||
case map (fst . fst . Num.smtpOther) def1 of
|
||||
case map (fst . Num.dpData) def1 of
|
||||
[g] -> \p -> g { goal = p }
|
||||
gs -> \p ->
|
||||
Goal { goalRange = rCombs (map goalRange gs)
|
||||
@ -177,7 +177,7 @@ simpGoals s gs0 =
|
||||
return $ Just ( apSubst su $ map toGoal extraProps ++
|
||||
map fst nonDef ++
|
||||
unsolvedClassCts ++
|
||||
map (fst . fst) def2
|
||||
map fst def2
|
||||
, su
|
||||
)
|
||||
where
|
||||
@ -238,12 +238,12 @@ lists of literals, so we have special handling for them. In particular:
|
||||
|
||||
NOTE: This assumes that the goals are well-defined.
|
||||
-}
|
||||
eliminateSimpleGEQ :: [Num.SMTProp (a,Num.Prop)] -> [Num.SMTProp (a,Num.Prop)]
|
||||
eliminateSimpleGEQ :: [Num.DefinedProp a] -> [Num.DefinedProp a]
|
||||
eliminateSimpleGEQ = go Map.empty []
|
||||
where
|
||||
|
||||
go geqs other (g : rest) =
|
||||
case snd (Num.smtpOther g) of
|
||||
case Num.dpSimpExprProp g of
|
||||
_ Num.:>= Num.K (Num.Nat 0) ->
|
||||
go geqs other rest
|
||||
|
||||
|
||||
@ -5,7 +5,7 @@ module Cryptol.TypeCheck.Solver.CrySAT
|
||||
, assumeProps, checkDefined, simplifyProps
|
||||
, check
|
||||
, Solver, logger
|
||||
, SMTProp (..)
|
||||
, DefinedProp(..)
|
||||
) where
|
||||
|
||||
import qualified Cryptol.TypeCheck.AST as Cry
|
||||
@ -22,16 +22,27 @@ import MonadLib
|
||||
import Data.Maybe ( mapMaybe )
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
import Data.Traversable ( traverse, for )
|
||||
import Data.Traversable ( traverse )
|
||||
import Data.Set ( Set )
|
||||
import qualified Data.Set as Set
|
||||
import Data.IORef ( IORef, newIORef, readIORef, modifyIORef',
|
||||
atomicModifyIORef' )
|
||||
|
||||
import SimpleSMT ( SExpr )
|
||||
import qualified SimpleSMT as SMT
|
||||
|
||||
|
||||
-- | We use this to rememebr what we simplified
|
||||
newtype SimpProp = SimpProp Prop
|
||||
|
||||
simpProp :: Prop -> SimpProp
|
||||
simpProp p = SimpProp (crySimplify p)
|
||||
|
||||
|
||||
data DefinedProp a = DefinedProp
|
||||
{ dpData :: a
|
||||
, dpSimpProp :: SimpProp -- ^ Fully simplified (may have ORs)
|
||||
, dpSimpExprProp :: Prop -- ^ Expressions are simplified (no ORs)
|
||||
}
|
||||
|
||||
type ImpMap = Map Name Expr
|
||||
|
||||
@ -40,18 +51,14 @@ It does not modify the solver's state.
|
||||
|
||||
The result is like this:
|
||||
* 'Nothing': The properties are inconsistent
|
||||
* 'Just' info: The properties may be consistent, and here is some info:
|
||||
* [a]: We could not prove that these are well defined.
|
||||
* [(a,Prop,SMTProp)]: We proved that these are well defined,
|
||||
and simplified the arguments to the input Prop.
|
||||
* ImpMap: We computed some improvements. -}
|
||||
* 'Just' info: The properties may be consistent, and here is some info. -}
|
||||
checkDefined :: Solver ->
|
||||
(Prop -> a -> a) {- ^ Update a goal -} ->
|
||||
Set Name {- ^ Unification variables -} ->
|
||||
[(a,Prop)] {- ^ Goals -} ->
|
||||
IO (Maybe ( [a] -- could not prove
|
||||
, [SMTProp (a,Prop)] -- proved ok and simplified terms
|
||||
, ImpMap -- computed improvements
|
||||
IO (Maybe ( [a] -- could not prove
|
||||
, [DefinedProp a] -- proved ok and simplified terms
|
||||
, ImpMap -- computed improvements
|
||||
))
|
||||
checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
|
||||
where
|
||||
@ -72,20 +79,21 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
|
||||
else
|
||||
do mapM_ addImpProp (Map.toList novelImps)
|
||||
let newImps = Map.union novelImps knownImps
|
||||
impDone <- mapM (updDone novelImps) newDone
|
||||
let impNotDone = map (updNotDone novelImps) newNotDone
|
||||
impDone = map (updDone novelImps) newDone
|
||||
impNotDone = map (updNotDone novelImps) newNotDone
|
||||
go newImps impDone impNotDone
|
||||
|
||||
addImpProp (x,e) = assert s =<< prepareProp s (Var x :== e)
|
||||
addImpProp (x,e) = assert s (simpProp (Var x :== e))
|
||||
|
||||
updDone su ct =
|
||||
let (g,p) = smtpOther ct
|
||||
in case apSubst su p of
|
||||
Nothing -> return ct
|
||||
Just p' ->
|
||||
do let p2 = crySimpPropExpr p'
|
||||
pr <- prepareProp s p2
|
||||
return pr { smtpOther = (updCt p2 g,p2) }
|
||||
case apSubst su (dpSimpExprProp ct) of
|
||||
Nothing -> ct
|
||||
Just p' ->
|
||||
let p2 = crySimpPropExpr p'
|
||||
in DefinedProp { dpData = updCt p2 (dpData ct)
|
||||
, dpSimpExprProp = p2
|
||||
, dpSimpProp = simpProp p2
|
||||
}
|
||||
|
||||
updNotDone su (g,p) =
|
||||
case apSubst su p of
|
||||
@ -99,11 +107,9 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
|
||||
-- * Well defined constraints are asserted at this point.
|
||||
-- * The expressions in the defined constraints are simplified.
|
||||
checkDefined' :: Solver -> (Prop -> a -> a) ->
|
||||
[(a,Prop)] -> IO ([(a,Prop)], [SMTProp (a,Prop)])
|
||||
[(a,Prop)] -> IO ([(a,Prop)], [DefinedProp a])
|
||||
checkDefined' s updCt props0 =
|
||||
do ps <- for props0 $ \(a,p) ->
|
||||
do p' <- prepareProp s (cryDefinedProp p)
|
||||
return (a,p,p')
|
||||
do let ps = [ (a,p,simpProp (cryDefinedProp p)) | (a,p) <- props0 ]
|
||||
go False [] [] ps
|
||||
|
||||
where
|
||||
@ -117,15 +123,23 @@ checkDefined' s updCt props0 =
|
||||
go False isDef isNotDef [] = return ([ (a,p) | (a,p,_) <- isNotDef ], isDef)
|
||||
|
||||
-- Process one constraint.
|
||||
go ch isDef isNotDef ((ct,p,q) : more) =
|
||||
do proved <- prove s q
|
||||
if proved then do r <- case crySimpPropExprMaybe p of
|
||||
Nothing -> do p' <- prepareProp s p
|
||||
return p' { smtpOther = (ct,p) }
|
||||
Just p' -> do p2 <- prepareProp s p'
|
||||
return p2 { smtpOther = (updCt p' ct, p') }
|
||||
|
||||
assert s r -- add defined prop as an assumption
|
||||
go ch isDef isNotDef ((ct,p,q@(SimpProp defCt)) : more) =
|
||||
do proved <- prove s defCt
|
||||
if proved then do let r = case crySimpPropExprMaybe p of
|
||||
Nothing ->
|
||||
DefinedProp
|
||||
{ dpData = ct
|
||||
, dpSimpExprProp = p
|
||||
, dpSimpProp = simpProp p
|
||||
}
|
||||
Just p' ->
|
||||
DefinedProp
|
||||
{ dpData = updCt p' ct
|
||||
, dpSimpExprProp = p'
|
||||
, dpSimpProp = simpProp p'
|
||||
}
|
||||
-- add defined prop as an assumption
|
||||
assert s (dpSimpProp r)
|
||||
go True (r : isDef) isNotDef more
|
||||
else go ch isDef ((ct,p,q) : isNotDef) more
|
||||
|
||||
@ -135,25 +149,27 @@ checkDefined' s updCt props0 =
|
||||
|
||||
|
||||
|
||||
|
||||
-- | Simplify a bunch of well-defined properties.
|
||||
-- Eliminates properties that are implied by the rest.
|
||||
-- Does not modify the set of assumptions.
|
||||
simplifyProps :: Solver -> [SMTProp a] -> IO [a]
|
||||
simplifyProps :: Solver -> [DefinedProp a] -> IO [a]
|
||||
simplifyProps s props = withScope s (go [] props)
|
||||
where
|
||||
go survived [] = return survived
|
||||
|
||||
go survived (p : more)
|
||||
| smtpLinPart p == SMT.Atom "true" = go survived more
|
||||
go survived (DefinedProp { dpSimpProp = SimpProp PTrue } : more) =
|
||||
go survived more
|
||||
|
||||
go survived (p : more) =
|
||||
do proved <- withScope s $ do mapM_ (assert s) more
|
||||
prove s p
|
||||
if proved
|
||||
then go survived more
|
||||
else do assert s p
|
||||
go (smtpOther p : survived) more
|
||||
case dpSimpProp p of
|
||||
SimpProp PTrue -> go survived more
|
||||
SimpProp p' ->
|
||||
do proved <- withScope s $ do mapM_ (assert s . dpSimpProp) more
|
||||
prove s p'
|
||||
if proved
|
||||
then go survived more
|
||||
else do assert s (SimpProp p')
|
||||
go (dpData p : survived) more
|
||||
|
||||
|
||||
-- | Add the given constraints as assumptions.
|
||||
@ -161,7 +177,7 @@ simplifyProps s props = withScope s (go [] props)
|
||||
-- Modifies the set of assumptions.
|
||||
assumeProps :: Solver -> [Cry.Prop] -> IO VarMap
|
||||
assumeProps s props =
|
||||
do mapM_ (assert s <=< prepareProp s) (map cryDefinedProp ps ++ ps)
|
||||
do mapM_ (assert s . simpProp) (map cryDefinedProp ps ++ ps)
|
||||
return (Map.unions varMaps)
|
||||
where (ps,varMaps) = unzip (mapMaybe exportProp props)
|
||||
-- XXX: Instead of asserting one at a time, perhaps we should
|
||||
@ -174,31 +190,6 @@ assumeProps s props =
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data SMTProp a = SMTProp
|
||||
{ smtpVars :: Set Name
|
||||
-- ^ Theses vars include vars in the linear part,
|
||||
-- as well as variables in the 'fst' of the non-linear part.
|
||||
, smtpLinPart :: SExpr
|
||||
, smtpNonLinPart :: [(Name,Expr)]
|
||||
-- ^ The names are all distinct, and don't appear in the the defs.
|
||||
|
||||
, smtpOther :: a
|
||||
-- ^ Additional information associated with this property.
|
||||
}
|
||||
|
||||
-- | Prepare a property for export to an SMT solver.
|
||||
prepareProp :: Solver -> Prop -> IO (SMTProp ())
|
||||
prepareProp Solver { .. } prop0 =
|
||||
do let prop1 = crySimplify prop0
|
||||
(nonLinEs, linProp) <- atomicModifyIORef' nameSource $ \name ->
|
||||
case nonLinProp name prop1 of
|
||||
(nonLinEs, linProp, newName) -> (newName, (nonLinEs, linProp))
|
||||
return SMTProp
|
||||
{ smtpVars = cryPropFVS linProp
|
||||
, smtpLinPart = ifPropToSmtLib (desugarProp linProp)
|
||||
, smtpNonLinPart = nonLinEs
|
||||
, smtpOther = ()
|
||||
}
|
||||
|
||||
-- | An SMT solver, and some info about declared variables.
|
||||
data Solver = Solver
|
||||
@ -219,11 +210,15 @@ data VarInfo = VarInfo
|
||||
|
||||
data Scope = Scope
|
||||
{ scopeNames :: [Name] -- ^ Variables declared in this scope
|
||||
, scopeAsmps :: [(Name,Expr)] -- ^ Non-linear assumptions.
|
||||
, scopeNonLin :: [(Name,Expr)] -- ^ Non-linear bindings
|
||||
, scopeNonLinS :: NonLinS -- ^ Info about non-linear terms
|
||||
}
|
||||
|
||||
scopeEmpty :: Scope
|
||||
scopeEmpty = Scope { scopeNames = [], scopeAsmps = [] }
|
||||
scopeEmpty = Scope { scopeNames = []
|
||||
, scopeNonLin = []
|
||||
, scopeNonLinS = initialNonLinS
|
||||
}
|
||||
|
||||
scopeElem :: Name -> Scope -> Bool
|
||||
scopeElem x Scope { .. } = x `elem` scopeNames
|
||||
@ -231,8 +226,15 @@ scopeElem x Scope { .. } = x `elem` scopeNames
|
||||
scopeInsert :: Name -> Scope -> Scope
|
||||
scopeInsert x Scope { .. } = Scope { scopeNames = x : scopeNames, .. }
|
||||
|
||||
scopeAssert :: [(Name,Expr)] -> Scope -> Scope
|
||||
scopeAssert as Scope { .. } = Scope { scopeAsmps = as ++ scopeAsmps, .. }
|
||||
-- | Given a *simplified* prop, separate linear and non-linear parts
|
||||
-- and return the linear ones.
|
||||
scopeAssert :: SimpProp -> Scope -> (SimpProp,Scope)
|
||||
scopeAssert (SimpProp p) Scope { .. } =
|
||||
let (defs,p1,s1) = nonLinProp scopeNonLinS p
|
||||
in (SimpProp p1, Scope { scopeNonLin = defs ++ scopeNonLin
|
||||
, scopeNonLinS = s1
|
||||
, ..
|
||||
})
|
||||
|
||||
|
||||
-- | No scopes.
|
||||
@ -247,14 +249,17 @@ viElem x VarInfo { .. } = any (x `scopeElem`) (curScope : otherScopes)
|
||||
viInsert :: Name -> VarInfo -> VarInfo
|
||||
viInsert x VarInfo { .. } = VarInfo { curScope = scopeInsert x curScope, .. }
|
||||
|
||||
-- | Add some non-linear assertions to the current scope.
|
||||
viAssert :: [(Name,Expr)] -> VarInfo -> VarInfo
|
||||
viAssert as VarInfo { .. } = VarInfo { curScope = scopeAssert as curScope, .. }
|
||||
-- | Add an assertion to the current scope. Returns the lienar part.
|
||||
viAssert :: SimpProp -> VarInfo -> (VarInfo, SimpProp)
|
||||
viAssert p VarInfo { .. } = ( VarInfo { curScope = s1, .. }, p1)
|
||||
where (p1, s1) = scopeAssert p curScope
|
||||
|
||||
-- | Enter a scope.
|
||||
viPush :: VarInfo -> VarInfo
|
||||
viPush VarInfo { .. } = VarInfo { curScope = scopeEmpty
|
||||
, otherScopes = curScope : otherScopes }
|
||||
viPush VarInfo { .. } =
|
||||
VarInfo { curScope = scopeEmpty { scopeNonLinS = scopeNonLinS curScope }
|
||||
, otherScopes = curScope : otherScopes
|
||||
}
|
||||
|
||||
-- | Exit a scope.
|
||||
viPop :: VarInfo -> VarInfo
|
||||
@ -306,25 +311,23 @@ declareVar Solver { .. } a =
|
||||
modifyIORef' declared (viInsert a)
|
||||
|
||||
-- | Add an assertion to the current context.
|
||||
assert :: Solver -> SMTProp a -> IO ()
|
||||
assert s@Solver { .. } SMTProp { .. }
|
||||
| smtpLinPart == SMT.Atom "true" = return ()
|
||||
| otherwise =
|
||||
do mapM_ (declareVar s) (Set.toList smtpVars)
|
||||
SMT.assert solver smtpLinPart
|
||||
modifyIORef' declared (viAssert smtpNonLinPart)
|
||||
-- INVARIANT: Assertion is simplified.
|
||||
assert :: Solver -> SimpProp -> IO ()
|
||||
assert _ (SimpProp PTrue) = return ()
|
||||
assert s@Solver { .. } p =
|
||||
do SimpProp p1 <- atomicModifyIORef' declared (viAssert p)
|
||||
mapM_ (declareVar s) (Set.toList (cryPropFVS p1))
|
||||
SMT.assert solver $ ifPropToSmtLib $ desugarProp p1
|
||||
|
||||
|
||||
-- | 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 -> SMTProp a -> IO Bool
|
||||
prove s@(Solver { .. }) SMTProp { .. }
|
||||
| smtpLinPart == SMT.Atom "true" = return True
|
||||
| otherwise =
|
||||
prove :: Solver -> Prop -> IO Bool
|
||||
prove _ PTrue = return True
|
||||
prove s@(Solver { .. }) p =
|
||||
withScope s $
|
||||
do mapM_ (declareVar s) (Set.toList smtpVars)
|
||||
SMT.assert solver (SMT.not smtpLinPart)
|
||||
do assert s (simpProp (Not p))
|
||||
res <- SMT.check solver
|
||||
case res of
|
||||
SMT.Unsat -> return True
|
||||
|
||||
@ -10,14 +10,20 @@
|
||||
-- element, and various arithmetic operators on them.
|
||||
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module Cryptol.TypeCheck.Solver.InfNat where
|
||||
|
||||
import Data.Bits
|
||||
import Cryptol.Utils.Panic
|
||||
|
||||
import Data.GenericTrie(TrieKey)
|
||||
import GHC.Generics(Generic)
|
||||
|
||||
-- | Natural numbers with an infinity element
|
||||
data Nat' = Nat Integer | Inf
|
||||
deriving (Show,Eq,Ord)
|
||||
deriving (Show,Eq,Ord,Generic)
|
||||
|
||||
instance TrieKey Nat'
|
||||
|
||||
fromNat :: Nat' -> Maybe Integer
|
||||
fromNat n' =
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
-- | The sytnax of numeric propositions.
|
||||
module Cryptol.TypeCheck.Solver.Numeric.AST
|
||||
( Name, toName, sysName, fromName, ppName
|
||||
@ -18,20 +19,16 @@ module Cryptol.TypeCheck.Solver.Numeric.AST
|
||||
, IfExpr(..), ppIfExpr
|
||||
|
||||
, Subst, HasVars(..), cryLet
|
||||
|
||||
, PropMap(..)
|
||||
, ExprMap(..)
|
||||
) where
|
||||
|
||||
import Cryptol.TypeCheck.Solver.InfNat ( Nat'(..) )
|
||||
import Cryptol.TypeCheck.TypeMap ( TrieMap(..), mapWithKeyTM )
|
||||
import Cryptol.Utils.Panic ( panic )
|
||||
import Cryptol.Utils.Misc ( anyJust )
|
||||
|
||||
import Control.Monad ( mplus )
|
||||
import Data.GenericTrie (TrieKey)
|
||||
import GHC.Generics(Generic)
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe ( isNothing )
|
||||
import Data.Set ( Set )
|
||||
import qualified Data.Set as Set
|
||||
import qualified Control.Applicative as A
|
||||
@ -50,7 +47,7 @@ infixr 8 :^^
|
||||
|
||||
|
||||
data Name = UserName Int | SysName Int
|
||||
deriving (Show,Eq,Ord)
|
||||
deriving (Show,Eq,Ord,Generic)
|
||||
|
||||
toName :: Int -> Name
|
||||
toName = UserName
|
||||
@ -82,7 +79,7 @@ data Prop =
|
||||
| Prop :&& Prop | Prop :|| Prop
|
||||
| Not Prop
|
||||
| PFalse | PTrue
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
|
||||
-- | Expressions, representing Cryptol's numeric types.
|
||||
@ -100,7 +97,7 @@ data Expr = K Nat'
|
||||
| Width Expr
|
||||
| LenFromThen Expr Expr Expr
|
||||
| LenFromThenTo Expr Expr Expr
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
|
||||
-- | The constant @0@.
|
||||
@ -295,322 +292,9 @@ instance HasVars Prop where
|
||||
-- Tries
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data PropMap a = EmptyPM
|
||||
| PropMap { pmFin :: ExprMap a
|
||||
, pmEq
|
||||
, pmGeq
|
||||
, pmGt
|
||||
, pmEqH
|
||||
, pmGtH :: ExprMap (ExprMap a)
|
||||
, pmAnd
|
||||
, pmOr :: PropMap (PropMap a)
|
||||
, pmNot :: PropMap a
|
||||
, pmFalse
|
||||
, pmTrue :: Maybe a
|
||||
}
|
||||
|
||||
instance TrieMap PropMap Prop where
|
||||
nullTM EmptyPM = True
|
||||
nullTM PropMap { .. } = and [ nullTM pmFin
|
||||
, nullTM pmEq
|
||||
, nullTM pmGeq
|
||||
, nullTM pmGt
|
||||
, nullTM pmEqH
|
||||
, nullTM pmGtH
|
||||
, nullTM pmAnd
|
||||
, nullTM pmOr
|
||||
, nullTM pmNot
|
||||
, isNothing pmFalse
|
||||
, isNothing pmTrue
|
||||
]
|
||||
|
||||
|
||||
emptyTM = EmptyPM
|
||||
|
||||
lookupTM _ EmptyPM = Nothing
|
||||
lookupTM p PropMap { .. } = go p
|
||||
where
|
||||
|
||||
go (Fin e) = lookupTM e pmFin
|
||||
|
||||
go (a :== b) = lookupTM b =<< lookupTM a pmEq
|
||||
go (a :>= b) = lookupTM b =<< lookupTM a pmGeq
|
||||
go (a :> b) = lookupTM b =<< lookupTM a pmGt
|
||||
|
||||
go (a :==: b) = lookupTM b =<< lookupTM a pmEqH
|
||||
go (a :>: b) = lookupTM b =<< lookupTM a pmGtH
|
||||
|
||||
go (a :&& b) = lookupTM b =<< lookupTM a pmAnd
|
||||
go (a :|| b) = lookupTM b =<< lookupTM a pmOr
|
||||
go (Not a) = lookupTM a pmNot
|
||||
|
||||
go PFalse = pmFalse
|
||||
go PTrue = pmTrue
|
||||
|
||||
alterTM p f EmptyPM = alterTM p f
|
||||
PropMap { pmFin = emptyTM
|
||||
, pmEq = emptyTM
|
||||
, pmGeq = emptyTM
|
||||
, pmGt = emptyTM
|
||||
, pmEqH = emptyTM
|
||||
, pmGtH = emptyTM
|
||||
, pmAnd = emptyTM
|
||||
, pmOr = emptyTM
|
||||
, pmNot = emptyTM
|
||||
, pmFalse = Nothing
|
||||
, pmTrue = Nothing
|
||||
}
|
||||
|
||||
alterTM p f PropMap { .. } = go p
|
||||
where
|
||||
|
||||
alter k (Just m) = Just (alterTM k f m)
|
||||
alter _ Nothing = Nothing
|
||||
|
||||
go (Fin e) = PropMap { pmFin = alterTM e f pmFin, .. }
|
||||
|
||||
go (a :== b) = PropMap { pmEq = alterTM a (alter b) pmEq, .. }
|
||||
go (a :>= b) = PropMap { pmGeq = alterTM a (alter b) pmGeq, .. }
|
||||
go (a :> b) = PropMap { pmGt = alterTM a (alter b) pmGt, .. }
|
||||
|
||||
go (a :==: b) = PropMap { pmEqH = alterTM a (alter b) pmEqH, .. }
|
||||
go (a :>: b) = PropMap { pmGtH = alterTM a (alter b) pmGtH, .. }
|
||||
|
||||
go (a :&& b) = PropMap { pmAnd = alterTM a (alter b) pmAnd, .. }
|
||||
go (a :|| b) = PropMap { pmOr = alterTM a (alter b) pmOr, .. }
|
||||
go (Not a) = PropMap { pmNot = alterTM a f pmNot, .. }
|
||||
|
||||
go PFalse = PropMap { pmFalse = f pmFalse, .. }
|
||||
go PTrue = PropMap { pmTrue = f pmTrue, .. }
|
||||
|
||||
unionTM _ EmptyPM r = r
|
||||
unionTM _ l EmptyPM = l
|
||||
unionTM f l r =
|
||||
PropMap { pmFin = unionTM f (pmFin l) (pmFin r)
|
||||
, pmEq = unionTM (unionTM f) (pmEq l) (pmEq r)
|
||||
, pmGeq = unionTM (unionTM f) (pmGeq l) (pmGeq r)
|
||||
, pmGt = unionTM (unionTM f) (pmGt l) (pmGt r)
|
||||
, pmEqH = unionTM (unionTM f) (pmEqH l) (pmEqH r)
|
||||
, pmGtH = unionTM (unionTM f) (pmGtH l) (pmGtH r)
|
||||
, pmAnd = unionTM (unionTM f) (pmAnd l) (pmAnd r)
|
||||
, pmOr = unionTM (unionTM f) (pmOr l) (pmOr r)
|
||||
, pmNot = unionTM f (pmNot l) (pmNot r)
|
||||
, pmFalse = case (pmFalse l, pmFalse r) of
|
||||
(Just a, Just b) -> Just (f a b)
|
||||
(mbL, mbR) -> mbL `mplus` mbR
|
||||
, pmTrue = case (pmTrue l, pmFalse r) of
|
||||
(Just a, Just b) -> Just (f a b)
|
||||
(mbL, mbR) -> mbL `mplus` mbR
|
||||
}
|
||||
|
||||
toListTM EmptyPM = []
|
||||
toListTM PropMap { .. } =
|
||||
[ (Fin x ,a) | (x,a) <- toListTM pmFin ] ++
|
||||
[ (l :== r,a) | (l,m) <- toListTM pmEq, (r,a) <- toListTM m ] ++
|
||||
[ (l :>= r,a) | (l,m) <- toListTM pmGeq, (r,a) <- toListTM m ] ++
|
||||
[ (l :> r,a) | (l,m) <- toListTM pmGt, (r,a) <- toListTM m ] ++
|
||||
[ (l :==: r,a) | (l,m) <- toListTM pmEqH, (r,a) <- toListTM m ] ++
|
||||
[ (l :>: r,a) | (l,m) <- toListTM pmGtH, (r,a) <- toListTM m ] ++
|
||||
[ (l :&& r,a) | (l,m) <- toListTM pmAnd, (r,a) <- toListTM m ] ++
|
||||
[ (l :|| r,a) | (l,m) <- toListTM pmOr, (r,a) <- toListTM m ] ++
|
||||
[ (Not x ,a) | (x,a) <- toListTM pmNot ] ++
|
||||
[ (PFalse ,a) | Just a <- [pmFalse] ] ++
|
||||
[ (PTrue ,a) | Just a <- [pmTrue] ]
|
||||
|
||||
mapMaybeWithKeyTM _ EmptyPM = EmptyPM
|
||||
mapMaybeWithKeyTM f PropMap { .. } =
|
||||
PropMap { pmFin = mapMaybeWithKeyTM (\t -> f (Fin t)) pmFin
|
||||
, pmEq = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :== r))) pmEq
|
||||
, pmGeq = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :>= r))) pmGeq
|
||||
, pmGt = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :> r))) pmGt
|
||||
, pmEqH = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :==: r))) pmEqH
|
||||
, pmGtH = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :>: r))) pmGtH
|
||||
, pmAnd = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :&& r))) pmAnd
|
||||
, pmOr = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :|| r))) pmOr
|
||||
, pmNot = mapMaybeWithKeyTM (\p -> f (Not p)) pmNot
|
||||
, pmFalse = f PFalse =<< pmFalse
|
||||
, pmTrue = f PTrue =<< pmTrue
|
||||
}
|
||||
|
||||
|
||||
data ExprMap a = EmptyEM
|
||||
| ExprMap { emK :: Map.Map Nat' a
|
||||
, emVar :: Map.Map Name a
|
||||
, emAdd
|
||||
, emSub
|
||||
, emMul
|
||||
, emDiv
|
||||
, emMod
|
||||
, emExp
|
||||
, emMin
|
||||
, emMax :: ExprMap (ExprMap a)
|
||||
, emLg2
|
||||
, emWidth :: ExprMap a
|
||||
, emLenFromThen
|
||||
, emLenFromThenTo :: ExprMap (ExprMap (ExprMap a))
|
||||
}
|
||||
|
||||
instance TrieMap ExprMap Expr where
|
||||
|
||||
nullTM EmptyEM = True
|
||||
nullTM ExprMap { .. } = and [ nullTM emK
|
||||
, nullTM emVar
|
||||
, nullTM emAdd
|
||||
, nullTM emSub
|
||||
, nullTM emMul
|
||||
, nullTM emDiv
|
||||
, nullTM emMod
|
||||
, nullTM emExp
|
||||
, nullTM emMin
|
||||
, nullTM emMax
|
||||
, nullTM emLg2
|
||||
, nullTM emWidth
|
||||
, nullTM emLenFromThen
|
||||
, nullTM emLenFromThenTo
|
||||
]
|
||||
|
||||
emptyTM = EmptyEM
|
||||
|
||||
lookupTM _ EmptyEM = Nothing
|
||||
lookupTM e ExprMap { .. } = go e
|
||||
where
|
||||
|
||||
go (K n) = Map.lookup n emK
|
||||
go (Var n) = Map.lookup n emVar
|
||||
go (a :+ b) = lookupTM b =<< lookupTM a emAdd
|
||||
go (a :- b) = lookupTM b =<< lookupTM a emSub
|
||||
go (a :* b) = lookupTM b =<< lookupTM a emMul
|
||||
go (Div a b) = lookupTM b =<< lookupTM a emDiv
|
||||
go (Mod a b) = lookupTM b =<< lookupTM a emMod
|
||||
go (a :^^ b) = lookupTM b =<< lookupTM a emExp
|
||||
go (Min a b) = lookupTM b =<< lookupTM a emMin
|
||||
go (Max a b) = lookupTM b =<< lookupTM a emMax
|
||||
go (Lg2 a) = lookupTM a emLg2
|
||||
go (Width a) = lookupTM a emWidth
|
||||
|
||||
go (LenFromThen a b c) = lookupTM c
|
||||
=<< lookupTM b
|
||||
=<< lookupTM a emLenFromThen
|
||||
|
||||
go (LenFromThenTo a b c) = lookupTM c
|
||||
=<< lookupTM b
|
||||
=<< lookupTM a emLenFromThenTo
|
||||
|
||||
alterTM e f EmptyEM = alterTM e f
|
||||
ExprMap { emK = emptyTM
|
||||
, emVar = emptyTM
|
||||
, emAdd = emptyTM
|
||||
, emSub = emptyTM
|
||||
, emMul = emptyTM
|
||||
, emDiv = emptyTM
|
||||
, emMod = emptyTM
|
||||
, emExp = emptyTM
|
||||
, emMin = emptyTM
|
||||
, emMax = emptyTM
|
||||
, emLg2 = emptyTM
|
||||
, emWidth = emptyTM
|
||||
, emLenFromThen = emptyTM
|
||||
, emLenFromThenTo = emptyTM
|
||||
}
|
||||
|
||||
alterTM e f ExprMap { .. } = go e
|
||||
where
|
||||
|
||||
alter k (Just m) = Just (alterTM k f m)
|
||||
alter _ Nothing = Nothing
|
||||
|
||||
go (K n) = ExprMap { emK = Map.alter f n emK, .. }
|
||||
go (Var n) = ExprMap { emVar = Map.alter f n emVar, .. }
|
||||
|
||||
go (a :+ b) = ExprMap { emAdd = alterTM a (alter b) emAdd, .. }
|
||||
go (a :- b) = ExprMap { emSub = alterTM a (alter b) emSub, .. }
|
||||
go (a :* b) = ExprMap { emMul = alterTM a (alter b) emMul, .. }
|
||||
go (Div a b) = ExprMap { emDiv = alterTM a (alter b) emDiv, .. }
|
||||
go (Mod a b) = ExprMap { emMod = alterTM a (alter b) emMod, .. }
|
||||
go (a :^^ b) = ExprMap { emExp = alterTM a (alter b) emExp, .. }
|
||||
go (Min a b) = ExprMap { emMin = alterTM a (alter b) emMin, .. }
|
||||
go (Max a b) = ExprMap { emMax = alterTM a (alter b) emMax, .. }
|
||||
|
||||
go (Lg2 a) = ExprMap { emLg2 = alterTM a f emLg2, .. }
|
||||
go (Width a) = ExprMap { emWidth = alterTM a f emWidth, .. }
|
||||
|
||||
go (LenFromThen a b c) =
|
||||
ExprMap { emLenFromThen = alterTM a (fmap (alterTM b (alter c))) emLenFromThen, .. }
|
||||
|
||||
go (LenFromThenTo a b c) =
|
||||
ExprMap { emLenFromThenTo = alterTM a (fmap (alterTM b (alter c))) emLenFromThenTo, .. }
|
||||
|
||||
unionTM _ EmptyEM r = r
|
||||
unionTM _ l EmptyEM = l
|
||||
unionTM f l r =
|
||||
ExprMap { emK = unionTM f (emK l) (emK r)
|
||||
, emVar = unionTM f (emVar l) (emVar r)
|
||||
, emAdd = unionTM (unionTM f) (emAdd l) (emAdd r)
|
||||
, emSub = unionTM (unionTM f) (emSub l) (emSub r)
|
||||
, emMul = unionTM (unionTM f) (emMul l) (emMul r)
|
||||
, emDiv = unionTM (unionTM f) (emDiv l) (emDiv r)
|
||||
, emMod = unionTM (unionTM f) (emMod l) (emMod r)
|
||||
, emExp = unionTM (unionTM f) (emExp l) (emExp r)
|
||||
, emMin = unionTM (unionTM f) (emMin l) (emMin r)
|
||||
, emMax = unionTM (unionTM f) (emMax l) (emMax r)
|
||||
, emLg2 = unionTM f (emLg2 l) (emLg2 r)
|
||||
, emWidth = unionTM f (emWidth l) (emWidth r)
|
||||
|
||||
, emLenFromThen = unionTM (unionTM (unionTM f)) (emLenFromThen l)
|
||||
(emLenFromThen r)
|
||||
, emLenFromThenTo = unionTM (unionTM (unionTM f)) (emLenFromThenTo l)
|
||||
(emLenFromThenTo r)
|
||||
}
|
||||
|
||||
toListTM EmptyEM = []
|
||||
toListTM ExprMap { .. } =
|
||||
[ (K n , a) | (n,a) <- Map.toList emK ] ++
|
||||
[ (Var n , a) | (n,a) <- Map.toList emVar ] ++
|
||||
[ (l :+ r , a) | (l,m) <- toListTM emAdd, (r,a) <- toListTM m ] ++
|
||||
[ (l :- r , a) | (l,m) <- toListTM emSub, (r,a) <- toListTM m ] ++
|
||||
[ (l :* r , a) | (l,m) <- toListTM emMul, (r,a) <- toListTM m ] ++
|
||||
[ (Div l r, a) | (l,m) <- toListTM emDiv, (r,a) <- toListTM m ] ++
|
||||
[ (Mod l r, a) | (l,m) <- toListTM emMod, (r,a) <- toListTM m ] ++
|
||||
[ (l :^^ r, a) | (l,m) <- toListTM emExp, (r,a) <- toListTM m ] ++
|
||||
[ (Min l r, a) | (l,m) <- toListTM emMin, (r,a) <- toListTM m ] ++
|
||||
[ (Max l r, a) | (l,m) <- toListTM emMax, (r,a) <- toListTM m ] ++
|
||||
[ (Lg2 x , a) | (x,a) <- toListTM emLg2 ] ++
|
||||
[ (Width x, a) | (x,a) <- toListTM emWidth ] ++
|
||||
|
||||
[ (LenFromThen x y z, a) | (x,m1) <- toListTM emLenFromThen
|
||||
, (y,m2) <- toListTM m1
|
||||
, (z,a) <- toListTM m2 ] ++
|
||||
|
||||
[ (LenFromThenTo x y z, a) | (x,m1) <- toListTM emLenFromThenTo
|
||||
, (y,m2) <- toListTM m1
|
||||
, (z,a) <- toListTM m2 ]
|
||||
|
||||
mapMaybeWithKeyTM _ EmptyEM = EmptyEM
|
||||
mapMaybeWithKeyTM f ExprMap { .. } =
|
||||
ExprMap { emK = mapMaybeWithKeyTM (\n -> f (K n)) emK
|
||||
, emVar = mapMaybeWithKeyTM (\n -> f (Var n)) emVar
|
||||
|
||||
, emAdd = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :+ r))) emAdd
|
||||
, emSub = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :- r))) emSub
|
||||
, emMul = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :* r))) emMul
|
||||
, emDiv = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (Div l r))) emDiv
|
||||
, emMod = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (Mod l r))) emMod
|
||||
, emExp = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (l :^^ r))) emExp
|
||||
, emMin = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (Min l r))) emMin
|
||||
, emMax = mapWithKeyTM (\l -> mapMaybeWithKeyTM (\r -> f (Max l r))) emMax
|
||||
|
||||
, emLg2 = mapMaybeWithKeyTM (\a -> f (Lg2 a)) emLg2
|
||||
, emWidth = mapMaybeWithKeyTM (\a -> f (Width a)) emWidth
|
||||
|
||||
, emLenFromThen = mapWithKeyTM (\x ->
|
||||
mapWithKeyTM (\y ->
|
||||
mapMaybeWithKeyTM (\z -> f (LenFromThen x y z)))) emLenFromThen
|
||||
|
||||
, emLenFromThenTo = mapWithKeyTM (\x ->
|
||||
mapWithKeyTM (\y ->
|
||||
mapMaybeWithKeyTM (\z -> f (LenFromThenTo x y z)))) emLenFromThenTo
|
||||
}
|
||||
|
||||
instance TrieKey Name
|
||||
instance TrieKey Prop
|
||||
instance TrieKey Expr
|
||||
|
||||
|
||||
|
||||
|
||||
@ -1,17 +1,34 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
-- | Separate Non-Linear Constraints
|
||||
--
|
||||
-- TODO: When naming non-linear terms,
|
||||
-- use the same name for the same expression.
|
||||
module Cryptol.TypeCheck.Solver.Numeric.NonLin
|
||||
( nonLinProp
|
||||
, NonLinS
|
||||
, initialNonLinS
|
||||
) where
|
||||
|
||||
import Cryptol.TypeCheck.Solver.Numeric.AST
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
import Data.GenericTrie (Trie)
|
||||
import qualified Data.GenericTrie as Trie
|
||||
import MonadLib
|
||||
|
||||
-- | Factor-out non-linear terms, by naming them
|
||||
nonLinProp :: NonLinS -> Prop -> ([(Name,Expr)], Prop, NonLinS)
|
||||
nonLinProp s0 prop = case runId $ runStateT s0 $ nonLinPropM prop of
|
||||
(p, sFin) -> ( nonLinExprs sFin
|
||||
, p
|
||||
, sFin { nonLinExprs = [] }
|
||||
)
|
||||
|
||||
-- | The initial state for the linearization process.
|
||||
initialNonLinS :: NonLinS
|
||||
initialNonLinS = NonLinS
|
||||
{ nextName = 0
|
||||
, nonLinExprs = []
|
||||
, nlKnown = Trie.empty
|
||||
}
|
||||
|
||||
|
||||
-- | Is the top-level operator a non-linear one.
|
||||
isNonLinOp :: Expr -> Bool
|
||||
@ -60,14 +77,6 @@ isNonLinOp expr =
|
||||
-- sure how to do that...
|
||||
|
||||
|
||||
-- | Factor-out non-linear terms, by naming them
|
||||
nonLinProp :: Int -> Prop -> ([(Name,Expr)], Prop, Int)
|
||||
nonLinProp name prop = case runId $ runStateT s0 $ nonLinPropM prop of
|
||||
(p, sFin) -> (nonLinExprs sFin, p, nextName sFin)
|
||||
where
|
||||
s0 = NonLinS { nextName = name, nonLinExprs = [] }
|
||||
|
||||
|
||||
nonLinPropM :: Prop -> NonLinM Prop
|
||||
nonLinPropM prop =
|
||||
case prop of
|
||||
@ -102,17 +111,19 @@ type NonLinM = StateT NonLinS Id
|
||||
data NonLinS = NonLinS
|
||||
{ nextName :: !Int
|
||||
, nonLinExprs :: [(Name,Expr)]
|
||||
, nlKnown :: Trie Expr Name
|
||||
}
|
||||
|
||||
nameExpr :: Expr -> NonLinM Expr
|
||||
nameExpr e = sets $ \s ->
|
||||
case [ x | (x,e1) <- nonLinExprs s, e == e1 ] of -- XXX: inefficient!
|
||||
x : _ -> (Var x,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 = (n,e) : nonLinExprs s
|
||||
, nlKnown = Trie.insert e n (nlKnown s)
|
||||
}
|
||||
in s1 `seq` (Var n, s1)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user