diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal index 3b9bdd0bc..b1790dc0e 100644 --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -57,6 +57,12 @@ library import: warnings exposed-modules: Data.ShareMap Language.Fixpoint.Conditional.Z3 + Language.Fixpoint.Counterexample + Language.Fixpoint.Counterexample.Build + Language.Fixpoint.Counterexample.Check + Language.Fixpoint.Counterexample.JSON + Language.Fixpoint.Counterexample.SMT + Language.Fixpoint.Counterexample.Types Language.Fixpoint.Defunctionalize Language.Fixpoint.Graph Language.Fixpoint.Graph.Deps @@ -158,6 +164,7 @@ library , smtlib-backends-process >= 0.3 , stm , store + , scientific >= 0.3.7 , vector < 0.14 , syb , text diff --git a/src/Language/Fixpoint/Counterexample.hs b/src/Language/Fixpoint/Counterexample.hs new file mode 100644 index 000000000..c62c16c20 --- /dev/null +++ b/src/Language/Fixpoint/Counterexample.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} + +module Language.Fixpoint.Counterexample + ( tryCounterExample + ) where + +import Language.Fixpoint.Types +import Language.Fixpoint.Counterexample.JSON (jsonCex) +import Language.Fixpoint.Types.Config (Config, counterexample) +import Language.Fixpoint.Solver.EnvironmentReduction (dropLikelyIrrelevantBindings) + +import Language.Fixpoint.Counterexample.Types +import Language.Fixpoint.Counterexample.Build +import Language.Fixpoint.Counterexample.Check + +import qualified Data.HashMap.Strict as Map + +import Control.Monad.IO.Class +import Control.Monad (forM_) + +-- TODO: Remove variables from the counter example that got mapped to +-- the "wrong" type in smt format (e.g. to an int while not being one). + +-- TODO: Ideally `Result` would not have `SubcId` in its generic. Instead, this +-- should just always be contained in a `Result`. Right now, our counterexample +-- will contain a bunch of meaningless `SubcId` as we need to read it from +-- the result. + +-- | Try to get a counter example for the given unsafe clauses (if any). +tryCounterExample + :: MonadIO m + => Show info + => Fixpoint info + => Loc info + => PPrint info + => Config + -> SInfo info + -> Result (SubcId, info) + -> m (Result (SubcId, info)) +tryCounterExample cfg si res@Result + { resStatus = Unsafe _ cids' + , resCounterexamples = cexs' + } | counterexample cfg = do + -- Build program from constraints + prog <- hornToProg cfg si + + -- Check the constraints, returning a substitution map + let cids = fst <$> cids' + smtcex <- checkProg cfg si prog cids + + -- Extend the smt counterexample to include additional bind info + let cexs = toFullCex si <$> smtcex + + -- Store the counterexamples as JSON + forM_ cexs $ jsonCex cfg si + return res { resCounterexamples = cexs <> cexs' } +tryCounterExample _ _ res = return res + +-- | Extend an SMT counterexample to a full counterexample. +toFullCex :: SInfo info -> SMTCounterexample -> FullCounterexample (SubcId, info) +toFullCex si (Counterexample env subcid trace) = Counterexample + { cexEnv = substToCexEnv si subcid env + , cexConstraint = subcid + , cexFrames = toFullCex si <$> trace + } + +-- | Extend an SMT counterexample environment (i.e. the substitution map) to a +-- full counterexample environment. With this, the variables are indexed by +-- `BindId` and they contain also their refinement type and user info. +substToCexEnv :: SInfo info -> SubcId -> Subst -> CexEnv (SubcId, info) +substToCexEnv si subcid (Su sub) = benv { beBinds = binds } + where + benv = bs si + horn = cm si Map.! subcid + ibenv = senv horn + + -- The constraint head symbol and refinement + (csym, creft, _) = beBinds benv Map.! cbind horn + + symbols = exprSymbolsSet $ crhs horn + symRefts = Map.fromList $ clhs benv horn + -- Make sure the rhs is always in the relevant set! + relevant = Map.insert csym creft + -- Get the relevant bindings i.e. those that affect the outcome of the rhs. + $ dropLikelyIrrelevantBindings symbols symRefts + + -- This new substitution map contains only the relevant bindings. + sub' = Map.intersectionWith const sub relevant + + -- Filter out all bind ids that are not in the constraint. Then map the + -- symbols back to the bind ids. + binds = Map.mapMaybe trans + . Map.filterWithKey (\bid _ -> memberIBindEnv bid ibenv) + . beBinds + $ benv + + -- Extends a symbol from the bind environment with a concrete instance (and + -- the subcid, but this just there to match the type signature of `Result` + -- later down the line). + trans (sym, sreft, info) = extend <$> Map.lookup sym sub' + where + extend ex = (sym, sreft, (ex, (subcid, info))) diff --git a/src/Language/Fixpoint/Counterexample/Build.hs b/src/Language/Fixpoint/Counterexample/Build.hs new file mode 100644 index 000000000..b52bf8158 --- /dev/null +++ b/src/Language/Fixpoint/Counterexample/Build.hs @@ -0,0 +1,334 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} + +module Language.Fixpoint.Counterexample.Build + ( hornToProg + ) where + + +import Language.Fixpoint.Types +import Language.Fixpoint.Counterexample.Types +import Language.Fixpoint.Types.Config (Config, queryFile, save) +import Language.Fixpoint.Solver.Sanitize (symbolEnv) +import Language.Fixpoint.Misc (ensurePath) +import Language.Fixpoint.SortCheck (Elaborate (..)) + +import qualified Language.Fixpoint.Utils.Files as Ext + +import Data.Maybe (fromMaybe) +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as Map +import qualified Data.Set as Set +import Data.List (find, sortBy, foldl') +import qualified Data.List as List + +import Control.Monad (foldM) +import Control.Monad.State +import Control.Monad.Reader +import Control.Monad (when, forM) + +-- | The enviroment used to build a program. +data BuildEnv info = BuildEnv + { info :: !(SInfo info) + -- ^ The horn constraints from which we build the program. + , symbols :: !SymEnv + -- ^ Contains the sorts of symbols, which we need for declarations. + } + +-- | The monad used to convert a set of horn constraints to +-- the imperative function format. See Prog for the format. +type MonadBuild info m = (MonadReader (BuildEnv info) m, MonadState Prog m, MonadIO m) + +type Binding = (BindId, Symbol, SortedReft) + +-- | Make an imperative program from horn clauses. This +-- can be used to generate a counter example. +hornToProg + :: MonadIO m + => Fixpoint info + => Show info + => Config + -> SInfo info + -> m Prog +hornToProg cfg si = do + -- Initial program is just an empty main. + let initial = Prog + { functions = Map.singleton mainName (Func [] []) + , definitions = mempty + } + let env = BuildEnv + { info = si + , symbols = symbolEnv cfg si + } + + -- Run monad that adds all horn clauses to the program + prog <- sortBodies <$> evalStateT (runReaderT buildProg env) initial + + -- Save the program in a file + liftIO . when (save cfg) $ do + let file = queryFile Ext.Prog cfg + liftIO . putStrLn $ "Saving counterexample program: " ++ file ++ "\n" + ensurePath file + writeFile file . show . pprint $ prog + + -- Return the generated program + return prog + +-- | Build the entire program structure from the constraints +-- inside the monad +buildProg :: MonadBuild info m => m Prog +buildProg = do + addDefinitions + constraints <- reader $ cm . info + mapM_ addHorn constraints + get + +addDefinitions :: MonadBuild info m => m () +addDefinitions = do + eqs <- reader $ aenvEqs . ae . info + mapM_ addEquation eqs + +addEquation :: MonadBuild info m => Equation -> m () +addEquation equ = do + -- Build a constraint from the equation + let call = foldl' EApp (EVar $ eqName equ) (EVar . fst <$> eqArgs equ) + let eq = PAtom Eq call $ eqBody equ + constraint' <- elaborate' $ PAll (eqArgs equ) eq + + modify (\s -> s { definitions = constraint' : definitions s }) + +-- | Given a horn clause, generates a body for a function. +-- +-- The body is generated from the lhs of the horn clause. +-- +-- This body is added to the function given by the kvar +-- on the rhs of the horn clause. If there was no kvar, +-- it is added to the main function. +addHorn :: MonadBuild info m => SimpC info -> m () +addHorn horn = do + -- Make the lhs of the clause into statements + lhs <- hornLhsToStmts horn + + -- The rhs has a special case depending on + -- if it is a kvar or not. + (name, decl, rhs) <- case crhs horn of + PKVar name sub -> do + decl <- getSig name + rhs <- substToStmts sub + return (name, decl, rhs) + e -> return (mainName, [], [Assert e]) + + -- Add the horn clause as a function body + let cid = fromMaybe (-1) $ sid horn + -- TODO: The exploration ideally doesn't need the ordering on the calls for + -- the pruning of branches. + -- TODO: It might be better to replace Let statements by a substitution map. + -- Sort the statements, let bindings should go first. Calls last. We want + -- to have all available variables at the start. + let statements = dedupCalls decl . List.sort $ lhs <> rhs + let body = Body cid $ statements + addFunc name $ Func decl [body] + +-- | Gets a signature of a KVar from its well foundedness constraint +getSig :: MonadBuild info m => Name -> m Signature +getSig kvar = do + -- Get the well foundedness constraint of the kvar + wfcs <- reader $ ws . info + let wfc = wfcs Map.! kvar + + -- Get the bind environment and bindings of the wfc + bindEnv <- reader $ bs . info + let ibinds = elemsIBindEnv . wenv $ wfc + + -- Lookup all Decl from the wfc using the ibinds + let asDecl (sym, sr, _) = Decl sym (sr_sort sr) + let decls = map (asDecl . flip lookupBindEnv bindEnv) ibinds + + -- Get the last Decl from the head of the wfc + let rhs = let (sym, sort, _) = wrft wfc in Decl sym sort + + -- Return the head + bindings as argument map + return $ rhs:decls + +-- | Defines some equalities between local variables +-- and the passed arguments given some substitution map. +substToStmts :: MonadBuild info m => Subst -> m [Statement] +substToStmts (Su sub) = do + let asEq (ksym, e) = Assume $ PAtom Eq (EVar ksym) e + return $ map asEq (Map.toList sub) + +-- | Converts the left hand side of the horn clause to a list +-- of assumptions (or calls given by a Name) +hornLhsToStmts :: MonadBuild info m => SimpC info -> m [Statement] +hornLhsToStmts horn = do + bindEnv <- reader $ bs . info + let lhs = relevantLhs bindEnv horn + lhs' <- filterLits . filterDuplicates $ lhs + stmts <- forM lhs' reftToStmts + return $ mconcat stmts + +relevantLhs :: BindEnv info -> SimpC info -> [Binding] +relevantLhs benv horn = + [ (bid, sym, ref) + | bid <- elemsIBindEnv $ senv horn + , let (sym, ref, _) = lookupBindEnv bid benv + ] + +filterDuplicates :: [Binding] -> [Binding] +filterDuplicates = foldr filter' [] + where + filter' e acc = case e `member` acc of + Nothing -> e:acc + Just _ -> acc + + snd' (_, x, _) = x + member e es = find (snd' e==) $ map snd' es + +filterLits :: MonadBuild info m => [Binding] -> m [Binding] +filterLits env = do + con <- reader $ gLits . info + dis <- reader $ dLits . info + let isLit (_, sym, _) = memberSEnv sym con || memberSEnv sym dis + return $ filter (not . isLit) env + +-- | Map a refinement to a declaration and constraint pair +reftToStmts :: MonadBuild info m => Binding -> m [Statement] +-- Ignore abstractions and functions, as they don't have refinements. +reftToStmts (_, _, RR { sr_sort = FAbs _ _ }) = return [] +reftToStmts (_, _, RR { sr_sort = FFunc _ _ }) = return [] +reftToStmts (bid, sym, RR + { sr_sort = sort + , sr_reft = Reft (v, e) + }) = do + -- Prefix the symbol if required. Otherwise, some symbols won't match their + -- fix$36$ version when substituting. + let sym' = symbol . prefixAlpha . symbolText $ sym + + -- Get correct sort for declaration + sort' <- elaborate' sort + let decl = Let $ Decl sym' sort' + + -- Get constraints from the expression. + let constraints = exprStmts bid e + -- Do substitution of self variable in the constraints + let sub = Su $ Map.singleton v (EVar sym) + return $ decl : subst sub constraints + +-- | Split the expression into a number of statements +-- +-- Note that kvars should only appear as conjuncted from the root expression, +-- or as the root itself. This function does not catch nested kvars. +exprStmts :: BindId -> Expr -> [Statement] +exprStmts bid = go + where + go (PAnd ps) = ps >>= go + -- TODO: Change call so it doesn't take a list of locations. + go (PKVar k su) = [Call bid [(k, su)]] + go e = [Assume e] + +-- | The sorts for the apply monomorphization only match if we do this elaborate +-- on the sort. Not sure why... +-- +-- This elaboration also happens inside the declaration of the symbol +-- environment, so that's where I got the idea. +elaborate' :: MonadBuild info m => Elaborate a => a -> m a +elaborate' x = do + symbols' <- reader symbols + return $ elaborate "elaborateSort" symbols' x + +-- | Add a function to the function map with index by its name. +-- If an entry already exists, it will merge the function +-- bodies. +addFunc :: MonadBuild info m => Name -> Func -> m () +addFunc kvar func = do + let merge (Func _ b) (Func d b') = Func d (b <> b') + prog <- get + let functions' = Map.insertWith merge kvar func $ functions prog + put $ prog { functions = functions' } + +-- | We try to place functions with as little kvars as possible first, as these +-- most likely find us a counterexample. Ideally, we do something less primitive +-- than just a sort though... +sortBodies :: Prog -> Prog +sortBodies prog = prog { functions = functions' } + where + functions' = sortFunc <$> functions prog + + sortFunc (Func sig bodies) = Func sig $ sortBy cmp bodies + cmp a b = count a `compare` count b + count (Body _ stmts) = length . filter isCall $ stmts + isCall (Call _ _) = True + isCall _ = False + +type Equivalents = HashMap Symbol ID +type ID = Int + +-- | Check if two symbols are equivalent. +symEq :: Equivalents -> Symbol -> Symbol -> Bool +symEq alias lhs rhs = Map.lookup lhs alias == Map.lookup rhs alias + +-- | Get a map of all equivalent symbols. I.e. symbols which were literally +-- defined to be by a statement of the form; assume x == y +getEqs :: Signature -> [Statement] -> Equivalents +getEqs sig statements = evalState getAliases' 0 + where + statements' = (Let <$> sig) <> statements + getAliases' = foldM go mempty statements' + + go acc (Let (Decl sym _)) = do + identifier <- fresh + return $ acc <> Map.singleton sym identifier + go acc (Assume (PAtom Eq lhs rhs)) + | EVar lhs' <- uncst lhs + , EVar rhs' <- uncst rhs = do + let identifier = Map.lookup lhs' acc + let old = Map.lookup rhs' acc + case (identifier, old) of + -- Add to aliases if both names are defined in the environment. + (Just identifier', Just old') -> do + let rename current = if current == old' then identifier' else current + return $ rename <$> acc + + -- Otherwise, just return the accumulator as is + _ -> return acc + go acc _ = return acc + + fresh = state $ \s -> (s, s + 1) + + uncst (ECst e _) = uncst e + uncst e = e + +-- | Deduplicate calls by building an equivalence map and checking whether +-- substitution maps are submaps of each other. +dedupCalls :: Signature -> [Statement] -> [Statement] +dedupCalls signature statements = dedup $ replace <$> statements + where + dedup = Set.toList . Set.fromList + + -- FIXME: I don't think this captures all cases! (has to do with ordering of + -- statements) + -- Replaces a submap subst with the bigger version. + replace (Call _ [(_, sub)]) + | Just v <- find (isSubmap' sub) statements = v + replace s = s + + isSubmap' sub (Call _ [(_, sub')]) = isSubmap eqs sub sub' + isSubmap' _ _ = False + + eqs = getEqs signature statements + +-- | Returns whether the first substitution map is a sub-assignment of the +-- second. In other words, if the first subst can be ignored if both as it +-- places the same (but less) constraints as the second subst. +isSubmap :: Equivalents -> Subst -> Subst -> Bool +isSubmap eqs (Su sub0) (Su sub1) = null remaining + where + remaining = Map.differenceWith diff sub0 sub1 + + diff (EVar sym0) (EVar sym1) + | not $ eq' sym0 sym1 = Just $ EVar sym0 + diff _ _ = Nothing + + eq' = symEq eqs diff --git a/src/Language/Fixpoint/Counterexample/Check.hs b/src/Language/Fixpoint/Counterexample/Check.hs new file mode 100644 index 000000000..820cea2f7 --- /dev/null +++ b/src/Language/Fixpoint/Counterexample/Check.hs @@ -0,0 +1,230 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} + +module Language.Fixpoint.Counterexample.Check + ( checkProg + ) where + +import Language.Fixpoint.Types +import Language.Fixpoint.Counterexample.Types +import Language.Fixpoint.Counterexample.SMT as SMT +import Language.Fixpoint.Types.Config (Config) + +import Data.Maybe (fromJust, catMaybes) +import Data.List (find) +import qualified Data.HashMap.Strict as Map +import qualified Data.HashSet as Set + +import Control.Monad.State.Strict +import Control.Monad.Reader +import Control.Monad (forM, foldM, when) + +-- | Environment for the counter example generation. +data CheckEnv = CheckEnv + { program :: !Prog + -- ^ The program we are checking + , context :: !SMT.Context + -- ^ The SMT context we write the constraints from the program to. + , maxIterations :: !Int + -- ^ The checker is an iterative deepening DFS. This is the maximum number of + -- iterations before we give up entirely. + } + +data CheckState = CheckState + { curRec :: !Int + -- ^ The number of recursive unfoldings currently in the path. + , maxRec :: !Int + -- ^ The maximum number of recursive unfoldings we allow in any path for this + -- iteration. + } + +instance SMTContext CheckEnv where + smtContext = context + +-- | The monad used to generate counter examples from a Prog. +type MonadCheck m = (MonadReader CheckEnv m, MonadIO m, MonadState CheckState m) + +-- | The runner is a computation path in the program. We use this as an argument +-- to pass around the remainder of a computation. This way, we can pop paths in +-- the SMT due to conditionals. Allowing us to retain anything prior to that. +type Runner m = m (Maybe SMTCounterexample) + +-- | Check the given constraints to try and find a counter example. +checkProg :: MonadIO m => Config -> SInfo info -> Prog -> [SubcId] -> m [SMTCounterexample] +checkProg cfg si prog cids = SMT.withContext cfg si check + where + check ctx = runCheck cids CheckEnv + { program = prog + , context = ctx + -- TODO: Perhaps the max iterative depth should be a user parameter? + , maxIterations = 3 + } + +-- | Runs the program checker with the monad stack +-- unwrapped. +runCheck :: MonadIO m => [SubcId] -> CheckEnv -> m [SMTCounterexample] +runCheck cids env = rd . st $ checkAll cids + where + rd = flip runReaderT env + st = flip evalStateT CheckState + { curRec = 0 + , maxRec = 0 + } + +-- | Try to find a counter example for all the given constraints. +checkAll :: MonadCheck m => [SubcId] -> m [SMTCounterexample] +checkAll cids = do + -- Using definitions as quantified axioms is really slow! Perhaps this should + -- be feature gated, or we should just never do this as there are most likely + -- faster alternatives. I'll leave it like this for now. + when False setDefinitions + cexs <- forM cids checkConstraint + return $ catMaybes cexs + +setDefinitions :: MonadCheck m => m () +setDefinitions = do + defs <- reader $ definitions . program + mapM_ SMT.assume defs + +-- | Check a specific constraint id. This will only do actual +-- checks for constraints without a KVar on the rhs, as we cannot +-- really generate a counter example for these constraints. +checkConstraint :: MonadCheck m => SubcId -> m (Maybe SMTCounterexample) +checkConstraint cid = do + Func _ bodies <- fromJust <$> getFunc mainName + let cmp (Body bid _) = bid == cid + let scope = Scope + { path = mempty + , constraint = cid + , binders = mempty + , visited = mempty + } + case find cmp bodies of + Just body -> iterateDepth $ runBody scope body SMT.getModel + Nothing -> return Nothing + +-- | Does iterative deepening of search; it checks if the current runner +-- produces a counterexample. If not, it increments the allowed recursion limit. +-- It will continue doing so until either a counterexample is found or the +-- iteration limit is reached. +iterateDepth :: MonadCheck m => Runner m -> Runner m +iterateDepth runner = do + cex <- runner + curLimit <- gets maxRec + limit <- reader maxIterations + case cex of + Just _ -> return cex + _ | curLimit > limit -> return Nothing + _ -> do + modify $ \s -> s { maxRec = maxRec s + 1 } + cex' <- iterateDepth runner + modify $ \s -> s { maxRec = maxRec s - 1 } + return cex' + +-- | Run a function. This essentially makes one running branch for +-- each body inside of the function. It will try each branch +-- sequentially, returning early if a counterexample was found. +runFunc :: MonadCheck m => Name -> Scope -> Runner m -> Runner m +runFunc name scope' runner = withRec name scope' $ \scope -> do + -- Lookup function bodies + func <- getFunc name + sat <- SMT.checkSat + case func of + -- This sub tree is already unsatisfiable. Adding more constraints never + -- makes it satisfiable and, as such, we prune this subtree. + _ | not sat -> return Nothing + + -- Unconstrained function body, so there is no counterexample here. This + -- would be equivalent to trying to create an inhabitant of {v:a | false}, + -- which doesn't exist. + Nothing -> return Nothing + + -- Constrained function body + Just (Func _ bodies) -> do + -- Generate all execution paths (as runners). + let runner' body = runBody (extendScope scope body) body runner + let paths = runner' <$> bodies + foldRunners paths + +-- | Increments the recursive call counter for the entire remaining runner. We +-- only allow `maxRec` recursive calls over an entire path, not of the subtree. +withRec :: MonadCheck m => Name -> Scope -> (Scope -> Runner m) -> Runner m +withRec name scope runner + | name `Set.member` visited scope = do + modify $ \s -> s { curRec = curRec s + 1 } + limit <- recursionLimit + result <- if limit then return Nothing else runner' + modify $ \s -> s { curRec = curRec s - 1 } + return result + | otherwise = runner' + where + runner' = runner scope { visited = Set.insert name (visited scope)} + +-- | Returns whether the recursion limit has been hit. +recursionLimit :: MonadCheck m => m Bool +recursionLimit = do + nrec <- gets curRec + limit <- gets maxRec + return $ nrec > limit + +-- | Run the statements in the body. If there are no more statements to run, +-- this will execute the Runner that was passed as argument. +-- +-- The passed runner here is thus the rest of the computation, when we "return" +-- from this function. +runBody :: MonadCheck m => Scope -> Body -> Runner m -> Runner m +runBody scope' body@(Body _ _) runner = SMT.inScope $ go scope' body + where + go _ (Body _ []) = runner + go scope (Body cid (stmt:ss)) = do + -- The remaining statements becomes a new Runner + let runner' = flip go (Body cid ss) + -- We pass this runner, such that it can be called at a later + -- point (possibly multiple times) if we were to encounter a call. + runStatement scope stmt runner' + +-- | Run the current statement. It might adjust the substitution map +-- for a portion of the statements, which is why the runner takes a +-- new substitution map as an argument. +runStatement :: MonadCheck m => Scope -> Statement -> (Scope -> Runner m) -> Runner m +runStatement scope stmt runner = do + -- Runner with the old subst map. + let runner' = runner scope + let stmt' = subst (binders scope) stmt + case stmt' of + Assume e -> SMT.assume e >> runner' + Assert e -> SMT.assert e >> runner' + Let decl -> do + scope' <- SMT.declare scope decl + runner scope' + Call origin calls -> do + let scope' app = Scope + { path = origin : path scope + -- We fake a SubcId here, it will later get mapped into the scope + -- when we decide which body to run. + , constraint = 0 + , binders = app + , visited = visited scope + } + let runCall (name, app) = runFunc name (scope' app) runner' + foldRunners $ runCall <$> calls + +-- | Get a function from the program given its name. +getFunc :: MonadCheck m => Name -> m (Maybe Func) +getFunc name = do + funcs <- reader $ functions . program + return $ Map.lookup name funcs + +-- | Fold the runners, selecting the first one that produced a counterexample, +-- if any. +foldRunners :: MonadCheck m => [Runner m] -> Runner m +foldRunners = foldM select Nothing + where + select Nothing r = r + select cex _ = return cex + +-- | Extend the scope to include the id of the body, i.e. the `SubcId`. +extendScope :: Scope -> Body -> Scope +extendScope scope (Body cid _) = scope { constraint = cid } diff --git a/src/Language/Fixpoint/Counterexample/JSON.hs b/src/Language/Fixpoint/Counterexample/JSON.hs new file mode 100644 index 000000000..0cc229a3b --- /dev/null +++ b/src/Language/Fixpoint/Counterexample/JSON.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NamedFieldPuns #-} + +module Language.Fixpoint.Counterexample.JSON + ( Symbol + , Refinement + , Expr + , Variable (..) + , Constraint (..) + , Counterexample (..) + , formatCex + , jsonCex + ) where + +import qualified Language.Fixpoint.Utils.Files as Ext +import qualified Language.Fixpoint.Types as F +import qualified Language.Fixpoint.Misc as F +import qualified Language.Fixpoint.Types.Config as F +import GHC.Generics (Generic) +import Data.Aeson (FromJSON, ToJSON, encodeFile) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.HashMap.Strict as Map +import qualified Data.ByteString as B +import qualified Data.ByteString.Char8 as B (lines) + +import Control.Exception +import Control.Monad.IO.Class + +data Counterexample = Counterexample + { environment :: ![Variable] + , constraint :: !Constraint + } deriving (Generic, Show) + +instance FromJSON Counterexample +instance ToJSON Counterexample + +data Variable = Variable + { symbol :: !Symbol + , expression :: !Expr + , refinement :: !Refinement + , must_instance :: !(Maybe Counterexample) + , location :: !(Maybe Location) + } deriving (Generic, Show) + +instance FromJSON Variable +instance ToJSON Variable + +data Constraint = Constraint + { concrete :: !Expr + , synthesized :: !Refinement + , required :: !Refinement + , location :: !(Maybe Location) + } deriving (Generic, Show) + +instance FromJSON Constraint +instance ToJSON Constraint + +-- data RowColumn = RowColumn +-- { row :: !Int +-- , col :: !Int +-- } deriving (Generic, Show) +-- +-- instance FromJSON RowColumn +-- instance ToJSON RowColumn +-- +-- data Location = Location +-- { start :: !RowColumn +-- , end :: !RowColumn +-- , path :: !Path +-- } deriving (Generic, Show) + +data Span = Span + { start :: !Int + , length :: !Int + } deriving (Generic, Show) + +instance FromJSON Span +instance ToJSON Span + +data Location = Location + { span :: !Span + , path :: !Path + } deriving (Generic, Show) + +instance FromJSON Location +instance ToJSON Location + +type Path = Text +type Symbol = Text +type Refinement = Text +type Expr = Text + +-- TODO: Check liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Tidy.hs +-- from LH to copy how they make the environment "tidy". +jsonCex :: (F.Loc info, MonadIO m) => F.Config -> F.SInfo info -> F.FullCounterexample (F.SubcId, info) -> m () +jsonCex cfg si cex | F.save cfg = do + cex' <- formatCex si cex + let ext = Ext.Cex . fromIntegral . F.cexConstraint $ cex + let file = F.queryFile ext cfg + liftIO . putStrLn $ "Saving counterexample json: " ++ file ++ "\n" + liftIO $ F.ensurePath file + liftIO $ encodeFile file cex' +jsonCex _ _ _ = return () + +formatCex :: (F.Loc info, MonadIO m) => F.SInfo info -> F.FullCounterexample (F.SubcId, info) -> m Counterexample +formatCex si cex = do + env <- formatEnv si cex + cst <- formatConstraint si cex + return Counterexample + { environment = env + , constraint = cst + } + +formatEnv :: (F.Loc info, MonadIO m) => F.SInfo info -> F.FullCounterexample (F.SubcId, info) -> m [Variable] +formatEnv si cex = do + mapM formatVar vars + where + vars = Map.toList . F.beBinds . F.cexEnv $ cex + + formatVar (bid, (sym, synth, (conc, (_, info)))) = do + must <- mapM (formatCex si) $ F.cexFrames cex Map.!? bid + loc <- getLocation info + return Variable + { symbol = ppFormat sym + , expression = ppFormat conc + , refinement = ppFormat synth + , must_instance = must + , location = loc + } + +formatConstraint :: (F.Loc info, MonadIO m) => F.SInfo info -> F.FullCounterexample (F.SubcId, info) -> m Constraint +formatConstraint si cex = do + let horn = F.cm si Map.! F.cexConstraint cex + let cheadId = F.cbind horn + let binds = F.beBinds . F.cexEnv $ cex + + -- Get the head of the constraint. + let (_csym, csynth, (cconcrete, (_, info))) = binds Map.! cheadId + + -- Get checked expr + let cexpr = F.crhs horn + let ccheck = withExpr csynth cexpr + + loc <- getLocation info + + return Constraint + { concrete = ppFormat cconcrete + , synthesized = ppFormat csynth + , required = ppFormat ccheck + , location = loc + } + where + withExpr sr e = sr { F.sr_reft = F.Reft (sort, e) } + where + F.Reft (sort, _) = F.sr_reft sr + +ppFormat :: F.PPrint a => a -> Text +ppFormat = T.pack . show . F.pprintTidy F.Lossy + +-- | Storing spans with columns and rows doesn't really make sense when +-- printing. The JSON format instead just stores a range. This function does +-- the conversion, though it might be a bit slow, as we are quite literally +-- counting the number of characters to reach the span. +getLocation :: MonadIO m => F.Loc info => info -> m (Maybe Location) +getLocation i = liftIO $ handle ignore $ do + -- Helpers + let getRow = F.unPos . F.sourceLine + let getCol = F.unPos . F.sourceColumn + + -- The initial SourceSpan + let F.SS { sp_start, sp_stop } = F.srcSpan i + let path = F.sourceName sp_start + let startRow = getRow sp_start - 1 + let endRow = getRow sp_stop + let startCol = getCol sp_start - 1 + let endCol = getCol sp_stop + + -- Split between what comes before and the rows that actually contain the + -- content. + content <- B.lines <$> B.readFile path + let (before, rest) = splitAt startRow content + let (content', _) = splitAt (endRow - startRow) rest + + -- This part remove the start and end of the rows in which the final span + -- lies. The start and end is dictated by the columns. + (hs, l) <- case unsnoc content' of + Just v -> return v + _ -> throwIO $ userError "incorrect range" + let content'' = hs <> [B.take endCol l] + (h, ls) <- case uncons content'' of + Just v -> return v + _ -> throwIO $ userError "incorrect range" + let content''' = B.drop startCol h : ls + + -- Calculate the final start and length, including the number of newline + -- characters. + let start = sum (B.length <$> before) + Prelude.length before + startCol + let len = sum (B.length <$> content''') + Prelude.length content''' - 1 + + return . Just $ Location + { span = Span + { start = start + , length = len + } + , path = T.pack path + } + +ignore :: MonadIO m => IOException -> m (Maybe a) +ignore = const $ return Nothing + +-- TODO: Remove these definitions of unsnoc and uncons once the GHC version is +-- high enough such that they're in Data.List. Don't forget to add them to the +-- import in this case! +unsnoc :: [a] -> Maybe ([a], a) +unsnoc = foldr (\x -> Just . maybe ([], x) (\(~(a, b)) -> (x : a, b))) Nothing + +uncons :: [a] -> Maybe (a, [a]) +uncons [] = Nothing +uncons (x:xs) = Just (x, xs) diff --git a/src/Language/Fixpoint/Counterexample/SMT.hs b/src/Language/Fixpoint/Counterexample/SMT.hs new file mode 100644 index 000000000..b002b2543 --- /dev/null +++ b/src/Language/Fixpoint/Counterexample/SMT.hs @@ -0,0 +1,185 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE OverloadedStrings #-} + +module Language.Fixpoint.Counterexample.SMT + ( SMT.Context + , SMTContext (..) + , withContext + , declare + , assert + , assume + , inScope + , checkSat + , getModel + , getModelUnsafe + ) where + +import Language.Fixpoint.Types +import Language.Fixpoint.Types.Config (Config, srcFile) +import Language.Fixpoint.Solver.Sanitize (symbolEnv) +import Language.Fixpoint.Counterexample.Types +import qualified Language.Fixpoint.Smt.Interface as SMT + +import Control.Monad.Reader +import Control.Monad (guard, (>=>)) + +import qualified Data.HashMap.Strict as Map +import qualified Data.Text as T +import Text.Read (readMaybe) +import Data.String (IsString(..)) +import Data.Bifunctor (first) +import Data.Char (chr) +import Data.List (intercalate, foldl') + +class SMTContext a where + smtContext :: a -> SMT.Context + +type MonadSMT r m = (SMTContext r, MonadReader r m, MonadIO m) + +-- | Run the checker with the SMT solver context. +withContext :: MonadIO m => Config -> SInfo info -> (SMT.Context -> m a) -> m a +withContext cfg si inner = do + let file = srcFile cfg <> ".prog" + let env = symbolEnv cfg si + ctx <- liftIO $ SMT.makeContextWithSEnv cfg file env + + !result <- inner ctx + + liftIO $ SMT.cleanupContext ctx + return result + +-- | Declare a new symbol, returning an updated substitution +-- given with this new symbol in it. The substitution map is +-- required to avoid duplicating variable names. +declare :: MonadSMT s m => Scope -> Decl -> m Scope +declare scope (Decl sym sort) = do + ctx <- reader smtContext + let sym' = scopeSym scope sym + liftIO $ SMT.smtDecl ctx sym' sort + let Su sub = binders scope + let binders' = Su $ Map.insert sym (EVar sym') sub + return scope { binders = binders' } + +-- | Assert the given expression. +assert :: MonadSMT s m => Expr -> m () +assert = assume . PNot + +-- | Assume the given expression. +assume :: MonadSMT s m => Expr -> m () +assume e = do + ctx <- reader smtContext + liftIO $ SMT.smtAssert ctx e + +-- | Run the checker within a scope (i.e. a push/pop pair). +inScope :: MonadSMT s m => m a -> m a +inScope inner = do + ctx <- reader smtContext + liftIO $ SMT.smtPush ctx + !result <- inner + liftIO $ SMT.smtPop ctx + return result + +-- | Check if there is a counterexample, returing one if it is available. +checkSat :: MonadSMT s m => m Bool +checkSat = do + ctx <- reader smtContext + liftIO $ not <$> SMT.smtCheckUnsat ctx + +-- | Returns a model, with as precondition that the SMT solver had a satisfying +-- assignment prior to this. Hence, this is "unsafe", as calling it without +-- this precondition will crash the program. +getModelUnsafe :: MonadSMT s m => m SMTCounterexample +getModelUnsafe = do + ctx <- reader smtContext + sub <- liftIO $ SMT.smtGetModel ctx + return $ smtSubstToCex sub + +-- | Checks satisfiability, returning a model if available. +getModel :: MonadSMT s m => m (Maybe SMTCounterexample) +getModel = do + sat <- checkSat + if sat then Just <$> getModelUnsafe else return Nothing + + +-- | Transform an SMT substitution, which contains SMT scoped symbols, into a +-- layered, tree-like counterexample. +smtSubstToCex :: Subst -> SMTCounterexample +smtSubstToCex (Su sub) = foldl' (flip $ uncurry insertCex) dummyCex traces + where + -- | Unwind SMT names. + renames = first unscopeSym <$> Map.toList sub + + -- | Keep just the ones that were introduced by the counterexample checker. + traces = [ (k, e) | (Just k, e) <- renames ] + + -- | A dummy counterexample to fill empty entries on insertion + dummyCex = Counterexample mempty 0 mempty + + -- | Insert a scoped name with its expression into the SMT counterexample + insertCex (sym, cid, trace) e = go $ reverse trace + where + go :: Trace -> SMTCounterexample -> SMTCounterexample + go (t:ts) cex = cex + { cexFrames = Map.insertWith (const $ go ts) t (go ts dummyCex) $ cexFrames cex + } + go _ cex@Counterexample + { cexEnv = Su su + } = cex + { cexConstraint = cid + , cexEnv = Su . Map.insert sym e $ su + } + +-- | Returns a version of a symbol with the scope encoded into its name. +scopeSym :: Scope -> Symbol -> Symbol +scopeSym scope sym = symbol name + where + name = intercalate bindSep strs + strs = symbolString <$> progPrefix : sym : cid : paths + cid = symbol . show . constraint $ scope + paths = symbol . show <$> path scope + +-- | We encode the trace of a symbol in its name. This way, +-- we do not lose it in the SMT solver. This function translates +-- the encoding back. +unscopeSym :: Symbol -> Maybe (Symbol, SubcId, Trace) +unscopeSym sym = do + -- Remove the escape tokens from the SMT formatted symbol + sym' <- escapeSmt . symbolText $ sym + + -- Check if it is in the program form + (name, cid, trace) <- case T.splitOn bindSep sym' of + (prefix:name:cid:trace) -> do + guard $ prefix == progPrefix + return (name, cid, trace) + _ -> Nothing + + let read' :: Read a => T.Text -> Maybe a + read' = readMaybe . T.unpack + + -- Try to parse the trace and constraint id + trace' <- sequence $ read' <$> trace + cid' <- read' cid + return (symbol name, cid', trace') + +-- | Remove escape tokens applied to the input string when it was formatted to +-- SMT string. +escapeSmt :: T.Text -> Maybe T.Text +escapeSmt = go False . T.split (=='$') + where + go _ [] = return "" + go escape (t:ts) = txt t <> go (not escape) ts + where + txt | escape = readMaybe . T.unpack >=> return . T.singleton . chr + | otherwise = return + +-- | The separator used to encode the stack trace (of binders) inside of smt +-- symbols. +bindSep :: IsString a => a +bindSep = "@" + +-- | Prefix used to show that this smt symbol was generated during a run of +-- the program. +progPrefix :: IsString a => a +progPrefix = "prog" + diff --git a/src/Language/Fixpoint/Counterexample/Types.hs b/src/Language/Fixpoint/Counterexample/Types.hs new file mode 100644 index 000000000..3d8f6c3fc --- /dev/null +++ b/src/Language/Fixpoint/Counterexample/Types.hs @@ -0,0 +1,209 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.Fixpoint.Counterexample.Types + ( Counterexample (..) + , SMTCounterexample + , FullCounterexample + , CexEnv + , Trace + , Scope (..) + + , Prog (..) + , Name + , Func (..) + , Body (..) + , Statement (..) + , Decl (..) + , Signature + + , mainName + , dbg -- TODO: Remove this on code clean-up! + ) where + +import Language.Fixpoint.Types +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as Map +import Data.HashSet (HashSet) +import Data.Bifunctor (second) + +import Text.PrettyPrint.HughesPJ ((<+>), ($+$)) +import qualified Text.PrettyPrint.HughesPJ as PP + +import Control.Monad.IO.Class + +dbg :: (MonadIO m, PPrint a) => a -> m () +dbg = liftIO . print . pprint + +-- | A counterexample that was mapped from an SMT result. It is a simple mapping +-- from symbol to concrete instance. +type SMTCounterexample = Counterexample Subst + +-- | A scope contains the current binders in place as well as the path traversed +-- to reach this scope. +data Scope = Scope + { path :: !Trace + -- ^ The path traversed to reach the scope. + , constraint :: !SubcId + -- ^ The current constraint, which dictates the binders. + , binders :: !Subst + -- ^ The binders available in the current scope. + , visited :: HashSet Name + -- ^ The functions that have already been visited. This is to track whether we + -- want to expand a function or if we have already hit the recursion limit. + } + deriving (Eq, Ord, Show) + +-- | A stack trace is built from multiple frame ids. This is mostly used for +-- SMT encodings. These traces are made into a tree like representation in the +-- actual counterexample object. +type Trace = [BindId] + +-- | A program, containing multiple function definitions mapped by their name. +data Prog = Prog + { functions :: (HashMap Name Func) + -- ^ The functions of this program. + , definitions :: [Expr] + -- ^ Constraints that need to hold originating from define statements. + } + deriving Show + +-- | Identifier of a function. All KVars are translated into functions, so it is +-- just an alias. +type Name = KVar + +-- | A function symbol corresponding to a Name. +data Func = Func !Signature ![Body] + deriving Show + +-- | Signature of a function. +type Signature = [Decl] + +-- | A sequence of statements. +data Body = Body !SubcId ![Statement] + deriving Show + +-- | A statement used to introduce/check constraints, together with its location +-- information. +-- +-- WARNING: We rely on the order of these declarations for the derive of Ord. +-- Specifically, to sort the statements in this same order for the builder. +-- Let bindings should appear first so everything is in scope and correctly +-- named. Calls should be last: this allows us to prune branches when executing +-- them. Do not change these unless you know what you are doing! +data Statement + = Let !Decl + -- ^ Introduces a new variable. + | Assume !Expr + -- ^ Constraints a variable. + | Assert !Expr + -- ^ Checks whether a predicate follows given prior constraints. + | Call !BindId ![(Name, Subst)] + -- ^ Call to function. The bind id is used to trace callstacks. I.e. it is the + -- caller of the function. + deriving (Show, Eq, Ord) + +-- | A declaration of a Symbol with a Sort. +data Decl = Decl !Symbol !Sort + deriving (Show, Eq, Ord) + +-- | The main function, which any horn clause without a KVar on the rhs will be +-- added to. +mainName :: Name +mainName = KV "main" + +instance PPrint Prog where + pprintTidy tidy prog = pcstr $+$ pfuncs + where + pcstr = PP.vcat + . PP.punctuate "\n" + . map (pprintTidy tidy) + . definitions + $ prog + + pfuncs = PP.vcat + . PP.punctuate "\n" + . map (uncurry $ ppfunc tidy) + . Map.toList + . functions + $ prog + + +instance PPrint Func where + pprintTidy tidy = ppfunc tidy anonymous + where + anonymous = KV "_" + +ppfunc :: Tidy -> Name -> Func -> PP.Doc +ppfunc tidy name (Func sig bodies) = pdecl $+$ pbody $+$ PP.rbrace + where + pdecl = "fn" <+> pname <+> psig <+> PP.lbrace + pname = pprintTidy tidy name + psig = PP.parens + . PP.hsep + . PP.punctuate PP.comma + . map (pprintTidy tidy) + $ sig + pbody = vpunctuate "||" + . map (PP.nest 4 . pprintTidy tidy) + $ bodies + + vpunctuate _ [] = mempty + vpunctuate _ [d] = d + vpunctuate p (d:ds) = d $+$ p $+$ vpunctuate p ds + +instance PPrint Decl where + pprintTidy tidy (Decl sym sort) = (psym <> PP.colon) <+> psort + where + psym = pprintTidy tidy sym + psort = pprintTidy tidy sort + +instance PPrint Body where + pprintTidy tidy (Body cid stmts) = pcid $+$ pstmts + where + pcid = "// constraint id" <+> pprintTidy tidy cid + pstmts = PP.vcat + . map (pprintTidy tidy) + $ stmts + +instance PPrint Statement where + pprintTidy tidy (Let decl) = "let" <+> pprintTidy tidy decl + pprintTidy tidy (Assume exprs) = "assume" <+> pprintTidy tidy exprs + pprintTidy tidy (Assert exprs) = "assert" <+> pprintTidy tidy exprs + pprintTidy tidy (Call bid calls) = "call" <+> porigin $+$ pcalls + where + porigin = "// bind id" <+> pprintTidy tidy bid + pcalls = PP.vcat $ PP.nest 4 . pcall <$> calls + pcall (name, sub) = pprintTidy tidy name <+> pprintTidy tidy sub + +instance Subable Statement where + syms (Let decl) = syms decl + syms (Assume e) = syms e + syms (Assert e) = syms e + syms (Call _ calls) = mconcat $ syms . (\(Su sub) -> sub) . snd <$> calls + + substa _ (Let decl) = Let decl + substa f (Assume e) = Assume $ substa f e + substa f (Assert e) = Assert $ substa f e + substa f (Call bid calls) = Call bid $ mapsub (substa f) <$> calls + + substf _ (Let decl) = Let decl + substf f (Assume e) = Assume $ substf f e + substf f (Assert e) = Assert $ substf f e + substf f (Call bid calls) = Call bid (mapsub (substf f) <$> calls) + + subst _ (Let decl) = Let decl + subst sub (Assume e) = Assume $ subst sub e + subst sub (Assert e) = Assert $ subst sub e + subst sub (Call bid calls) = Call bid (mapsub (subst sub) <$> calls) + +mapsub :: (HashMap Symbol Expr -> HashMap Symbol Expr) -> (a, Subst) -> (a, Subst) +mapsub f = second (\(Su sub) -> Su $ f sub) + +instance Subable Decl where + syms (Decl sym _) = [sym] + + substa f (Decl sym sort) = Decl (substa f sym) sort + + substf f (Decl sym sort) = Decl (substf f sym) sort + + subst sub (Decl sym sort) = Decl (subst sub sym) sort diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs index 2642c6335..433a4dac1 100644 --- a/src/Language/Fixpoint/Smt/Interface.hs +++ b/src/Language/Fixpoint/Smt/Interface.hs @@ -50,6 +50,8 @@ module Language.Fixpoint.Smt.Interface ( , smtBracket, smtBracketAt , smtDistinct , smtPush, smtPop + , smtGetValues + , smtGetModel -- * Check Validity , checkValid @@ -75,6 +77,7 @@ import qualified Language.Fixpoint.Smt.Theories as Thy import Language.Fixpoint.Smt.Serialize () import Control.Applicative ((<|>)) import Control.Monad +import Control.Monad.IO.Class import Control.Exception import Data.ByteString.Builder (Builder) import qualified Data.ByteString.Builder as BS @@ -83,6 +86,7 @@ import qualified Data.ByteString.Lazy.Char8 as Char8 import Data.Char import qualified Data.HashMap.Strict as M import Data.Maybe (fromMaybe) +import Data.List (foldl') import qualified Data.Text as T import qualified Data.Text.Encoding as TE import qualified Data.Text.IO @@ -93,6 +97,7 @@ import System.Console.CmdArgs.Verbosity import System.FilePath import System.IO import qualified Data.Attoparsec.Text as A +import qualified Data.Scientific as S -- import qualified Data.HashMap.Strict as M import Data.Attoparsec.Internal.Types (Parser) import Text.PrettyPrint.HughesPJ (text) @@ -158,7 +163,7 @@ checkValids cfg f xts ps -------------------------------------------------------------------------------- {-# SCC command #-} -command :: Context -> Command -> IO Response +command :: Context -> Command -> IO Response -------------------------------------------------------------------------------- command Ctx {..} !cmd = do -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n") @@ -168,19 +173,15 @@ command Ctx {..} !cmd = do LBS.hPutStr h "\n" case cmd of CheckSat -> commandRaw - GetValue _ -> commandRaw _ -> SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok where commandRaw = do resp <- SMTLIB.Backends.command ctxSolver cmdBS - let respTxt = - TE.decodeUtf8With (const $ const $ Just ' ') $ - LBS.toStrict resp - parse respTxt - cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd + parse $ bs2txt resp + cmdBS = {-# SCC "Command-runSmt2" #-} smt2 ctxSymEnv cmd parse resp = do case A.parseOnly responseP resp of - Left e -> Misc.errorstar $ "SMTREAD:" ++ e + Left e -> Misc.errorstar $ "SMTREAD: " ++ e ++ "\n" ++ T.unpack resp Right r -> do let textResponse = "; SMT Says: " <> T.pack (show r) forM_ ctxLog $ \h -> @@ -189,48 +190,138 @@ command Ctx {..} !cmd = do Data.Text.IO.putStrLn textResponse return r +bs2txt :: Char8.ByteString -> T.Text +bs2txt = TE.decodeUtf8With (const $ const $ Just ' ') . LBS.toStrict + +smtGetValues :: MonadIO m => Context -> [Symbol] -> m Subst +smtGetValues _ [] = return $ Su M.empty +smtGetValues Ctx {..} symbols = do + let cmd = key "get-value" (parenSeqs $ map (smt2 ctxSymEnv) symbols) + bytestring <- liftIO $ SMTLIB.Backends.command ctxSolver cmd + let txt = bs2txt bytestring + case A.parseOnly valuesP txt of + Left e -> Misc.errorstar $ "Parse error on get-value: " ++ e ++ "\n\n" ++ show txt + Right sol -> return sol + +smtGetModel :: MonadIO m => Context -> m Subst +smtGetModel Ctx {..} = do + let cmd = "(get-model)" + bytestring <- liftIO $ SMTLIB.Backends.command ctxSolver cmd + let txt = bs2txt bytestring + case A.parseOnly modelP txt of + Left e -> Misc.errorstar $ "Parse error on get-model: " ++ e ++ "\n\n" ++ show txt + Right sol -> return sol + smtSetMbqi :: Context -> IO () smtSetMbqi me = interact' me SetMbqi type SmtParser a = Parser T.Text a +modelP :: SmtParser Subst +modelP = parenP $ do + defs <- A.many' defP + return $ Su (M.fromList defs) + +defP :: SmtParser (Symbol, Expr) +defP = parenP $ do + _ <- A.string "define-fun" + sym <- symbolP + sortP + e <- exprP + return (sym, e) + +sortP :: SmtParser () +sortP = do + -- A type is just an S-Expression, we can reuse the parser + let tyP = void exprP + _ <- parenP $ A.many' tyP + tyP + +valuesP :: SmtParser Subst +valuesP = parenP $ do + vs <- A.many' valueP + return $ Su (M.fromList vs) + +valueP :: SmtParser (Symbol, Expr) +valueP = parenP $ do + sym <- symbolP + e <- exprP + return (sym, e) + +exprP :: SmtParser Expr +exprP = appP <|> litP + +appP :: SmtParser Expr +appP = do + (e:es) <- parenP $ A.many1' exprP + return $ foldl' EApp e es + +litP :: SmtParser Expr +litP = scientificP <|> boolP <|> bitvecP <|> (EVar <$> symbolP) + +scientificP :: SmtParser Expr +scientificP = do + val <- A.scientific + let con = case S.floatingOrInteger val of + Left double -> R double + Right int -> I int + return $ ECon con + +boolP :: SmtParser Expr +boolP = trueP <|> falseP + where + trueP = A.string "true" >> return PTrue + falseP = A.string "false" >> return PFalse + +bitvecP :: SmtParser Expr +bitvecP = do + _ <- A.char '#' + (bv, _) <- A.match (hexP <|> binP) + return $ ECon (L bv $ sizedBitVecSort "x") + where + hexP = do + _ <- A.char 'x' + _ <- A.hexadecimal :: SmtParser Integer + return () + binP = do + _ <- A.char 'b' + _ <- A.many1' (A.char '0' <|> A.char '1') + return () + +symbolP :: SmtParser Symbol +symbolP = {- SCC "symbolP" -} do + A.skipSpace + raw <- A.takeWhile1 (not . exclude) + A.skipSpace + return $ symbol raw + where + exclude x = isSpace x || x == '(' || x == ')' + +parenP :: SmtParser a -> SmtParser a +parenP inner = do + A.skipSpace + _ <- A.char '(' + res <- inner + _ <- A.char ')' + A.skipSpace + return res + responseP :: SmtParser Response -responseP = {- SCC "responseP" -} A.char '(' *> sexpP - <|> A.string "sat" *> return Sat +responseP = {- SCC "responseP" -} + A.string "sat" *> return Sat <|> A.string "unsat" *> return Unsat <|> A.string "unknown" *> return Unknown - -sexpP :: SmtParser Response -sexpP = {- SCC "sexpP" -} A.string "error" *> (Error <$> errorP) - <|> Values <$> valuesP + <|> (Error <$> errorP) errorP :: SmtParser T.Text -errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")" - -valuesP :: SmtParser [(Symbol, T.Text)] -valuesP = A.many1' pairP <* A.char ')' - -pairP :: SmtParser (Symbol, T.Text) -pairP = {- SCC "pairP" -} - do A.skipSpace - _ <- A.char '(' - !x <- symbolP - A.skipSpace - !v <- valueP - _ <- A.char ')' - return (x,v) - -symbolP :: SmtParser Symbol -symbolP = {- SCC "symbolP" -} symbol <$> A.takeWhile1 (not . isSpace) - -valueP :: SmtParser T.Text -valueP = {- SCC "valueP" -} negativeP - <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c)) - -negativeP :: SmtParser T.Text -negativeP - = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')' - return $ "(" <> v <> ")" +errorP = do + A.skipSpace + _ <- A.string "error" + A.skipSpace + _ <- A.string "(\"" + res <- A.takeWhile1 (/= '"') + _ <- A.string "\")" + return res -------------------------------------------------------------------------- -- | SMT Context --------------------------------------------------------- diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs index 83ad4114c..4447e4055 100644 --- a/src/Language/Fixpoint/Smt/Theories.hs +++ b/src/Language/Fixpoint/Smt/Theories.hs @@ -171,6 +171,191 @@ mapPrj = "Map_project" mapShift = "Map_shift" -- See [Map key shift] mapToSet = "Map_to_set" +-- | (seq.unit elem) +-- Sequence with a single element `elem`. +seqUnit :: TheorySymbol +seqUnit = Thy + { tsSym = "Seq$unit" + , tsRaw = "seq.unit" + -- forall a. a -> Seq a + , tsSort = FAbs 0 $ FFunc (FVar 0) $ seqSort 0 + , tsInterp = Theory + } + +-- | (as seq.empty (Seq Int)) +-- The empty sequence of integers. +seqEmpty :: TheorySymbol +seqEmpty = Thy + { tsSym = "Seq$empty" + , tsRaw = "seq.empty" + -- forall a. Seq a + , tsSort = FAbs 0 $ seqSort 0 + , tsInterp = Theory + } + +-- | (seq.++ a b c) +-- Concatenation of one or more sequences. +-- +-- We define the concat in fixpoint as just joining two sequences. +seqConcat :: TheorySymbol +seqConcat = Thy + { tsSym = "Seq$concat" + , tsRaw = "seq.++" + -- forall a. Seq a -> Seq a -> Seq a + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (seqSort 0) $ seqSort 0 + , tsInterp = Theory + } + +-- | (seq.len s) +-- Sequence length. Returns an integer. +seqLen :: TheorySymbol +seqLen = Thy + { tsSym = "Seq$len" + , tsRaw = "seq.len" + -- forall a. Seq a -> Int + , tsSort = FAbs 0 $ FFunc (seqSort 0) intSort + , tsInterp = Theory + } + +-- | (seq.extract s offset length) +-- Retrieves sub-sequence of `s` at `offset`. +seqExtract :: TheorySymbol +seqExtract = Thy + { tsSym = "Seq$extract" + , tsRaw = "seq.extract" + -- forall a. Seq a -> Int -> Int -> Seq a + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc intSort $ FFunc intSort $ seqSort 0 + , tsInterp = Theory + } + +-- | (seq.indexof s sub [offset]) +-- Retrieves first position of `sub` in `s`, -1 if there are no occurrences. +-- +-- We don't take the optional `offset` argument in fixpoint. +seqIndexOf :: TheorySymbol +seqIndexOf = Thy + { tsSym = "Seq$indexof" + , tsRaw = "seq.indexof" + -- forall a. Seq a -> a -> Int + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (FVar 0) $ intSort + , tsInterp = Theory + } + +-- | (seq.at s offset) +-- Sub-sequence of length 1 at offset in s. +seqAt :: TheorySymbol +seqAt = Thy + { tsSym = "Seq$at" + , tsRaw = "seq.at" + -- forall a. Seq a -> Int -> Seq a + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc intSort $ seqSort 0 + , tsInterp = Theory + } + +-- | (seq.nth s offset) +-- Element at offset in s. If offset is out of bounds the result is +-- under-specified. In other words, it is treated as a fresh variable. +seqNth :: TheorySymbol +seqNth = Thy + { tsSym = "Seq$nth" + , tsRaw = "seq.nth" + -- forall a. Seq a -> Int -> a + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc intSort $ FVar 0 + , tsInterp = Theory + } + +-- | (seq.contains s sub) +-- Does s contain the sub-sequence sub? +seqContains :: TheorySymbol +seqContains = Thy + { tsSym = "Seq$contains" + , tsRaw = "seq.contains" + -- forall a. Seq a -> Seq a -> Bool + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (seqSort 0) $ boolSort + , tsInterp = Theory + } + +-- | (seq.prefixof pre s) +-- Is pre a prefix of s? +seqPrefixOf :: TheorySymbol +seqPrefixOf = Thy + { tsSym = "Seq$prefixof" + , tsRaw = "seq.prefixof" + -- forall a. Seq a -> Seq a -> Bool + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (seqSort 0) $ boolSort + , tsInterp = Theory + } + +-- | (seq.suffixof suf s) +-- Is suf a suffix of s? +seqSuffixOf :: TheorySymbol +seqSuffixOf = Thy + { tsSym = "Seq$suffixof" + , tsRaw = "seq.suffixof" + -- forall a. Seq a -> Seq a -> Bool + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (seqSort 0) $ boolSort + , tsInterp = Theory + } + +-- | (seq.replace s src dst) +-- Replace the first occurrence of src by dst in s. +seqReplace :: TheorySymbol +seqReplace = Thy + { tsSym = "Seq$replace" + , tsRaw = "seq.replace" + -- forall a. Seq a -> a -> a -> Seq a + , tsSort = FAbs 0 $ FFunc (seqSort 0) $ FFunc (FVar 0) $ FFunc (FVar 0) $ seqSort 0 + , tsInterp = Theory + } + +-- | (seq.map fn s) +-- Map function `fn` (an expression of sort (Array S T)) on sequence `s` of sort +-- (Seq S). +seqMap :: TheorySymbol +seqMap = Thy + { tsSym = "Seq$map" + , tsRaw = "seq.map" + -- TODO: Define correct type (this requires array type) + , tsSort = intSort + , tsInterp = Theory + } + +-- (seq.mapi fn o s) +-- Map function `fn` (an expression of sort (Array Int S T)) on offset `o` and +-- sequence `s` of sort (Seq S). +seqMapi :: TheorySymbol +seqMapi = Thy + { tsSym = "Seq$mapi" + , tsRaw = "seq.mapi" + -- TODO: Define correct type (this requires array type) + , tsSort = intSort + , tsInterp = Theory + } + +-- | (seq.fold_left fn b s) +-- Fold function `fn` (an expression of sort (Array T S T)) on initial value `b` +-- of sort `T` and sequence `s` of sort (Seq S). +seqFoldLeft :: TheorySymbol +seqFoldLeft = Thy + { tsSym = "Seq$fold_left" + , tsRaw = "seq.fold_left" + -- TODO: Define correct type (this requires array type) + , tsSort = intSort + , tsInterp = Theory + } + +-- | (seq.fold_lefti fn o b s) +-- Fold function `fn` (an expression of sort (Array Int T S T)) on offset `o`, +-- initial value `b` of sort `T` and sequence `s` of sort (Seq S). +seqFoldLefti :: TheorySymbol +seqFoldLefti = Thy + { tsSym = "Seq$fold_lefti" + , tsRaw = "seq.fold_lefti" + -- TODO: Define correct type (this requires array type) + , tsSort = intSort + , tsInterp = Theory + } + -- [Interaction between Map and Set] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- Function mapToSet: Convert a map to a set. The map's key may be of @@ -423,6 +608,7 @@ smt2SmtSort SBool = "Bool" smt2SmtSort SString = fromText string smt2SmtSort SSet = fromText set smt2SmtSort SMap = fromText map +smt2SmtSort (SSeq a) = parens $ "Seq" <+> smt2SmtSort a smt2SmtSort (SBitVec n) = key "_ BitVec" (bShow n) smt2SmtSort (SVar n) = "T" <> bShow n smt2SmtSort (SData c []) = symbolBuilder c @@ -506,7 +692,7 @@ theorySymbols ds = fromListSEnv $ -- SHIFTLAM uninterpSymbols -------------------------------------------------------------------------------- interpSymbols :: [(Symbol, TheorySymbol)] -------------------------------------------------------------------------------- -interpSymbols = +interpSymbols = interpSeq <> [ interpSym setEmp emp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort) , interpSym setEmpty emp (FAbs 0 $ FFunc intSort (setSort $ FVar 0)) , interpSym setSng sng (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0)) @@ -586,7 +772,6 @@ interpSymbols = , interpSym intbv64Name "(_ int2bv 64)" (FFunc intSort bv64) , interpSym bv32intName "(_ bv2int 32)" (FFunc bv32 intSort) , interpSym bv64intName "(_ bv2int 64)" (FFunc bv64 intSort) - ] where -- (sizedBitVecSort "Size1") @@ -621,6 +806,28 @@ interpSymbols = mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1) (mapSort (FVar 0) (FVar 1)) +interpSeq :: [(Symbol, TheorySymbol)] +interpSeq = interpTheorySymbol <$> + [ seqUnit + , seqEmpty + , seqConcat + , seqLen + , seqExtract + , seqIndexOf + , seqAt + , seqNth + , seqContains + , seqPrefixOf + , seqSuffixOf + , seqReplace + , seqMap + , seqMapi + , seqFoldLeft + , seqFoldLefti + ] + +interpTheorySymbol :: TheorySymbol -> (Symbol, TheorySymbol) +interpTheorySymbol ts = (tsSym ts, ts) interpBvUop :: Symbol -> (Symbol, TheorySymbol) interpBvUop name = interpSym' name bvUopSort diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs index 8a565a051..b7874248c 100644 --- a/src/Language/Fixpoint/Solver.hs +++ b/src/Language/Fixpoint/Solver.hs @@ -57,10 +57,12 @@ import Language.Fixpoint.Types hiding (GInfo(..), fi) import qualified Language.Fixpoint.Types as Types (GInfo(..)) import Language.Fixpoint.Minimize (minQuery, minQuals, minKvars) import Language.Fixpoint.Solver.Instantiate (instantiate) +import Language.Fixpoint.Counterexample import Control.DeepSeq import qualified Data.ByteString as B import Data.Maybe (catMaybes) + --------------------------------------------------------------------------- -- | Solve an .fq file ---------------------------------------------------- --------------------------------------------------------------------------- @@ -187,7 +189,7 @@ solveNative !cfg !fi0 = solveNative' cfg fi0 (return . crashResult (errorMap fi0)) crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a) -crashResult m err' = Result res mempty mempty mempty +crashResult m err' = Result res mempty mempty mempty mempty where res = Crash es msg es = catMaybes [ findError m e | e <- errs err' ] @@ -271,13 +273,8 @@ reduceFInfo cfg fi = do solveNative' !cfg !fi0 = do si6 <- simplifyFInfo cfg fi0 res <- {- SCC "Sol.solve" -} Sol.solve cfg $!! si6 - -- rnf soln `seq` donePhase Loud "Solve2" - --let stat = resStatus res - -- saveSolution cfg res when (save cfg) $ saveSolution cfg res - -- writeLoud $ "\nSolution:\n" ++ showpp (resSolution res) - -- colorStrLn (colorResult stat) (show stat) - return res + tryCounterExample cfg si6 res -------------------------------------------------------------------------------- -- | Parse External Qualifiers ------------------------------------------------- @@ -290,9 +287,9 @@ parseFI :: FilePath -> IO (FInfo a) parseFI f = do str <- readFile f let fi = rr' f str :: FInfo () - return $ mempty { Types.quals = Types.quals fi - , Types.gLits = Types.gLits fi - , Types.dLits = Types.dLits fi } + return $ mempty { Types.quals = Types.quals fi + , Types.gLits = Types.gLits fi + , Types.dLits = Types.dLits fi } saveSolution :: Config -> Result a -> IO () saveSolution cfg res = when (save cfg) $ do diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs index 6b6229822..ccf024582 100644 --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -52,6 +52,7 @@ import Data.List (partition) -- import Data.Char (isUpper) import Control.Monad.State.Strict import qualified Data.HashMap.Strict as M +--import qualified Data.HashSet as HashSet import Data.Maybe (catMaybes) import Control.Exception.Base (bracket) diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs index fcf880ab4..ed0c479c7 100644 --- a/src/Language/Fixpoint/Solver/Solve.hs +++ b/src/Language/Fixpoint/Solver/Solve.hs @@ -45,7 +45,6 @@ mytrace _ x = {- trace -} x -------------------------------------------------------------------------------- solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a)) -------------------------------------------------------------------------------- - solve cfg fi = do whenLoud $ donePhase Misc.Loud "Worklist Initialize" vb <- getVerbosity @@ -244,7 +243,7 @@ result bindingsInSmt cfg wkl s = stat <- result_ bindingsInSmt2 cfg wkl s lift $ whenLoud $ putStrLn $ "RESULT: " ++ show (F.sid <$> stat) - F.Result (ci <$> stat) <$> solResult cfg s <*> solNonCutsResult s <*> return mempty + F.Result (ci <$> stat) <$> solResult cfg s <*> solNonCutsResult s <*> return mempty <*> return mempty where ci c = (F.subcId c, F.sinfo c) diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs index 75e8868ac..ca48f443f 100644 --- a/src/Language/Fixpoint/Types/Config.hs +++ b/src/Language/Fixpoint/Types/Config.hs @@ -94,6 +94,7 @@ data Config = Config , etaElim :: Bool -- ^ eta eliminate function definitions , gradual :: Bool -- ^ solve "gradual" constraints , ginteractive :: Bool -- ^ interactive gradual solving + , counterexample :: Bool -- ^ Tries to produce a counter example if unsafe , autoKuts :: Bool -- ^ ignore given kut variables , nonLinCuts :: Bool -- ^ Treat non-linear vars as cuts , noslice :: Bool -- ^ Disable non-concrete KVar slicing @@ -245,6 +246,7 @@ defConfig = Config { , minimalSol = False &= help "Shrink fixpoint by removing implied qualifiers" , gradual = False &= help "Solve gradual-refinement typing constraints" , ginteractive = False &= help "Interactive Gradual Solving" + , counterexample = False &= name "counterexample" &= help "Tries to produce a counter example for unsafe clauses" , autoKuts = False &= help "Ignore given Kut vars, compute from scratch" , nonLinCuts = False &= help "Treat non-linear kvars as cuts" , noslice = False &= help "Disable non-concrete KVar slicing" diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs index 98b4a6971..fbc104337 100644 --- a/src/Language/Fixpoint/Types/Constraints.hs +++ b/src/Language/Fixpoint/Types/Constraints.hs @@ -61,6 +61,9 @@ module Language.Fixpoint.Types.Constraints ( , qualBinds -- * Results + , Counterexample (..) + , FullCounterexample + , FixSolution , GFixSolution, toGFixSol , Result (..) @@ -263,6 +266,30 @@ subcId = mfromJust "subCId" . sid -- | Solutions and Results --------------------------------------------------------------------------- +-- | A counterexample in a tree like representation. +data Counterexample a = Counterexample + { cexEnv :: !a + -- ^ The environment in the current stack frame. + , cexConstraint :: !SubcId + -- ^ The constraint which the environment belongs to. + , cexFrames :: !(M.HashMap BindId (Counterexample a)) + -- ^ The counterexamples stack frames that can be explored from the current + -- environment. + } + deriving (Generic, Show, Functor) + +instance PPrint a => PPrint (Counterexample a) where + pprintTidy tidy (Counterexample env cid trace) = pcid $+$ penv $+$ ptrace + where + pcid = "in constraint" <+> pprintTidy tidy cid + penv = pprintTidy tidy env + ptrace = pprintTidy tidy trace + +-- | A counterexample that was extended with additional information from the +-- environment. It additionally includes types, bind ids and user info, aside +-- from what is already provided from an `SMTCounterexample`. +type FullCounterexample a = Counterexample (CexEnv a) + type GFixSolution = GFixSol Expr type FixSolution = M.HashMap KVar Expr @@ -273,12 +300,12 @@ newtype GFixSol e = GSol (M.HashMap KVar (e, [e])) toGFixSol :: M.HashMap KVar (e, [e]) -> GFixSol e toGFixSol = GSol - data Result a = Result - { resStatus :: !(FixResult a) - , resSolution :: !FixSolution + { resStatus :: !(FixResult a) + , resSolution :: !FixSolution , resNonCutsSolution :: !FixSolution , gresSolution :: !GFixSolution + , resCounterexamples :: ![FullCounterexample a] } deriving (Generic, Show, Functor) @@ -288,15 +315,16 @@ instance ToJSON a => ToJSON (Result a) where toJSON = toJSON . resStatus instance Semigroup (Result a) where - r1 <> r2 = Result stat soln nonCutsSoln gsoln + r1 <> r2 = Result stat soln nonCutsSoln gsoln cntExs where stat = resStatus r1 <> resStatus r2 soln = resSolution r1 <> resSolution r2 nonCutsSoln = resNonCutsSolution r1 <> resNonCutsSolution r2 gsoln = gresSolution r1 <> gresSolution r2 + cntExs = resCounterexamples r1 <> resCounterexamples r2 instance Monoid (Result a) where - mempty = Result mempty mempty mempty mempty + mempty = Result mempty mempty mempty mempty mempty mappend = (<>) unsafe, safe :: Result a @@ -414,6 +442,7 @@ instance (NFData a) => NFData (WfC a) instance (NFData a) => NFData (SimpC a) instance (NFData (c a), NFData a) => NFData (GInfo c a) instance (NFData a) => NFData (Result a) +instance (NFData a) => NFData (Counterexample a) instance Hashable Qualifier instance Hashable QualPattern diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs index 8654c0d29..b5db33e47 100644 --- a/src/Language/Fixpoint/Types/Environments.hs +++ b/src/Language/Fixpoint/Types/Environments.hs @@ -48,6 +48,7 @@ module Language.Fixpoint.Types.Environments ( , filterBindEnv, mapBindEnv, mapWithKeyMBindEnv, adjustBindEnv , bindEnvFromList, bindEnvToList, deleteBindEnv, elemsBindEnv , EBindEnv, splitByQuantifiers + , CexEnv -- * Information needed to lookup and update Solutions -- , SolEnv (..) @@ -99,6 +100,10 @@ instance PPrint a => PPrint (SizedEnv a) where type BindEnv a = SizedEnv (Symbol, SortedReft, a) newtype EBindEnv a = EB (BindEnv a) +-- | A counterexample environment. Contains an expression (the concrete +-- instance) aside from the regular symbol and refinement. +type CexEnv a = BindEnv (Expr, a) + splitByQuantifiers :: BindEnv a -> [BindId] -> (BindEnv a, EBindEnv a) splitByQuantifiers (BE i bs) ebs = ( BE i $ M.filterWithKey (\k _ -> notElem k ebs) bs , EB $ BE i $ M.filterWithKey (\k _ -> elem k ebs) bs diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs index 5e9ffbf32..3b9c6328b 100644 --- a/src/Language/Fixpoint/Types/Names.hs +++ b/src/Language/Fixpoint/Types/Names.hs @@ -61,6 +61,7 @@ module Language.Fixpoint.Types.Names ( , vvCon , tidySymbol , unKArgSymbol + , prefixAlpha -- * Widely used prefixes , anfPrefix @@ -106,6 +107,7 @@ module Language.Fixpoint.Types.Names ( , vvName , sizeName , bitVecName + , seqName -- , bvAndName, bvOrName, bvSubName, bvAddName , intbv32Name, intbv64Name, bv32intName, bv64intName , propConName @@ -683,11 +685,12 @@ intbv64Name = "int_to_bv64" bv32intName = "bv32_to_int" bv64intName = "bv64_to_int" -nilName, consName, sizeName, bitVecName :: Symbol +nilName, consName, sizeName, bitVecName, seqName :: Symbol nilName = "nil" consName = "cons" sizeName = "Size" bitVecName = "BitVec" +seqName = "Seq" mulFuncName, divFuncName :: Symbol diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs index 3b1e64217..e3556bf8c 100644 --- a/src/Language/Fixpoint/Types/Sorts.hs +++ b/src/Language/Fixpoint/Types/Sorts.hs @@ -37,7 +37,7 @@ module Language.Fixpoint.Types.Sorts ( , mapFVar , basicSorts, intSort, realSort, boolSort, strSort, funcSort -- , bitVec32Sort, bitVec64Sort - , setSort, bitVecSort + , setSort, bitVecSort, seqSort , sizedBitVecSort , mapSort, charSort , listFTyCon @@ -494,6 +494,10 @@ setSort = FApp (FTC setFTyCon) -- bitVec64Sort :: Sort -- bitVec64Sort = bitVecSort (FTC (symbolFTycon' size64Name)) +-- | Produces a `Seq a` from a given polymorphic identifier. +seqSort :: Int -> Sort +seqSort i = FApp (FTC $ symbolFTycon' seqName) (FVar i) + bitVecSort :: Int -> Sort bitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FVar i) diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs index c33681c4e..37820694c 100644 --- a/src/Language/Fixpoint/Types/Theories.hs +++ b/src/Language/Fixpoint/Types/Theories.hs @@ -230,6 +230,7 @@ data SmtSort | SString | SSet | SMap + | SSeq SmtSort | SBitVec !Int | SVar !Int | SData !FTycon ![SmtSort] @@ -240,12 +241,17 @@ instance Hashable SmtSort instance NFData SmtSort instance S.Store SmtSort + + -- | The 'poly' parameter is True when we are *declaring* sorts, -- and so we need to leave the top type variables be; it is False when -- we are declaring variables etc., and there, we serialize them -- using `Int` (though really, there SHOULD BE NO floating tyVars... -- 'smtSort True msg t' serializes a sort 't' using type variables, -- 'smtSort False msg t' serializes a sort 't' using 'Int' instead of tyvars. +-- +-- Perhaps we should change this to not use ints as a default, but a new sort? +-- (i.e. declare a new sort (declare-sort Default) for this use) sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort sortSmtSort poly env t = {- tracepp ("sortSmtSort: " ++ showpp t) else id) $ -} go . unAbs $ t where @@ -269,6 +275,8 @@ fappSmtSort poly m env = go -- HKT go t@(FVar _) ts = SApp (sortSmtSort poly env <$> (t:ts)) go (FTC c) _ | setConName == symbol c = SSet + go (FTC c) [s] + | seqName == symbol c = SSeq $ sortSmtSort poly env s go (FTC c) _ | mapConName == symbol c = SMap go (FTC bv) [FTC s] @@ -294,6 +302,7 @@ instance PPrint SmtSort where pprintTidy _ SString = text "Str" pprintTidy _ SSet = text "Set" pprintTidy _ SMap = text "Map" + pprintTidy k (SSeq a) = text "Seq" <+> pprintTidy k a pprintTidy _ (SBitVec n) = text "BitVec" <+> int n pprintTidy _ (SVar i) = text "@" <-> int i -- HKT pprintTidy k (SApp ts) = ppParens k (pprintTidy k tyAppName) ts diff --git a/src/Language/Fixpoint/Utils/Files.hs b/src/Language/Fixpoint/Utils/Files.hs index 49f3723cd..39d339a5f 100644 --- a/src/Language/Fixpoint/Utils/Files.hs +++ b/src/Language/Fixpoint/Utils/Files.hs @@ -89,6 +89,8 @@ data Ext = Cgi -- ^ Constraint Generation Information | PAss | Dat | BinFq -- ^ Binary representation of .fq / FInfo + | Prog -- ^ Program file (counter example generation) + | Cex !Int -- ^ Counterexample JSON file (for external explorer) | Smt2 -- ^ SMTLIB2 query file | HSmt2 -- ^ Horn query file | HJSON -- ^ Horn query JSON file @@ -123,6 +125,8 @@ extMap = go go Result = ".out" go Saved = ".bak" go Cache = ".err" + go (Cex n) = ".cex." <> show n <> ".json" + go Prog = ".prog" go Smt2 = ".smt2" go HSmt2 = ".horn.smt2" go HJSON = ".horn.json" diff --git a/tests/neg/NonLinear.fq b/tests/neg/NonLinear.fq index e341af830..68b95c477 100644 --- a/tests/neg/NonLinear.fq +++ b/tests/neg/NonLinear.fq @@ -1,4 +1,3 @@ - bind 1 pig : {v: int | []} bind 2 pigOut : {v: int | [v = pig + 1]} @@ -25,4 +24,3 @@ constraint: wf: env [10] reft {vk02: int | [$k0]} - diff --git a/tests/neg/ProgTest.fq b/tests/neg/ProgTest.fq new file mode 100644 index 000000000..44f1624d4 --- /dev/null +++ b/tests/neg/ProgTest.fq @@ -0,0 +1,24 @@ +wf: + env [] + reft {vk: int | [$k0]} + +bind 1 x : {v: int | $k0[vk := v]} +bind 2 y : {v: int | $k0[vk := v]} + +constraint: + env [1; 2] + lhs {v: int | v == x + y} + rhs {v: int | v != 7} + id 0 tag [] + +constraint: + env [] + lhs {v: int | v == 3} + rhs {v: int | $k0[vk := v]} + id 1 tag [] + +constraint: + env [] + lhs {v: int | v == 4} + rhs {v: int | $k0[vk := v]} + id 2 tag [] diff --git a/tests/neg/decl-order.fq b/tests/neg/decl-order.fq new file mode 100644 index 000000000..dcb5fdb50 --- /dev/null +++ b/tests/neg/decl-order.fq @@ -0,0 +1,22 @@ +bind 0 x : {v: int | $k[v2:=v][karg:=y]} +bind 1 y : {v: int | y == 0} + +constraint: + env [0; 1] + lhs {v0: int | v0 == x} + rhs {v0: int | v0 > 1} + id 0 tag [] + +bind 2 z : {v: int | true} + +constraint: + env [2] + lhs {v1: int | v1 > z} + rhs {v1: int | $k[v2:=v1][karg:=z]} + id 1 tag [] + +bind 10 karg : {v:int | true} + +wf: + env [10] + reft {v2 : int | $k} diff --git a/tests/neg/duplicate-names.fq b/tests/neg/duplicate-names.fq new file mode 100644 index 000000000..ffd037211 --- /dev/null +++ b/tests/neg/duplicate-names.fq @@ -0,0 +1,26 @@ +fixpoint "--counterexample" + +distinct True : (bool) +distinct False : (bool) + +bind 2 True : {v: bool | v} +bind 3 False : {v: bool | ~v} + +bind 0 dup : {v: int | $k} +bind 1 dup : {v: int | $k} + +constraint: + env [] + lhs {v : int | v = 0} + rhs {v : int | $k} + id 0 tag [] + +constraint: + env [0; 1; 2; 3] + lhs {v : int | v = dup} + rhs {v : int | v > 0} + id 1 tag [] + +wf: + env [] + reft {v : int | $k} diff --git a/tests/neg/duplicate-names2.fq b/tests/neg/duplicate-names2.fq new file mode 100644 index 000000000..99bb9a450 --- /dev/null +++ b/tests/neg/duplicate-names2.fq @@ -0,0 +1,32 @@ +fixpoint "--counterexample" + +bind 0 duplicator : {v: int | $k0 && $k1} + +bind 1 duplicated : {v: int | v == 0} +bind 2 duplicated : {v: int | v == 1} + +constraint: + env [1] + lhs {v : int | v == duplicated} + rhs {v : int | $k0} + id 0 tag [] + +constraint: + env [2] + lhs {v : int | v == duplicated} + rhs {v : int | $k1} + id 1 tag [] + +constraint: + env [0] + lhs {v : int | v = duplicator} + rhs {v : int | v > 0} + id 2 tag [] + +wf: + env [] + reft {v : int | $k0} + +wf: + env [] + reft {v : int | $k1} diff --git a/tests/neg/duplicate-names3.fq b/tests/neg/duplicate-names3.fq new file mode 100644 index 000000000..51fead988 --- /dev/null +++ b/tests/neg/duplicate-names3.fq @@ -0,0 +1,30 @@ +fixpoint "--counterexample" + +bind 0 x : {v: int | [$k[vk := v]]} +bind 1 y : {v: int | [$k[vk := v]]} + +constraint: + env [0; 1] + lhs {v0: int | v0 == x + y} + rhs {v0: int | v0 != 7} + id 0 tag [] + +bind 3 z : {v: int | v = 3} + +constraint: + env [3] + lhs {v1: int | [v1 == z]} + rhs {v1: int | $k[vk := v1]} + id 1 tag [] + +bind 4 z : {v: int | v = 4} + +constraint: + env [4] + lhs {v2: int | [v2 == z]} + rhs {v2: int | $k[vk := v2]} + id 2 tag [] + +wf: + env [] + reft {vk: int | [$k]} diff --git a/tests/neg/false.fq b/tests/neg/false.fq new file mode 100644 index 000000000..73306826b --- /dev/null +++ b/tests/neg/false.fq @@ -0,0 +1,7 @@ +fixpoint "--counterexample" + +constraint: + env [] + lhs {v : int | true} + rhs {v : int | false} + id 0 tag [] diff --git a/tests/neg/linear.fq b/tests/neg/linear.fq new file mode 100644 index 000000000..7c3ab53bf --- /dev/null +++ b/tests/neg/linear.fq @@ -0,0 +1,39 @@ +fixpoint "--counterexample" + +bind 0 x : {v : int | true} +bind 1 y : {v : int | true} +bind 2 y : {v : int | true} + +// constraint: +// env [0] +// lhs {v : int | x = 10} +// rhs {v : int | $k0[v:=x]} +// id 1 tag [] + +constraint: + env [1] + lhs {v : int | y <= v} + rhs {v : int | v >= 0} + id 1 tag [] + +constraint: + env [0;1] + lhs {v : int | true} + rhs {v : int | y <= x} + id 2 tag [] + +constraint: + env [0;2] + lhs {v : int | [v == y; y <= x] } + rhs {v : int | [v == y] } + id 3 tag [] + +// constraint: +// env [2] +// lhs {v : int | $k0[v:=z]} +// rhs {v : int | 10 <= z} +// id 3 tag [] + +// wf: +// env [ ] +// reft {v: int | $k0} diff --git a/tests/neg/list-len-define.fq b/tests/neg/list-len-define.fq new file mode 100644 index 000000000..1f6b56b9c --- /dev/null +++ b/tests/neg/list-len-define.fq @@ -0,0 +1,20 @@ +fixpoint "--counterexample" + +data Vec 1 = [ + | VNil { } + | VCons { head : @(0), tail : Vec @(0)} +] + +constant len: (func(1, [(Vec @(0)); int])) + +define len(l: Vec a) : int = { + if (is$VNil l) then 0 else (1 + len(tail l)) +} + +bind 0 xs : {v: Vec int | v = (VCons 2 VNil)} + +constraint: + env [0] + lhs {v : Vec int | len v == 3} + rhs {v : Vec int | v = xs} + id 1 tag [] diff --git a/tests/neg/obsolete-env.fq b/tests/neg/obsolete-env.fq new file mode 100644 index 000000000..3dcc4b19d --- /dev/null +++ b/tests/neg/obsolete-env.fq @@ -0,0 +1,12 @@ + +bind 0 x : {v: int | true} +bind 1 y : {v: int | v >= 0} +bind 2 unused0 : {v:int | v = 2} +bind 3 unused1 : {v:int | v = 3} +bind 4 unused2 : {v:int | v = 4} + +constraint: + env [0; 1; 2; 3; 4] + lhs {v: int | v == x + y} + rhs {v: int | v >= 0} + id 0 tag [] diff --git a/tests/neg/parse-types.fq b/tests/neg/parse-types.fq new file mode 100644 index 000000000..8a7dcd63f --- /dev/null +++ b/tests/neg/parse-types.fq @@ -0,0 +1,17 @@ +bind 0 x : {v: real | $k} + +constraint: + env [] + lhs {v : real | v = 0.0} + rhs {v : real | $k} + id 0 tag [] + +constraint: + env [0] + lhs {v : real | v = x} + rhs {v : real | v > 0.0} + id 1 tag [] + +wf: + env [] + reft {v : real | $k} diff --git a/tests/neg/sequence.fq b/tests/neg/sequence.fq new file mode 100644 index 000000000..2e2a4d115 --- /dev/null +++ b/tests/neg/sequence.fq @@ -0,0 +1,10 @@ +fixpoint "--counterexample" + +bind 0 xs : {v: Seq int | Seq$len v == 2} +bind 1 ys : {v: Seq int | Seq$len v == 2} + +constraint: + env [0;1] + lhs {v : Seq int | v == xs} + rhs {v : Seq int | v == ys} + id 0 tag [] diff --git a/tests/neg/two-calls.fq b/tests/neg/two-calls.fq new file mode 100644 index 000000000..2ba1e23d9 --- /dev/null +++ b/tests/neg/two-calls.fq @@ -0,0 +1,30 @@ +fixpoint "--counterexample" + +bind 0 x : {v: int | [$k[vk := v]]} +bind 1 y : {v: int | [$k[vk := v]]} + +constraint: + env [0; 1] + lhs {v0: int | v0 == x + y} + rhs {v0: int | v0 != 7} + id 0 tag [] + +bind 3 three : {v: int | v = 3} + +constraint: + env [3] + lhs {v1: int | [v1 == three]} + rhs {v1: int | $k[vk := v1]} + id 1 tag [] + +bind 4 four : {v: int | v = 4} + +constraint: + env [4] + lhs {v2: int | [v2 == four]} + rhs {v2: int | $k[vk := v2]} + id 2 tag [] + +wf: + env [] + reft {vk: int | [$k]} diff --git a/tests/pos/sequence.fq b/tests/pos/sequence.fq new file mode 100644 index 000000000..5e54bebb6 --- /dev/null +++ b/tests/pos/sequence.fq @@ -0,0 +1,7 @@ +bind 0 xs : {v: Seq int | xs == Seq$concat (Seq$unit 0) (Seq$unit 1)} + +constraint: + env [0] + lhs {v : Seq int | v == xs} + rhs {v : Seq int | Seq$len v == 2} + id 0 tag []