Mr Solver Widening

heapster-saw/examples/Makefile

@@ -1,4 +1,4 @@
-all: Makefile.coq
+all: Makefile.coq mr-solver-tests
 
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
@@ -32,3 +32,12 @@ rust_data.bc: rust_data.rs
 
 rust_lifetimes.bc: rust_lifetimes.rs
 	rustc --crate-type=lib --emit=llvm-bc rust_lifetimes.rs
+
+# Lists all the Mr Solver tests, without their ".saw" suffix
+MR_SOLVER_TESTS = arrays_mr_solver
+
+.PHONY: mr-solver-tests $(MR_SOLVER_TESTS)
+mr-solver-tests: $(MR_SOLVER_TESTS)
+
+$(MR_SOLVER_TESTS):
+	$(SAW) $@.saw

heapster-saw/examples/arrays_mr_solver.saw

@@ -1,3 +1,19 @@
 include "arrays.saw";
+
+let eq_bool b1 b2 =
+  if b1 then
+    if b2 then true else false
+  else
+    if b2 then false else true;
+
+let fail = do { print "Test failed"; exit 1; };
+let run_test name test expected =
+  do { if expected then print (str_concat "Test: " name) else
+         print (str_concat (str_concat "Test: " name) " (expecting failure)");
+       actual <- test;
+       if eq_bool actual expected then print "Success\n" else
+         do { print "Test failed\n"; exit 1; }; };
+
+// Test that contains0 |= contains0
 contains0 <- parse_core_mod "arrays" "contains0";
-mr_solver_debug 1 contains0 contains0;
+run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;

src/SAWScript/Prover/MRSolver/Monad.hs

@@ -66,8 +66,6 @@ data MRFailure
   | MalformedDefsFun Term
   | MalformedComp Term
   | NotCompFunType Term
-  | CoIndHypMismatchWidened FunName FunName CoIndHyp
-  | CoIndHypMismatchFailure (NormComp, NormComp) (NormComp, NormComp)
     -- | A local variable binding
   | MRFailureLocalVar LocalName MRFailure
     -- | Information about the context of the failure
@@ -81,8 +79,8 @@ ppWithPrefix :: PrettyInCtx a => String -> a -> PPInCtxM SawDoc
 ppWithPrefix str a = (pretty str <>) <$> nest 2 <$> (line <>) <$> prettyInCtx a
 
 -- | Pretty-print two objects, prefixed with a 'String' and with a separator
-ppWithPrefixSep :: PrettyInCtx a => String -> a -> String -> a ->
-                   PPInCtxM SawDoc
+ppWithPrefixSep :: (PrettyInCtx a, PrettyInCtx b) =>
+                   String -> a -> String -> b -> PPInCtxM SawDoc
 ppWithPrefixSep d1 t2 d3 t4 =
   prettyInCtx t2 >>= \d2 -> prettyInCtx t4 >>= \d4 ->
   return $ group (pretty d1 <> nest 2 (line <> d2) <> line <>
@@ -124,13 +122,6 @@ instance PrettyInCtx MRFailure where
     ppWithPrefix "Could not handle computation:" t
   prettyInCtx (NotCompFunType tp) =
     ppWithPrefix "Not a computation or computational function type:" tp
-  prettyInCtx (CoIndHypMismatchWidened nm1 nm2 _) =
-    ppWithPrefixSep "[Internal] Trying to widen co-inductive hypothesis on:" nm1 "," nm2
-  prettyInCtx (CoIndHypMismatchFailure (tm1, tm2) (tm1', tm2')) =
-    do pp <- ppWithPrefixSep "" tm1 "|=" tm2
-       pp' <- ppWithPrefixSep "" tm1' "|=" tm2'
-       return $ "Could not match co-inductive hypothesis:" <> pp' <> line <>
-                                              "with goal:" <> pp
   prettyInCtx (MRFailureLocalVar x err) =
     local (x:) $ prettyInCtx err
   prettyInCtx (MRFailureCtx ctx err) =
@@ -184,16 +175,34 @@ data CoIndHyp = CoIndHyp {
   -- from outermost to innermost; that is, the uvars as "seen from outside their
   -- scope", which is the reverse of the order of 'mrUVars', below
   coIndHypCtx :: [(LocalName,Term)],
+  -- | The LHS function name
+  coIndHypLHSFun :: FunName,
+  -- | The RHS function name
+  coIndHypRHSFun :: FunName,
   -- | The LHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
   coIndHypLHS :: [Term],
   -- | The RHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
   coIndHypRHS :: [Term]
 } deriving Show
 
+-- | Extract the @i@th argument on either the left- or right-hand side of a
+-- coinductive hypothesis
+coIndHypArg :: CoIndHyp -> Either Int Int -> Term
+coIndHypArg (CoIndHyp _ _ _ args1 _) (Left i) = args1 !! i
+coIndHypArg (CoIndHyp _ _ _ _ args2) (Right i) = args2 !! i
+
 -- | A map from pairs of function names to co-inductive hypotheses over those
 -- names
 type CoIndHyps = Map (FunName, FunName) CoIndHyp
 
+instance PrettyInCtx CoIndHyp where
+  prettyInCtx (CoIndHyp ctx f1 f2 args1 args2) =
+    local (const $ map fst $ reverse ctx) $
+    prettyAppList [return (ppCtx ctx <> "."),
+                   prettyInCtx (FunBind f1 args1 CompFunReturn),
+                   return "|=",
+                   prettyInCtx (FunBind f2 args2 CompFunReturn)]
+
 -- | An assumption that a named function refines some specificaiton. This has
 -- the form
 --
@@ -244,14 +253,20 @@ data MRState = MRState {
   mrsVars :: MRVarMap
 }
 
+-- | The exception type for MR. Solver, which is either a 'MRFailure' or a
+-- widening request
+data MRExn = MRExnFailure MRFailure
+           | MRExnWiden FunName FunName [Either Int Int]
+           deriving Show
+
 -- | Mr. Monad, the monad used by MR. Solver, which has 'MRInfo' as as a
 -- shared environment, 'MRState' as state, and 'MRFailure' as an exception
 -- type, all over an 'IO' monad
 newtype MRM a = MRM { unMRM :: ReaderT MRInfo (StateT MRState
-                                              (ExceptT MRFailure IO)) a }
+                                              (ExceptT MRExn IO)) a }
               deriving (Functor, Applicative, Monad, MonadIO,
                         MonadReader MRInfo, MonadState MRState,
-                                            MonadError MRFailure)
+                                            MonadError MRExn)
 
 instance MonadTerm MRM where
   mkTermF = liftSC1 scTermF
@@ -301,23 +316,41 @@ runMRM sc timeout debug assumps m =
                               mriUVars = [], mriCoIndHyps = Map.empty,
                               mriAssumptions = true_tm }
      let init_st = MRState { mrsVars = Map.empty }
-     runExceptT $ flip evalStateT init_st $ flip runReaderT init_info $ unMRM m
+     res <- runExceptT $ flip evalStateT init_st $
+       flip runReaderT init_info $ unMRM m
+     case res of
+       Right a -> return $ Right a
+       Left (MRExnFailure failure) -> return $ Left failure
+       Left exn -> fail ("runMRM: unexpected internal exception: " ++ show exn)
+
+-- | Throw an 'MRFailure'
+throwMRFailure :: MRFailure -> MRM a
+throwMRFailure = throwError . MRExnFailure
 
 -- | Apply a function to any failure thrown by an 'MRM' computation
-mapFailure :: (MRFailure -> MRFailure) -> MRM a -> MRM a
-mapFailure f m = catchError m (throwError . f)
+mapMRFailure :: (MRFailure -> MRFailure) -> MRM a -> MRM a
+mapMRFailure f m = catchError m $ \case
+  MRExnFailure failure -> throwError $ MRExnFailure $ f failure
+  e -> throwError e
+
+-- | Catch any 'MRFailure' raised by a computation
+catchFailure :: MRM a -> (MRFailure -> MRM a) -> MRM a
+catchFailure m f =
+  m `catchError` \case
+  MRExnFailure failure -> f failure
+  e -> throwError e
 
 -- | Try two different 'MRM' computations, combining their failures if needed.
 -- Note that the 'MRState' will reset if the first computation fails.
 mrOr :: MRM a -> MRM a -> MRM a
 mrOr m1 m2 =
-  catchError m1 $ \err1 ->
-  catchError m2 $ \err2 ->
-  throwError $ MRFailureDisj err1 err2
+  catchFailure m1 $ \err1 ->
+  catchFailure m2 $ \err2 ->
+  throwMRFailure $ MRFailureDisj err1 err2
 
 -- | Run an 'MRM' computation in an extended failure context
 withFailureCtx :: FailCtx -> MRM a -> MRM a
-withFailureCtx ctx = mapFailure (MRFailureCtx ctx)
+withFailureCtx ctx = mapMRFailure (MRFailureCtx ctx)
 
 {-
 -- | Catch any errors thrown by a computation and coerce them to a 'Left'
@@ -394,11 +427,20 @@ mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize
 -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in
 -- the order as seen "from the outside"
 mrUVarCtx :: MRM [(LocalName,Term)]
-mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars
+mrUVarCtx = reverse <$> mrUVarCtxRev
+
+-- | Get the current context of uvars as a list of variable names and their
+-- types as SAW core 'Term's, with the most recently bound uvar first, i.e., in
+-- the order as seen "from the inside"
+mrUVarCtxRev :: MRM [(LocalName,Term)]
+mrUVarCtxRev = map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars
 
 -- | Get the type of a 'Term' in the current uvar context
 mrTypeOf :: Term -> MRM Term
-mrTypeOf t = mrUVarCtx >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t
+mrTypeOf t =
+  -- NOTE: scTypeOf' wants the type context in the most recently bound var
+  -- first, i.e., in the mrUVarCtxRev order
+  mrUVarCtxRev >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t
 
 -- | Check if two 'Term's are convertible in the 'MRM' monad
 mrConvertible :: Term -> Term -> MRM Bool
@@ -419,7 +461,7 @@ mrFunOutType fname args =
        debugPrint 0 ("Expected: " ++ show (length vars) ++
                      ", found: " ++ show (length args))
        debugPretty 0 ("For function: " <> pp_fname <> " with type: " <> pp_ftype)
-       error"mrFunOutType"
+       error "mrFunOutType"
 
 -- | Turn a 'LocalName' into one not in a list, adding a suffix if necessary
 uniquifyName :: LocalName -> [LocalName] -> LocalName
@@ -430,16 +472,19 @@ uniquifyName nm nms =
     Just nm' -> nm'
     Nothing -> error "uniquifyName"
 
+-- | Turn a list of 'LocalName's into one names not in a list, adding suffixes
+-- if necessary
+uniquifyNames :: [LocalName] -> [LocalName] -> [LocalName]
+uniquifyNames [] _ = []
+uniquifyNames (nm:nms) nms_other =
+  let nm' = uniquifyName nm nms_other in
+  nm' : uniquifyNames nms (nm' : nms_other)
+
 -- | Run a MR Solver computation in a context extended with a universal
 -- variable, which is passed as a 'Term' to the sub-computation. Note that any
 -- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
-withUVar nm tp m =
-  do nm' <- uniquifyName nm <$> map fst <$> mrUVars
-     assumps' <- mrAssumptions >>= liftTerm 0 1
-     local (\info -> info { mriUVars = (nm',tp) : mriUVars info,
-                            mriAssumptions = assumps' }) $
-       mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
+withUVar nm (Type tp) m = withUVars [(nm,tp)] (\[v] -> m v)
 
 -- | Run a MR Solver computation in a context extended with a universal variable
 -- and pass it the lifting (in the sense of 'incVars') of an MR Solver term
@@ -453,16 +498,25 @@ withUVarLift nm tp t m =
 -- The variables are bound "outside in", meaning the first variable in the list
 -- is bound outermost, and so will have the highest deBruijn index.
 withUVars :: [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
-withUVars = helper [] where
-  -- The extra input list gives the variables that have already been bound, in
-  -- order from most to least recently bound
-  helper :: [Term] -> [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
-  helper vars [] m = m $ reverse vars
-  helper vars ((nm,tp):ctx) m =
-    -- FIXME: I think substituting here is wrong, but works on closed terms, so
-    -- it's fine to use at the top level at least...
-    substTerm 0 vars tp >>= \tp' ->
-    withUVarLift nm (Type tp') vars $ \var vars' -> helper (var:vars') ctx m
+withUVars [] f = f []
+withUVars ctx f =
+  do nms <- uniquifyNames (map fst ctx) <$> map fst <$> mrUVars
+     let ctx_u = zip nms $ map (Type . snd) ctx
+     assumps' <- mrAssumptions >>= liftTerm 0 (length ctx)
+     vars <- reverse <$> mapM (liftSC1 scLocalVar) [0 .. length ctx - 1]
+     local (\info -> info { mriUVars = reverse ctx_u ++ mriUVars info,
+                            mriAssumptions = assumps' }) $
+       foldr (\nm m -> mapMRFailure (MRFailureLocalVar nm) m) (f vars) nms
+
+-- | Run a MR Solver in a top-level context, i.e., with no uvars or assumptions
+withNoUVars :: MRM a -> MRM a
+withNoUVars m =
+  do true_tm <- liftSC1 scBool True
+     local (\info -> info { mriUVars = [], mriAssumptions = true_tm }) m
+
+-- | Run a MR Solver in a context of only the specified UVars, no others
+withOnlyUVars :: [(LocalName,Term)] -> MRM a -> MRM a
+withOnlyUVars vars m = withNoUVars $ withUVars vars $ const m
 
 -- | Build 'Term's for all the uvars currently in scope, ordered from least to
 -- most recently bound
@@ -699,32 +753,13 @@ _mrSubstEVarsStrict = mrSubstEVarsStrict
 mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
 mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 
--- | Run a compuation under the additional co-inductive assumption that
--- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are
--- the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ are the given
--- argument lists, and @x1, ..., xn@ is the current context of uvars. If
--- while running the given computation a 'CoIndHypMismatchWidened' error is
--- reached with the given names, the state is restored and the computation is
--- re-run with the widened hypothesis. This is done recursively, meaning this
--- function will only return once no 'CoIndHypMismatchWidened' errors are
--- raised with the given names.
-withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
-withCoIndHyp nm1 args1 nm2 args2 m =
-  do ctx <- mrUVarCtx
-     withCoIndHyp' (nm1, nm2) (CoIndHyp ctx args1 args2) m
-
--- | The main loop of 'withCoIndHyp'
-withCoIndHyp' :: (FunName, FunName) -> CoIndHyp -> MRM a -> MRM a
-withCoIndHyp' (nm1, nm2) hyp@(CoIndHyp _ args1 args2) m =
-  do mrDebugPPPrefixSep 1 "withCoIndHyp" (FunBind nm1 args1 CompFunReturn)
-                                    "|=" (FunBind nm2 args2 CompFunReturn)
-     st <- get
-     hyps' <- Map.insert (nm1, nm2) hyp <$> mrCoIndHyps
-     (local (\info -> info { mriCoIndHyps = hyps' }) m) `catchError` \case
-       CoIndHypMismatchWidened nm1' nm2' hyp' | nm1 == nm1' && nm2 == nm2'
-         -> -- FIXME: Could restoring the state here cause any problems?
-            put st >> withCoIndHyp' (nm1, nm2) hyp' m
-       e -> throwError e
+-- | Run a compuation under an additional co-inductive assumption
+withCoIndHypRaw :: CoIndHyp -> MRM a -> MRM a
+withCoIndHypRaw hyp m =
+  do debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
+     hyps' <- Map.insert (coIndHypLHSFun hyp,
+                          coIndHypRHSFun hyp) hyp <$> mrCoIndHyps
+     local (\info -> info { mriCoIndHyps = hyps' }) m
 
 -- | Generate fresh evars for the context of a 'CoIndHyp' and
 -- substitute them into its arguments and right-hand side
@@ -791,8 +826,8 @@ mrPPInCtx a =
 
 -- | Pretty-print the result of 'ppWithPrefixSep' relative to the current uvar
 -- context to 'stderr' if the debug level is at least the 'Int' provided
-mrDebugPPPrefixSep :: PrettyInCtx a => Int -> String -> a -> String -> a ->
-                      MRM ()
+mrDebugPPPrefixSep :: (PrettyInCtx a, PrettyInCtx b) =>
+                      Int -> String -> a -> String -> b -> MRM ()
 mrDebugPPPrefixSep i pre a1 sp a2 =
   mrUVars >>= \ctx ->
   debugPretty i $

src/SAWScript/Prover/MRSolver/SMT.hs

@@ -177,6 +177,7 @@ mrProvableRaw prop_term =
 -- | Test if a Boolean term over the current uvars is provable given the current
 -- assumptions
 mrProvable :: Term -> MRM Bool
+mrProvable (asBool -> Just b) = return b
 mrProvable bool_tm =
   do assumps <- mrAssumptions
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
@@ -276,12 +277,10 @@ mrAssertProveEq :: Term -> Term -> MRM ()
 mrAssertProveEq t1 t2 =
   do success <- mrProveEq t1 t2
      if success then return () else
-       throwError (TermsNotEq t1 t2)
+       throwMRFailure (TermsNotEq t1 t2)
 
--- | The main workhorse for 'prProveEq'. Build a Boolean term expressing that
--- the third and fourth arguments, whose type is given by the second. This is
--- done in a continuation monad so that the output term can be in a context with
--- additional universal variables.
+-- | The main workhorse for 'mrProveEq'. Build a Boolean term expressing that
+-- the third and fourth arguments, whose type is given by the second.
 mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM TermInCtx
 
 {-
@@ -309,6 +308,10 @@ mrProveEqH var_map _tp t1 (asEVarApp var_map -> Just (evar, args, Nothing)) =
      success <- mrTrySetAppliedEVar evar args t1'
      TermInCtx [] <$> liftSC1 scBool success
 
+-- For unit types, always return true
+mrProveEqH _ (asTupleType -> Just []) _ _ =
+  TermInCtx [] <$> liftSC1 scBool True
+
 -- For the nat, bitvector, Boolean, and integer types, call mrProveEqSimple
 mrProveEqH _ (asDataType -> Just (pn, [])) t1 t2
   | primName pn == "Prelude.Nat" =