diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,14 @@ ## NEXT +## 0.9.6.3.3 (2025-03-22) + +- Add support for GHC HEAD (9.13) [#745](https://github.com/ucsd-progsys/liquid-fixpoint/pull/745). +- Expose SMTLIB define-fun to users of liquid-fixpoint [#744](https://github.com/ucsd-progsys/liquid-fixpoint/pull/744). +- Check that expressions in refinements are Bool-sorted [#743](https://github.com/ucsd-progsys/liquid-fixpoint/pull/743). +- Fix crashes when a datatype is declared with a `Map_t` field [#738](https://github.com/ucsd-progsys/liquid-fixpoint/issues/738). +- Simplify expressions in fqout files [#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741). + ## 0.9.6.3.2 (2025-03-06) - Expose relatedSymbols from EnvironmentReduction. Needed for improving error diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquid-fixpoint -version: 0.9.6.3.2 +version: 0.9.6.3.3 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint @@ -25,7 +25,7 @@ license: BSD-3-Clause license-file: LICENSE build-type: Simple -tested-with: GHC == 9.10.1, GHC == 9.8.2, GHC == 9.6.5 +tested-with: GHC == 9.12.2, GHC == 9.10.1, GHC == 9.8.2 extra-source-files: tests/neg/*.fq tests/pos/*.fq unix/Language/Fixpoint/Utils/*.hs diff --git a/src/Language/Fixpoint/Horn/Info.hs b/src/Language/Fixpoint/Horn/Info.hs --- a/src/Language/Fixpoint/Horn/Info.hs +++ b/src/Language/Fixpoint/Horn/Info.hs @@ -30,6 +30,7 @@ , F.ae = axEnv cfg q cs , F.ddecls = H.qData q , F.hoInfo = F.cfgHoInfo cfg + , F.defns = H.qDefs q } where be0 = F.emptyBindEnv diff --git a/src/Language/Fixpoint/Horn/Parse.hs b/src/Language/Fixpoint/Horn/Parse.hs --- a/src/Language/Fixpoint/Horn/Parse.hs +++ b/src/Language/Fixpoint/Horn/Parse.hs @@ -36,6 +36,7 @@ , H.qData = [ dd | HDat dd <- things ] , H.qOpts = [ o | HOpt o <- things ] , H.qNums = [ n | HNum n <- things ] + , H.qDefs = [] } -- | A @HThing@ describes the kinds of things we may see, in no particular order diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs --- a/src/Language/Fixpoint/Horn/SMTParse.hs +++ b/src/Language/Fixpoint/Horn/SMTParse.hs @@ -126,16 +126,17 @@ mkQuery :: [HThing a] -> H.Query a mkQuery things = H.Query - { H.qQuals = [ q | HQual q <- things ] - , H.qVars = [ k | HVar k <- things ] - , H.qCstr = H.CAnd [ c | HCstr c <- things ] - , H.qCon = M.fromList [ (x,t) | HCon x t <- things ] - , H.qDis = M.fromList [ (x,t) | HDis x t <- things ] - , H.qEqns = [ e | HDef e <- things ] - , H.qMats = [ m | HMat m <- things ] - , H.qData = [ dd | HDat dd <- things ] - , H.qOpts = [ o | HOpt o <- things ] - , H.qNums = [ s | HNum s <- things ] + { H.qQuals = [ q | HQual q <- things ] + , H.qVars = [ k | HVar k <- things ] + , H.qCstr = H.CAnd [ c | HCstr c <- things ] + , H.qCon = M.fromList [ (x,t) | HCon x t <- things ] + , H.qDis = M.fromList [ (x,t) | HDis x t <- things ] + , H.qEqns = [ e | HDef e <- things ] + , H.qDefs = [ e | HDfn e <- things ] + , H.qMats = [ m | HMat m <- things ] + , H.qData = [ dd | HDat dd <- things ] + , H.qOpts = [ o | HOpt o <- things ] + , H.qNums = [ s | HNum s <- things ] } -- | A @HThing@ describes the kinds of things we may see, in no particular order @@ -150,6 +151,7 @@ | HCon F.Symbol F.Sort | HDis F.Symbol F.Sort | HDef F.Equation + | HDfn F.Equation | HMat F.Rewrite | HDat !F.DataDecl | HOpt !String @@ -166,6 +168,7 @@ <|> HCon <$> (reserved "constant" *> symbolP) <*> sortP <|> HDis <$> (reserved "distinct" *> symbolP) <*> sortP <|> HDef <$> (reserved "define" *> defineP) + <|> HDfn <$> (reserved "define_fun" *> defineP) <|> HMat <$> (reserved "match" *> matchP) <|> HDat <$> (reserved "datatype" *> dataDeclP) <|> HNum <$> (reserved "numeric" *> numericDeclP) diff --git a/src/Language/Fixpoint/Horn/Solve.hs b/src/Language/Fixpoint/Horn/Solve.hs --- a/src/Language/Fixpoint/Horn/Solve.hs +++ b/src/Language/Fixpoint/Horn/Solve.hs @@ -34,9 +34,9 @@ q <- parseQuery baseCfg -- If you want to set --eliminate=none, you better make it a pragma - cfgElim <- if F.eliminate baseCfg == F.None - then pure (baseCfg { F.eliminate = F.Some }) - else pure baseCfg + let cfgElim = if F.eliminate baseCfg == F.None + then baseCfg { F.eliminate = F.Some } + else baseCfg cfgPragmas <- F.withPragmas cfgElim (H.qOpts q) diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -647,7 +647,8 @@ Nothing -> [] Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex] - argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols (F.solver cfg) []) `S.union`measures + argsAndPrims = args `S.union` S.fromList (fst <$> F.toListSEnv thySyms) `S.union`measures + thySyms = F.theorySymbols (F.solver cfg) isWellFormed :: F.Expr -> Bool isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims diff --git a/src/Language/Fixpoint/Horn/Types.hs b/src/Language/Fixpoint/Horn/Types.hs --- a/src/Language/Fixpoint/Horn/Types.hs +++ b/src/Language/Fixpoint/Horn/Types.hs @@ -196,9 +196,10 @@ { qQuals :: ![F.Qualifier] -- ^ qualifiers over which to solve cstrs , qVars :: ![Var a] -- ^ kvars, with parameter-sorts , qCstr :: !(Cstr a) -- ^ list of constraints - , qCon :: M.HashMap F.Symbol F.Sort -- ^ list of constants (uninterpreted functions) + , qCon :: M.HashMap F.Symbol F.Sort -- ^ list of constants (un/interpreted functions) , qDis :: M.HashMap F.Symbol F.Sort -- ^ list of *distinct* constants (uninterpreted functions) , qEqns :: ![F.Equation] -- ^ list of equations + , qDefs :: ![F.Equation] -- ^ list of equations to be sent to SMT as define-fun , qMats :: ![F.Rewrite] -- ^ list of match-es , qData :: ![F.DataDecl] -- ^ list of data-declarations , qOpts :: ![String] -- ^ list of fixpoint options @@ -340,7 +341,8 @@ , P.vcat (toHornSMT <$> qQuals q) , P.vcat (toHornSMT <$> qVars q) , P.vcat [toHornCon x t | (x, t) <- M.toList (qCon q)] - , P.vcat (toHornSMT <$> qEqns q) + , P.vcat (eqnToHornSMT "define" <$> qEqns q) + , P.vcat (eqnToHornSMT "define_fun" <$> qDefs q) , P.vcat (toHornSMT <$> qData q) , P.vcat (toHornSMT <$> qMats q) , P.parens (P.vcat ["constraint", P.nest 1 (toHornSMT (qCstr q))]) @@ -371,8 +373,9 @@ toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc toHornAnd f xs = P.parens (P.vcat ("and" : (P.nest 1 . f <$> xs))) -instance ToHornSMT F.Equation where - toHornSMT (F.Equ f xs e s _) = P.parens ("define" P.<+> F.pprint f P.<+> toHornSMT xs P.<+> toHornSMT s P.<+> toHornSMT e) +eqnToHornSMT :: P.Doc -> F.Equation -> P.Doc +eqnToHornSMT keyword (F.Equ f xs e s _) = P.parens (keyword P.<+> F.pprint f P.<+> toHornSMT xs P.<+> toHornSMT s P.<+> toHornSMT e) + instance ToHornSMT F.DataDecl where toHornSMT (F.DDecl tc n ctors) = diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs --- a/src/Language/Fixpoint/Parse.hs +++ b/src/Language/Fixpoint/Parse.hs @@ -1449,7 +1449,7 @@ <|> (reserved "False" >> return False) defsFInfo :: [Def a] -> FInfo a -defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae lrws +defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae lrws mempty where cm = Misc.safeFromList "defs-cm" [(cid c, c) | Cst c <- defs] diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs --- a/src/Language/Fixpoint/Smt/Interface.hs +++ b/src/Language/Fixpoint/Smt/Interface.hs @@ -7,6 +7,8 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DoAndIfThenElse #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use isNothing" #-} -- | This module contains an SMTLIB2 interface for -- 1. checking the validity, and, @@ -252,20 +254,19 @@ where smtFile = extFileName Smt2 f -makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context -makeContextWithSEnv cfg f env = do +makeContextWithSEnv :: Config -> FilePath -> SymEnv -> [Equation] -> IO Context +makeContextWithSEnv cfg f env defns = do ctx <- makeContext cfg f - let ctx' = ctx {ctxSymEnv = env} + let ctx' = ctx {ctxSymEnv = env, ctxDefines = defns} declare ctx' return ctx' - -- where msg = "makeContextWithSEnv" ++ show env makeContextNoLog :: Config -> IO Context -makeContextNoLog cfg - = do me <- makeContext' cfg Nothing - pre <- smtPreamble cfg (solver cfg) me - mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre - return me +makeContextNoLog cfg = do + me <- makeContext' cfg Nothing + pre <- smtPreamble cfg (solver cfg) me + mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre + return me makeProcess :: Maybe Handle @@ -302,11 +303,11 @@ Cvc4 -> makeProcess ctxLog $ Process.defaultConfig { Process.exe = "cvc4" - , Process.args = ["--incremental", "-L", "smtlib2"] } + , Process.args = ["-L", "smtlib2"] } Cvc5 -> makeProcess ctxLog $ Process.defaultConfig { Process.exe = "cvc5" - , Process.args = ["--incremental", "-L", "smtlib2"] } + , Process.args = ["-L", "smtlib2"] } solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend loud <- isLoud return Ctx { ctxSolver = solver @@ -315,6 +316,7 @@ , ctxLog = ctxLog , ctxVerbose = loud , ctxSymEnv = mempty + , ctxDefines = mempty } -- | Close file handles and release the solver backend's resources. @@ -331,7 +333,7 @@ | s == Z3 || s == Z3mem = do v <- getZ3Version me checkValidStringFlag Z3 v cfg - return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3 + return $ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3 | otherwise = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s) @@ -404,10 +406,13 @@ smtAssert :: Context -> Expr -> IO () smtAssert me p = interact' me (Assert Nothing p) +smtDefineEqn :: Context -> Equation -> IO () +smtDefineEqn me Equ {..} = smtDefineFunc me eqName eqArgs eqSort eqBody + smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO () smtDefineFunc me name symList rsort e = let env = seData (ctxSymEnv me) - in interact' me $ + in interact' me $ DefineFunc name (map (sortSmtSort False env <$>) symList) @@ -456,13 +461,7 @@ | gradual cfg = [""] | otherwise = ["\n(set-option :smt.mbqi false)"] -z3_options :: [Builder] -z3_options - = [ "(set-option :auto-config false)" - , "(set-option :model true)" ] - - -------------------------------------------------------------------------------- declare :: Context -> IO () -------------------------------------------------------------------------------- @@ -471,6 +470,7 @@ forM_ thyXTs $ uncurry $ smtDecl me forM_ qryXTs $ uncurry $ smtDecl me forM_ ats $ uncurry $ smtFuncDecl me + forM_ defs $ smtDefineEqn me forM_ ess $ smtDistinct me forM_ axs $ smtAssert me where @@ -479,12 +479,13 @@ lts = F.toListSEnv . F.seLits $ env ess = distinctLiterals lts axs = Thy.axiomLiterals lts - thyXTs = filter (isKind 1) xts - qryXTs = fmap tx <$> filter (isKind 2) xts - isKind n = (n ==) . symKind env . fst - xts = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env) + thyXTs = [ (x, t) | (x, t) <- xts, symKind env x == Just F.Uninterp ] + qryXTs = fmap tx <$> [ (x, t) | (x, t) <- xts, symKind env x == Nothing ] + -- isKind n = (n ==) . symKind env . fst + xts = symbolSorts (F.seSort env) tx = elaborate (ElabParam (ctxElabF me) "declare" env) ats = funcSortVars env + defs = ctxDefines me symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)] symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ] @@ -507,24 +508,8 @@ lamSort (s,t) = ([s, t], F.SInt) argSort (s,_) = ([] , s) --- | 'symKind' returns {0, 1, 2} where: --- 0 = Theory-Definition, --- 1 = Theory-Declaration, --- 2 = Query-Binder - -symKind :: F.SymEnv -> F.Symbol -> Int -symKind env x = case F.tsInterp <$> F.symEnvTheory x env of - Just F.Theory -> 0 - Just F.Ctor -> 0 - Just F.Test -> 0 - Just F.Field -> 0 - Just F.Uninterp -> 1 - Nothing -> 2 - -- Just t -> if tsInterp t then 0 else 1 - - --- assumes :: [F.Expr] -> SolveM () --- assumes es = withContext $ \me -> forM_ es $ smtAssert me +symKind :: F.SymEnv -> F.Symbol -> Maybe Sem +symKind env x = F.tsInterp <$> F.symEnvTheory x env -- | `distinctLiterals` is used solely to determine the set of literals -- (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT, diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs --- a/src/Language/Fixpoint/Smt/Theories.hs +++ b/src/Language/Fixpoint/Smt/Theories.hs @@ -8,6 +8,7 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE InstanceSigs #-} module Language.Fixpoint.Smt.Theories ( @@ -237,7 +238,7 @@ = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y") onlyLinearArith :: Config -> Bool -onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Cvc5] +onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Z3mem, Cvc5] preamble :: Config -> SMTSolver -> [Builder] preamble cfg s = snd <$> filter (matchesCondition s . fst) (solverPreamble cfg) @@ -249,8 +250,12 @@ solverPreamble :: Config -> [Preamble] solverPreamble cfg - = [(SOnly [Cvc4], "(set-logic ALL_SUPPORTED)")] - ++ [(SOnly [Cvc5], "(set-logic ALL)")] + = [ (SOnly [Z3, Z3mem], "(set-option :auto-config false)") + , (SOnly [Z3, Z3mem], "(set-option :model true)") + , (SOnly [Cvc4], "(set-logic ALL_SUPPORTED)") + , (SOnly [Cvc5], "(set-logic ALL)") + , (SOnly [Cvc4, Cvc5], "(set-option :incremental true)") + ] ++ boolPreamble cfg ++ arithPreamble cfg ++ stringPreamble cfg @@ -375,13 +380,22 @@ -- symbols, and `interpSEnv` is for interpreted symbols. -------------------------------------------------------------------------------- --- | `theorySymbols` contains the list of ALL SMT symbols with interpretations, --- i.e. which are given via `define-fun` (as opposed to `declare-fun`) -theorySymbols :: SMTSolver -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol -theorySymbols cfg ds = fromListSEnv $ -- SHIFTLAM uninterpSymbols - interpSymbols cfg - ++ concatMap dataDeclSymbols ds +instance TheorySymbols SMTSolver where + theorySymbols :: SMTSolver -> SEnv TheorySymbol + theorySymbols = fromListSEnv . interpSymbols +instance TheorySymbols [DataDecl] where + theorySymbols :: [DataDecl] -> SEnv TheorySymbol + theorySymbols = fromListSEnv . concatMap dataDeclSymbols + +instance TheorySymbols [Equation] where + theorySymbols = fromListSEnv . fmap equationSymbol + +equationSymbol :: Equation -> (Symbol, TheorySymbol) +equationSymbol eq = (sym, Thy sym (symbolRaw sym) sort Defined) + where + sym = eqName eq + sort = mkFFunc 0 ((snd <$> eqArgs eq) <> [eqSort eq]) -------------------------------------------------------------------------------- interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)] diff --git a/src/Language/Fixpoint/Smt/Types.hs b/src/Language/Fixpoint/Smt/Types.hs --- a/src/Language/Fixpoint/Smt/Types.hs +++ b/src/Language/Fixpoint/Smt/Types.hs @@ -102,6 +102,7 @@ , ctxLog :: !(Maybe Handle) , ctxVerbose :: !Bool , ctxSymEnv :: !SymEnv + , ctxDefines :: ![Equation] } -------------------------------------------------------------------------------- diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs --- a/src/Language/Fixpoint/Solver.hs +++ b/src/Language/Fixpoint/Solver.hs @@ -34,7 +34,7 @@ import System.Exit (ExitCode (..)) import System.Console.CmdArgs.Verbosity (whenNormal, whenLoud) import Text.PrettyPrint.HughesPJ (render) -import Control.Monad (when) +import Control.Monad (mplus, when) import Control.Exception (catch) import Language.Fixpoint.Solver.EnvironmentReduction (reduceEnvironments, simplifyBindings) @@ -59,7 +59,7 @@ import Language.Fixpoint.Solver.Instantiate (instantiate) import Control.DeepSeq import qualified Data.ByteString as B -import Data.Maybe (catMaybes) +import Data.Maybe (catMaybes, mapMaybe) --------------------------------------------------------------------------- -- | Solve an .fq file ---------------------------------------------------- @@ -271,7 +271,8 @@ solveNative' !cfg !fi0 = do si6 <- simplifyFInfo cfg fi0 - res <- {- SCC "Sol.solve" -} Sol.solve cfg $!! si6 + res0 <- {- SCC "Sol.solve" -} Sol.solve cfg $!! si6 + let res = simplifyResult res0 -- rnf soln `seq` donePhase Loud "Solve2" --let stat = resStatus res -- saveSolution cfg res @@ -305,8 +306,10 @@ , "Solution:" , showpp (resSolution res) ] ++ - ( if gradual cfg then ["", "", showpp (gresSolution res)] - else [] + ( if gradual cfg then + ["", "", showpp $ gresSolution res] + else + [] ) ++ [ "" , "" @@ -314,3 +317,106 @@ , "" , showpp (HashMap.map unElab $ resNonCutsSolution res) ] + +simplifyResult :: Result a -> Result a +simplifyResult res = + res + { resSolution = HashMap.map simplifyKVar (resSolution res) + , resNonCutsSolution = HashMap.map simplifyKVar (resNonCutsSolution res) + } + +-- | Simplifies existential expressions with unused or inconsequential bindings. +-- +-- For instance, in the following example, "x" is not used at all. +-- +-- > simplifyKVar "exists x y. y == z && y == C" == "exists y. y == z && y == C" +-- +-- And in the following example, @x@ is used but in a way that doesn't +-- contribute any useful knowledge. +-- +-- > simplifyKVar "exists x y. x == C && y == z && y == C" +-- > == +-- > "exists y. y == z && y == C" +-- +-- We require that relevant variables occur more than once, or that +-- they occur in some other place than as an argument to @==@. +-- +simplifyKVar :: Expr -> Expr +simplifyKVar (POr es) = POr $ map simplifyKVar es +simplifyKVar (PExist bs e@(PAnd es)) = + let fvs = L.group $ L.sort $ collectFreeVarOccurrences e + esv = map (isUniqueEq fvs) es + removed = mapMaybe fst esv + needed = map head fvs L.\\ removed + bs' = filter ((`elem` needed) . fst) bs + in + PExist bs' $ PAnd $ [ei | (Nothing, ei) <- esv] + where + -- | Determine if the expression is an equality that sets the value of + -- a variable that doesn't occur elsewhere. + -- + -- In @isUniqueEq fvs e@, @fvs@ contains the occurrences of the free + -- variables, so we can infer if there is more than one occurrence + -- of a given free variable, and @e@ is the equality to analyze. + -- + -- Yields @(Just v, e)@ if @v@ doesn't occur elsewhere, and @e@ has + -- the form @v == e'@. + isUniqueEq :: [[Symbol]] -> Expr -> (Maybe Symbol, Expr) + isUniqueEq fvs er = case unElab er of + PAtom brel e0 e1 + | isEqRel brel -> + let m = isVarToDrop fvs e0 `mplus` isVarToDrop fvs e1 + in (m, er) + _ -> + (Nothing, er) + + -- | Tells if the binary relation is an equality. + isEqRel Eq = True + isEqRel Ueq = True + isEqRel _ = False + + -- | @isVarToDrop fvs s@ yields @Just s@ if the variable @s@ doesn't occur + -- elsewhere according to @fvs@. + -- + -- > isVarToDrop fvs (cast_as_int s) == isVarToDrop fvs s + -- + isVarToDrop fvs (EApp (EVar "cast_as_int") ei) = isVarToDrop fvs ei + isVarToDrop fvs (EVar s) + | elem [s] fvs = Just s + isVarToDrop _fvs _ = Nothing + +simplifyKVar e = e + +-- | Produces the free variables of an expressions as many times as they occur. +-- +-- There are no guarantees on the order in which the variables are produced. For +-- instance, +-- +-- > collectFreeVarOccurrences "z (y x) (y x)" == ["z", "y", "x", "y", "x"] +-- +collectFreeVarOccurrences :: Expr -> [Symbol] +collectFreeVarOccurrences = go [] + where + go acc e0 = case e0 of + ESym _ -> acc + ECon _ -> acc + EVar v -> v : acc + PKVar _ (Su m) -> foldr (flip go) acc $ HashMap.elems m + PGrad _ (Su m) _ e -> foldr (flip go) acc $ e : HashMap.elems m + ENeg e -> go acc e + PNot p -> go acc p + ECst e _t -> go acc e + PAll _xts p -> go acc p + ELam (b, _) e -> go acc e L.\\ [b] + ECoerc _a _t e -> go acc e + PExist _xts p -> go acc p + ETApp e _s -> go acc e + ETAbs e _s -> go acc e + EApp g e -> go (go acc e) g + EBin _o e1 e2 -> go (go acc e2) e1 + PImp p1 p2 -> go (go acc p2) p1 + PIff p1 p2 -> go (go acc p2) p1 + PAtom _r e1 e2 -> go (go acc e2) e1 + EIte p e1 e2 -> go (go (go acc e2) e1) p + PAnd ps -> foldr (flip go) acc ps + POr ps -> foldr (flip go) acc ps diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs --- a/src/Language/Fixpoint/Solver/Extensionality.hs +++ b/src/Language/Fixpoint/Solver/Extensionality.hs @@ -214,6 +214,11 @@ DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0) , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1) ] +#elif MIN_TOOL_VERSION_ghc(9,13,0) + ct = DCtor (dummyLoc (symbol "GHC.Internal.Tuple.(,)")) [ + DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$1")) (FVar 0) + , DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$2")) (FVar 1) + ] #else ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [ DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0) diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs --- a/src/Language/Fixpoint/Solver/Instantiate.hs +++ b/src/Language/Fixpoint/Solver/Instantiate.hs @@ -82,7 +82,7 @@ , maybe True (i `L.elem`) subcIds ] let t = mkCTrie cs -- 1. BUILD the Trie res <- withProgress (1 + length cs) $ - withCtx cfg file sEnv (pleTrie t . instEnv cfg info cs) -- 2. TRAVERSE Trie to compute InstRes + withCtx cfg file sEnv (defns info) (pleTrie t . instEnv cfg info cs) -- 2. TRAVERSE Trie to compute InstRes return $ resSInfo cfg sEnv info res -- 3. STRENGTHEN SInfo using InstRes where file = srcFile cfg ++ ".evals" @@ -296,7 +296,7 @@ -- | "Old" GLOBAL PLE -------------------------------------------------------------------------------- instantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a) -instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env act +instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env (defns info) act where act ctx = forM cstrs $ \(i, c) -> ((i,srcSpan c),) . mytracepp ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs info) aenv i c @@ -800,9 +800,9 @@ -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a -withCtx cfg file env k = do - ctx <- SMT.makeContextWithSEnv cfg file env +withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a +withCtx cfg file env defns k = do + ctx <- SMT.makeContextWithSEnv cfg file env defns _ <- SMT.smtPush ctx res <- k ctx SMT.cleanupContext ctx diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -84,7 +84,7 @@ s0 ctx = SS ctx be (stats0 fi) act' = assumesAxioms (F.asserts fi) >> act release = cleanupContext - acquire = makeContextWithSEnv cfg file initEnv + acquire = makeContextWithSEnv cfg file initEnv (F.defns fi) initEnv = symbolEnv cfg fi be = F.bs fi file = C.srcFile cfg diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -80,7 +80,7 @@ (cm info) let t = mkCTrie (M.toList cs) -- 1. BUILD the Trie res <- withRESTSolver $ \solver -> withProgress (1 + M.size cs) $ - withCtx cfg file sEnv $ \ctx -> do + withCtx cfg file sEnv (defns fi') $ \ctx -> do env <- instEnv cfg info cs solver ctx pleTrie t env -- 2. TRAVERSE Trie to compute InstRes savePLEEqualities cfg info sEnv res @@ -107,6 +107,7 @@ where equalitiesPerConstraint (cid, c) = (cid, L.sort [ e | i <- elemsIBindEnv (senv c), Just e <- [M.lookup i res] ]) + elabParam = ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv renderConstraintRewrite (cid, eqs) = "constraint id" <+> text (show cid ++ ":") $+$ nest 2 @@ -114,7 +115,7 @@ map (toFix . unElab) $ Set.toList $ Set.fromList $ -- call elabExpr to try to bring equations that are missing -- some casts into a fully annotated form for comparison - map (elabExpr (ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv)) $ + map (elabExpr elabParam (Just boolSort)) $ concatMap conjuncts eqs ) $+$ "" @@ -1334,9 +1335,9 @@ -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a -withCtx cfg file env k = do - ctx <- SMT.makeContextWithSEnv cfg file env +withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a +withCtx cfg file env defns k = do + ctx <- SMT.makeContextWithSEnv cfg file env defns _ <- SMT.smtPush ctx res <- k ctx SMT.cleanupContext ctx diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs --- a/src/Language/Fixpoint/Solver/Sanitize.hs +++ b/src/Language/Fixpoint/Solver/Sanitize.hs @@ -34,12 +34,12 @@ import qualified Data.Text as T import Data.Maybe (isNothing, mapMaybe, fromMaybe) import Control.Monad ((>=>)) -import Text.PrettyPrint.HughesPJ +import Text.PrettyPrint.HughesPJ hiding ((<>)) type SanitizeM a = Either E.Error a -------------------------------------------------------------------------------- -sanitize :: Config -> F.SInfo a -> SanitizeM (F.SInfo a) +sanitize :: (Show a) => Config -> F.SInfo a -> SanitizeM (F.SInfo a) -------------------------------------------------------------------------------- sanitize cfg = banIrregularData >=> Misc.fM dropFuncSortedShadowedBinders @@ -152,14 +152,20 @@ splitApp (fvar, arg:args) fapp' e = pure (e, []) - theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols (Cfg.solver cfg) $ F.ddecls si + thySyms = theoryEnv cfg si splitApp (e, es) - | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App theorySymbols $ stripCasts e + | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App thySyms (stripCasts e) = pure (e,es) | otherwise = Nothing +theoryEnv :: Config -> F.GInfo c a -> F.SEnv F.TheorySymbol +theoryEnv cfg si + = Thy.theorySymbols (Cfg.solver cfg) + <> Thy.theorySymbols (F.defns si) + <> Thy.theorySymbols (F.ddecls si) + -------------------------------------------------------------------------------- -- | See issue liquid-fixpoint issue #230. This checks that whenever we have, -- G1 |- K.su1 @@ -317,8 +323,9 @@ known cfg fi = \x -> F.memberSEnv x lits || F.memberSEnv x prims where lits = F.gLits fi - prims = Thy.theorySymbols (Cfg.solver cfg) . F.ddecls $ fi + prims = theoryEnv cfg fi + cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol] cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv) where @@ -387,15 +394,15 @@ -- it makes it hard to actually find the fundefs within (breaking PLE.) -------------------------------------------------------------------------------- symbolEnv :: Config -> F.SInfo a -> F.SymEnv -symbolEnv cfg si = F.symEnv sEnv tEnv ds lits (ts ++ ts') +symbolEnv cfg si = F.symEnv sEnv thyEnv ds lits (ts ++ ts') where ts' = applySorts ae' ae' = elaborate (ElabParam ef (F.atLoc E.dummySpan "symbolEnv") env0) (F.ae si) - env0 = F.symEnv sEnv tEnv ds lits ts - tEnv = Thy.theorySymbols slv ds + env0 = F.symEnv sEnv thyEnv ds lits ts + thyEnv = theoryEnv cfg si ds = F.ddecls si ts = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv]) - sEnv = F.coerceSortEnv ef $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts + sEnv = F.coerceSortEnv ef $ (F.tsSort <$> thyEnv) `mappend` F.fromListSEnv xts slv = Cfg.solver cfg ef = solverFlags slv xts = symbolSorts cfg si ++ alits @@ -488,7 +495,6 @@ ws' = deleteWfCBinds drops <$> F.ws si (_,drops) = filterBindEnv keepF $ F.bs si keepF = conjKF [nonConstantF si, nonFunctionF si, _nonDerivedLH] - -- drops = F.tracepp "sanitizeWfC: dropping" $ L.sort drops' conjKF :: [KeepBindF] -> KeepBindF conjKF fs x t = and [f x t | f <- fs] diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs --- a/src/Language/Fixpoint/SortCheck.hs +++ b/src/Language/Fixpoint/SortCheck.hs @@ -141,6 +141,7 @@ { F.cm = elaborate ep <$> F.cm si , F.bs = elaborate ep $ F.bs si , F.asserts = elaborate ep <$> F.asserts si + , F.ddecls = coerceDataDecl (epFlags ep) <$> F.ddecls si } @@ -178,13 +179,16 @@ ep' = ep { epEnv = insertsSymEnv (epEnv ep) (eqArgs eq) } instance Elaborate Expr where - elaborate (ElabParam ef msg env) = - elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) + elaborate p e = elaborateExpr p e Nothing + +elaborateExpr :: ElabParam -> Expr -> Maybe Sort -> Expr +elaborateExpr (ElabParam ef msg env) e t = + elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') t . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e where env' = coerceEnv ef env skipElabExpr :: ElabParam -> Expr -> Expr -skipElabExpr ep e = case elabExprE ep e of +skipElabExpr ep e = case elabExprE ep Nothing e of Left _ -> e Right e' -> elabNumeric . elabApply (epEnv ep) $ e' @@ -211,7 +215,7 @@ instance Elaborate SortedReft where elaborate ep (RR s (Reft (v, e))) = RR s (Reft (v, e')) where - e' = elaborate ep' e + e' = elaborateExpr ep' e (Just boolSort) -- check that a SortedReft is in fact a bool ep' = ep { epEnv = insertSymEnv v s (epEnv ep) } instance (Loc a) => Elaborate (BindEnv a) where @@ -307,21 +311,28 @@ -------------------------------------------------------------------------------- -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites. -------------------------------------------------------------------------------- -elabExpr :: ElabParam -> Expr -> Expr -elabExpr ep e = case elabExprE ep e of +elabExpr :: ElabParam -> Maybe Sort -> Expr -> Expr +elabExpr ep t e = case elabExprE ep t e of Left ex -> die ex Right e' -> F.notracepp ("elabExp " ++ showpp e) e' -elabExprE :: ElabParam -> Expr -> Either Error Expr -elabExprE (ElabParam ef msg env) e = +validateSort :: Sort -> Maybe Sort -> CheckM () +validateSort t (Just t') + | t == t' = return () + | otherwise = throwErrorAt $ printf "unexpected sort: got `%s` but expected `%s`" (showpp t) (showpp t') +validateSort _ Nothing = return () + +elabExprE :: ElabParam -> Maybe Sort -> Expr -> Either Error Expr +elabExprE (ElabParam ef msg env) t e = case runCM0 (srcSpan msg) (Just ef) $ do - (!e', _) <- elab (env, envLookup) e + (!e', eSort) <- elab (env, envLookup) e + validateSort eSort t finalThetaRef <- asks chTVSubst finalTheta <- liftIO $ readIORef finalThetaRef return (applyExpr finalTheta e') of Left (ChError f') -> let e' = f' () - in Left $ err (srcSpan e') (d (val e')) + in Left $ err (srcSpan e') (d (val e')) Right s -> Right s where sEnv = seSort env @@ -334,6 +345,7 @@ , nest 4 (pprint $ subEnv sEnv e) ] + -------------------------------------------------------------------------------- -- | 'elabApply' replaces all direct function calls indirect calls via `apply` -------------------------------------------------------------------------------- @@ -431,9 +443,6 @@ -------------------------------------------------------------------------------- mkSearchEnv env x = lookupSEnvWithDistance x env --- withError :: CheckM a -> ChError -> CheckM a --- act `withError` e' = act `catchError` (\e -> throwError (atLoc e (val e ++ "\n because\n" ++ val e'))) - withError :: HasCallStack => CheckM a -> String -> CheckM a act `withError` msg = do r <- ask @@ -730,7 +739,6 @@ isUndef s = case bkAbs s of (is, FVar j) -> j `elem` is _ -> False - elabAddEnv :: Eq a => (t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b) elabAddEnv (g, f) bs = (g, addEnv f bs) diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs --- a/src/Language/Fixpoint/Types/Constraints.hs +++ b/src/Language/Fixpoint/Types/Constraints.hs @@ -697,7 +697,8 @@ , ae = axe , ddecls = adts , ebinds = ebs - , lrws = mempty + , lrws = mempty + , defns = mempty } where --TODO handle duplicates gracefully instead (merge envs by intersect?) @@ -744,6 +745,7 @@ , asserts :: ![Triggered Expr] -- ^ TODO: what is this? , ae :: AxiomEnv -- ^ Information about reflected function defs , lrws :: LocalRewritesEnv -- ^ Local rewrites + , defns :: ![Equation] -- ^ `define_fun` definitions to be passed to SMT } deriving (Eq, Show, Functor, Generic) @@ -773,6 +775,7 @@ , asserts = asserts i1 <> asserts i2 , ae = ae i1 <> ae i2 , lrws = lrws i1 <> lrws i2 + , defns = defns i1 <> defns i2 } @@ -791,6 +794,7 @@ , asserts = mempty , ae = mempty , lrws = mempty + , defns = mempty } instance PTable (SInfo a) where @@ -1073,7 +1077,7 @@ instance Fixpoint LocalRewritesEnv where toFix (LocalRewritesMap rws) = vcat $ uncurry toFixLocal <$> M.toList rws where - toFixLocal bid (LocalRewrites rws) = text "defineLocal" <+> toFix bid + toFixLocal bid (LocalRewrites rws) = text "defineLocal" <+> toFix bid <+> brackets (vcat $ punctuate ";" $ uncurry toFixRewrite <$> M.toList rws) toFixRewrite sym eq = toFix sym <+> text ":=" <+> toFix eq diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs --- a/src/Language/Fixpoint/Types/Sorts.hs +++ b/src/Language/Fixpoint/Types/Sorts.hs @@ -87,6 +87,7 @@ -- * Sort coercion for SMT theory encoding , coerceMapToArray , coerceSetBagToArray + , coerceDataDecl ) where import qualified Data.Store as S @@ -104,6 +105,7 @@ #endif import Control.DeepSeq import Data.Maybe (fromMaybe) +import Language.Fixpoint.Types.Config (ElabFlags, elabSetBag) import Language.Fixpoint.Types.Names import Language.Fixpoint.Types.PrettyPrint import Language.Fixpoint.Types.Spans @@ -706,3 +708,12 @@ | isBag sf = arraySort (coerceSetBagToArray sa) intSort | otherwise = FApp (coerceSetBagToArray sf) (coerceSetBagToArray sa) coerceSetBagToArray s = s + +coerceDataField :: ElabFlags -> DataField -> DataField +coerceDataField ef (DField x t) = DField x (((if elabSetBag ef then coerceSetBagToArray else id) . coerceMapToArray) t) + +coerceDataCtor :: ElabFlags -> DataCtor -> DataCtor +coerceDataCtor ef (DCtor x flds) = DCtor x (coerceDataField ef <$> flds) + +coerceDataDecl :: ElabFlags -> DataDecl -> DataDecl +coerceDataDecl ef (DDecl tc n ctors) = DDecl tc n (coerceDataCtor ef <$> ctors) diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs --- a/src/Language/Fixpoint/Types/Theories.hs +++ b/src/Language/Fixpoint/Types/Theories.hs @@ -37,6 +37,7 @@ -- * Coercing sorts in environments , coerceEnv , coerceSortEnv + , TheorySymbols(..) ) where @@ -250,6 +251,10 @@ } deriving (Eq, Ord, Show, Data, Typeable, Generic) + +class TheorySymbols a where + theorySymbols :: a -> SEnv TheorySymbol + instance NFData Sem instance NFData TheorySymbol instance S.Store TheorySymbol @@ -273,6 +278,7 @@ | Test -- ^ for ADT tests : `is$cons` | Field -- ^ for ADT field: `hd`, `tl` | Theory -- ^ for theory ops: mem, cup, select + | Defined -- ^ for user-defined `define-fun` deriving (Eq, Ord, Show, Data, Typeable, Generic) instance S.Store Sem