mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Just debugging improvements.
This commit is contained in:
Iavor S. Diatchki
parent
ce09d23d74
commit
d85a5d5aa0
@ -43,7 +43,7 @@ library
|
||||
random >= 1.0.1,
|
||||
sbv >= 4.0,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.4,
|
||||
simple-smt >= 0.5.4,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
tf-random >= 0.5,
|
||||
|
||||
@ -27,7 +27,6 @@ import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
|
||||
import Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Parser.Position(rCombs)
|
||||
import Cryptol.Utils.PP(pp)
|
||||
|
||||
import Cryptol.TypeCheck.Defaulting(tryDefaultWith)
|
||||
|
||||
@ -134,18 +133,15 @@ numericRight g = case Num.exportProp (goal g) of
|
||||
|
||||
_testSimpGoals :: IO ()
|
||||
_testSimpGoals = Num.withSolver $ \s ->
|
||||
do Num.assumeProps s asmps
|
||||
do _ <- Num.assumeProps s asmps
|
||||
mb <- simpGoals s gs
|
||||
case mb of
|
||||
Just (gs1,su) ->
|
||||
do debugBlock s "Simplified goals"
|
||||
$ mapM_ (debugLog s . show . pp . goal) gs1
|
||||
debugLog s (show (pp su))
|
||||
Just _ -> debugLog s "End of test"
|
||||
Nothing -> debugLog s "Impossible"
|
||||
where
|
||||
asmps = [ pFin (tv 1) ]
|
||||
gs = map fakeGoal [ tv 0 =#= (num 1 .+. tMin (tv 1) (tv 0)) ]
|
||||
-- ?g4 == 1 + min m ?g4
|
||||
-- gs = map fakeGoal [ pFin (num 1 .+. tMin (tv 1) (tv 0)) ]
|
||||
|
||||
-- [ tv 0 =#= tInf, tMod (num 3) (tv 0) =#= num 4 ]
|
||||
|
||||
@ -157,7 +153,7 @@ _testSimpGoals = Num.withSolver $ \s ->
|
||||
simpGoals :: Num.Solver -> [Goal] -> IO (Maybe ([Goal],Subst))
|
||||
simpGoals _ [] = return (Just ([],emptySubst))
|
||||
simpGoals s gs0 =
|
||||
debugBlock s "simpGoals" $
|
||||
debugBlock s "Simplifying goals" $
|
||||
do debugBlock s "goals:" (debugLog s gs0)
|
||||
|
||||
let (unsolvedClassCts,numCts) = solveClassCts gs0
|
||||
@ -171,14 +167,14 @@ simpGoals s gs0 =
|
||||
, show r
|
||||
]
|
||||
case numCts of
|
||||
[] -> do debugBlock s "survivors" $ debugLog s unsolvedClassCts
|
||||
[] -> do debugBlock s "After simplification (no numerics):"
|
||||
$ debugLog s unsolvedClassCts
|
||||
return $ Just (unsolvedClassCts, emptySubst)
|
||||
|
||||
_ -> do mbOk <- Num.checkDefined s updCt uvs numCts
|
||||
case mbOk of
|
||||
|
||||
Nothing -> do debugLog s "check defined: impossible"
|
||||
return Nothing
|
||||
Nothing -> return Nothing
|
||||
|
||||
Just (nonDef,def,imps) ->
|
||||
|
||||
@ -193,20 +189,13 @@ simpGoals s gs0 =
|
||||
, goalSource = CtImprovement
|
||||
, goal = p }
|
||||
|
||||
debugBlock s "check defined:" $
|
||||
do debugBlock s "undefined" $
|
||||
debugLog s (map fst nonDef)
|
||||
debugBlock s "defined" $
|
||||
debugLog s (map Num.dpSimpExprProp def1)
|
||||
|
||||
|
||||
def2 <- Num.simplifyProps s def1
|
||||
let allCts = apSubst su $ map toGoal extraProps ++
|
||||
map fst nonDef ++
|
||||
unsolvedClassCts ++
|
||||
map fst def2
|
||||
|
||||
debugBlock s "survivors" $
|
||||
debugBlock s "After simplification:" $
|
||||
do debugLog s allCts
|
||||
debugLog s su
|
||||
|
||||
|
||||
@ -81,14 +81,17 @@ checkDefined :: Solver ->
|
||||
, Subst -- computed improvements, for the conjuction
|
||||
-- of the proved properties.
|
||||
))
|
||||
checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
|
||||
checkDefined s updCt uniVars props0 =
|
||||
debugBlock s "Checking for well-defined properties" $
|
||||
withScope s (go Map.empty [] props0)
|
||||
where
|
||||
go knownImps done notDone =
|
||||
do (newNotDone, novelDone) <- checkDefined' s updCt notDone
|
||||
(possible, imps) <- check s uniVars
|
||||
|
||||
if not possible
|
||||
then return Nothing
|
||||
then do debugLog s "Found contradiction"
|
||||
return Nothing
|
||||
else
|
||||
do let goAgain novelImps newDone =
|
||||
do mapM_ addImpProp (Map.toList novelImps)
|
||||
@ -102,10 +105,16 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
|
||||
|
||||
if Map.null novelImps
|
||||
then case findImpByDef [] newDone of
|
||||
Nothing -> return $ Just ( map fst newNotDone
|
||||
, newDone
|
||||
, knownImps
|
||||
)
|
||||
Nothing ->
|
||||
do debugBlock s "Not well-defined:" $
|
||||
debugLog s (map snd newNotDone)
|
||||
debugBlock s "Always defined:" $
|
||||
debugLog s (map dpSimpExprProp newDone)
|
||||
|
||||
return $ Just ( map fst newNotDone
|
||||
, newDone
|
||||
, knownImps
|
||||
)
|
||||
Just ((x,e), rest) ->
|
||||
goAgain (Map.singleton x e) rest
|
||||
|
||||
@ -194,7 +203,9 @@ checkDefined' s updCt props0 =
|
||||
-- * Eliminates properties that are implied by the rest.
|
||||
-- * Does not modify the set of assumptions.
|
||||
simplifyProps :: Solver -> [DefinedProp a] -> IO [a]
|
||||
simplifyProps s props = withScope s (go [] props)
|
||||
simplifyProps s props =
|
||||
debugBlock s "Simplifying properties" $
|
||||
withScope s (go [] props)
|
||||
where
|
||||
go survived [] = return survived
|
||||
|
||||
@ -491,8 +502,9 @@ declareVar s@Solver { .. } a =
|
||||
-- INVARIANT: Assertion is simplified.
|
||||
assert :: Solver -> SimpProp -> IO ()
|
||||
assert _ (SimpProp PTrue) = return ()
|
||||
assert s@Solver { .. } p =
|
||||
do SimpProp p1 <- atomicModifyIORef' declared (viAssert p)
|
||||
assert s@Solver { .. } p@(SimpProp p0) =
|
||||
do debugLog s ("Assuming: " ++ show (ppProp p0))
|
||||
SimpProp p1 <- atomicModifyIORef' declared (viAssert p)
|
||||
mapM_ (declareVar s) (Set.toList (cryPropFVS p1))
|
||||
SMT.assert solver $ ifPropToSmtLib $ desugarProp p1
|
||||
|
||||
@ -508,9 +520,9 @@ prove s@(Solver { .. }) p =
|
||||
do assert s (simpProp (Not p))
|
||||
res <- SMT.check solver
|
||||
case res of
|
||||
SMT.Unsat -> return True
|
||||
SMT.Unknown -> return False -- We are not sure
|
||||
SMT.Sat -> return False
|
||||
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.
|
||||
@ -524,13 +536,14 @@ The 'Bool' is 'False' if the current assumptions are *definately*
|
||||
not satisfiable. -}
|
||||
check :: Solver -> Set Name -> IO (Bool, Subst)
|
||||
check s@Solver { .. } uniVars =
|
||||
debugBlock s "check" $
|
||||
do res <- SMT.check solver
|
||||
case res of
|
||||
SMT.Unsat -> return (False, Map.empty)
|
||||
SMT.Unknown -> return (True, Map.empty)
|
||||
SMT.Unsat -> debugLog s "Not satisfiable" >> return (False, Map.empty)
|
||||
SMT.Unknown -> debugLog s "Unknown" >> return (True, Map.empty)
|
||||
SMT.Sat ->
|
||||
do impMap <- debugBlock s "improvements" (getImpSubst s uniVars)
|
||||
do debugLog s "Satisfiable"
|
||||
impMap <- debugBlock s "Computing improvements"
|
||||
(getImpSubst s uniVars)
|
||||
return (True, impMap)
|
||||
|
||||
{- | The set of unification variables is used to guide ordering of
|
||||
@ -557,7 +570,12 @@ getImpSubst s@Solver { .. } uniVars =
|
||||
dump (x,e) = debugLog s (show (ppProp (Var x :== e)))
|
||||
|
||||
when (not (Map.null tricky)) $
|
||||
debugBlock s "Tricky subst" $ mapM_ dump (Map.toList tricky)
|
||||
debugBlock s "Tricky subst:" $ mapM_ dump (Map.toList tricky)
|
||||
|
||||
if Map.null easy
|
||||
then debugLog s "(no improvements)"
|
||||
else mapM_ dump (Map.toList easy)
|
||||
|
||||
|
||||
return easy
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user