Skip to content

Commit

Permalink
perform proper encoding of (Smt2 Symbol)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ranjitjhala
ranjitjhala committed Oct 2, 2015
1 parent 247441d commit a1818aa
Show file tree
Hide file tree
Showing 8 changed files with 7,455 additions and 89 deletions.
147 changes: 147 additions & 0 deletions TODO.md
View file
@@ -1 +1,148 @@
# TODO

lits = [Prop : func(0, [GHC.Types.Bool; bool]);
x_Tuple64 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(3)]);
x_Tuple54 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(3)]);
x_Tuple41 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(0)]);
autolen : func(1, [@(0); int]);
addrLen : func(0, [int; int]);
x_Tuple65 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(4)]);
strLen : func(0, [int; int]);
fix#GHC.Types.#58##35#64 : func(1, [@(0); [@(0)]; [@(0)]]);
x_Tuple52 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(1)]);
x_Tuple44 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(3)]);
xListSelector : func(1, [[@(0)]; @(0)]);
x_Tuple33 : func(3, [(Tuple @(0) @(1) @(2)); @(2)]);
fst : func(2, [(Tuple @(0) @(1)); @(0)]);
x_Tuple76 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(5)]);
x_Tuple31 : func(3, [(Tuple @(0) @(1) @(2)); @(0)]);
x_Tuple43 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(2)]);
papp4 : func(8, [(Pred @(0) @(1) @(2) @(6));
@(3);
@(4);
@(5);
@(7);
bool]);
papp2 : func(4, [(Pred @(0) @(1)); @(2); @(3); bool]);
x_Tuple32 : func(3, [(Tuple @(0) @(1) @(2)); @(1)]);
x_Tuple63 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(2)]);
x_Tuple75 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(4)]);
x_Tuple51 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(0)]);
len : func(2, [(@(0) @(1)); int]);
xsListSelector : func(1, [[@(0)]; [@(0)]]);
null : func(1, [[@(0)]; bool]);
x_Tuple53 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(2)]);
x_Tuple22 : func(2, [(Tuple @(0) @(1)); @(1)]);
fromJust : func(1, [(GHC.Base.Maybe @(0)); @(0)]);
snd : func(2, [(Tuple @(0) @(1)); @(1)]);
x_Tuple73 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(2)]);
fix#lit#35#tests#47#pos#47#scanr.hs#58#7#58#29#45#53#124#qs#64##40#q#32##58##32#_#41# : Str;
x_Tuple62 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(1)]);
x_Tuple55 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(4)]);
papp3 : func(6, [(Pred @(0) @(1) @(2));
@(3);
@(4);
@(5);
bool]);
fix#GHC.Tuple.#40##44##41##35#74 : func(2, [@(0);
@(1);
(Tuple @(0) @(1))]);
cmp : func(0, [GHC.Types.Ordering; GHC.Types.Ordering]);
papp1 : func(1, [(Pred @(0)); @(0); bool]);
fix#GHC.Types.#91##93##35#6m : func(1, [[@(0)]]);
isJust : func(1, [(GHC.Base.Maybe @(0)); bool]);
x_Tuple42 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(1)]);
x_Tuple72 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(1)]);
x_Tuple21 : func(2, [(Tuple @(0) @(1)); @(0)]);
x_Tuple61 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(0)]);
x_Tuple74 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(3)]);
x_Tuple66 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(5)]);
x_Tuple71 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(0)]);
x_Tuple77 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(6)])]
,

lits' = [Prop : func(0, [GHC.Types.Bool; bool]);
x_Tuple64 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(3)]);
x_Tuple54 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(3)]);
fix#GHC.Types.#91##93##35#6m : func(1, [[@(0)]]);
x_Tuple41 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(0)]);
autolen : func(1, [@(0); int]);
addrLen : func(0, [int; int]);
x_Tuple65 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(4)]);
strLen : func(0, [int; int]);
x_Tuple52 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(1)]);
x_Tuple44 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(3)]);
xListSelector : func(1, [[@(0)]; @(0)]);
fix#lit#35#tests#47#pos#47#scanr.hs#58#7#58#29#45#53#124#qs#64##40#q#32##58##32#_#41# : Str;
x_Tuple33 : func(3, [(Tuple @(0) @(1) @(2)); @(2)]);
fst : func(2, [(Tuple @(0) @(1)); @(0)]);
x_Tuple76 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(5)]);
x_Tuple31 : func(3, [(Tuple @(0) @(1) @(2)); @(0)]);
x_Tuple43 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(2)]);
papp4 : func(8, [(Pred @(0) @(1) @(2) @(6));
@(3);
@(4);
@(5);
@(7);
bool]);
papp2 : func(4, [(Pred @(0) @(1)); @(2); @(3); bool]);
x_Tuple32 : func(3, [(Tuple @(0) @(1) @(2)); @(1)]);
x_Tuple63 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(2)]);
x_Tuple75 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(4)]);
x_Tuple51 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(0)]);
len : func(2, [(@(0) @(1)); int]);
xsListSelector : func(1, [[@(0)]; [@(0)]]);
null : func(1, [[@(0)]; bool]);
x_Tuple53 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(2)]);
x_Tuple22 : func(2, [(Tuple @(0) @(1)); @(1)]);
fromJust : func(1, [(GHC.Base.Maybe @(0)); @(0)]);
fix#GHC.Tuple.#40##44##41##35#74 : func(2, [@(0);
@(1);
(Tuple @(0) @(1))]);
snd : func(2, [(Tuple @(0) @(1)); @(1)]);
x_Tuple73 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(2)]);
x_Tuple62 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(1)]);
x_Tuple55 : func(5, [(Tuple @(0) @(1) @(2) @(3) @(4)); @(4)]);
papp3 : func(6, [(Pred @(0) @(1) @(2));
@(3);
@(4);
@(5);
bool]);
cmp : func(0, [GHC.Types.Ordering; GHC.Types.Ordering]);
papp1 : func(1, [(Pred @(0)); @(0); bool]);
isJust : func(1, [(GHC.Base.Maybe @(0)); bool]);
x_Tuple42 : func(4, [(Tuple @(0) @(1) @(2) @(3)); @(1)]);
x_Tuple72 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(1)]);
x_Tuple21 : func(2, [(Tuple @(0) @(1)); @(0)]);
x_Tuple61 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(0)]);
x_Tuple74 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(3)]);
x_Tuple66 : func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(5)]);
x_Tuple71 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(0)]);
x_Tuple77 : func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(6)]);
fix#GHC.Types.#58##35#64 : func(1, [@(0); [@(0)]; [@(0)]])]
54 changes: 40 additions & 14 deletions src/Language/Fixpoint/Interface.hs
View file
Expand Up @@ -71,7 +71,7 @@ solve :: (Fixpoint a) => Config -> FInfo a -> IO (Result a)
solve cfg
| parts cfg = partition cfg
| stats cfg = statistics cfg
| native cfg = solveNativeWithFInfo cfg
| native cfg = {-# SCC "solveNative" #-} solveNativeWithFInfo cfg
| multicore cfg = solvePar cfg
| otherwise = solveExt cfg

Expand All @@ -82,42 +82,68 @@ solveWith :: Config -> (FInfo () -> IO (Result ())) -> IO ExitCode
solveWith cfg s = exit (ExitFailure 2) $ do
let file = inFile cfg
str <- readFile file
let fi = rr' file str :: FInfo ()
let fi = {-# SCC "parsefq" #-} rr' file str :: FInfo ()
let fi' = fi { fileName = file }
res <- s fi'
return $ resultExit (resStatus res)

-- DEBUG debugDiff :: FInfo a -> FInfo b -> IO ()
-- DEBUG debugDiff fi fi' = putStrLn msg
-- DEBUG where
-- DEBUG {- msg = printf "\nDEBUG: diff = %s, cs = %s, ws = %s, bs = %s, \n lits = %s \n, \n lits' = %s"
-- DEBUG (show $ ufi == ufi')
-- DEBUG (show $ cm ufi == cm ufi')
-- DEBUG (show $ ws ufi == ws ufi')
-- DEBUG (show $ bs ufi == bs ufi')
-- DEBUG -- (show $ lits ufi == lits ufi')
-- DEBUG (show $ lits ufi)
-- DEBUG (show $ lits ufi') -}
-- DEBUG
-- DEBUG msg = printf "\nquals = %s\n\n\nquals' = %s"
-- DEBUG (show $ sort $ quals fi)
-- DEBUG (show $ sort $ quals fi')
-- DEBUG
-- DEBUG (ufi, ufi') = (fu <$> fi , fu <$> fi')
-- DEBUG fu = const ()
-- DEBUG (ncs, ncs') = (cLength fi , cLength fi')
-- DEBUG (nws, nws') = (wLength fi , wLength fi')
-- DEBUG (nbs, nbs') = (beLength fi , beLength fi')
-- DEBUG (nls, nls') = (litLength fi , litLength fi')
-- DEBUG (nqs, nqs') = (qLength fi , qLength fi')
-- DEBUG cLength = M.size . cm
-- DEBUG wLength = length . ws
-- DEBUG beLength = length . bindEnvToList . bs
-- DEBUG litLength = length . toListSEnv . lits
-- DEBUG qLength = length . quals

solveNativeWithFInfo :: (Fixpoint a) => Config -> FInfo a -> IO (Result a)
solveNativeWithFInfo cfg fi = do
writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)
donePhase Loud "Read Constraints"
--FIXME: inefficient since toFixpoint and rr are mostly inverses - better to
-- replace this by the net effect of rr . toFixpoint,
-- and the correct solution is to make toFixpoint and rr actually inverses.
let fi' = rr $ render $ toFixpoint cfg fi :: FInfo ()
let si = convertFormat fi'
let fi' = fi
let si = {-# SCC "convertFormat" #-} convertFormat fi'
writeLoud $ "fq file after format convert: \n" ++ render (toFixpoint cfg si)
donePhase Loud "Format Conversion"
let Right si' = validate cfg si
let Right si' = {-# SCC "validate" #-} validate cfg si
writeLoud $ "fq file after validate: \n" ++ render (toFixpoint cfg si')
donePhase Loud "Validated Constraints"
when (elimStats cfg) $ printElimStats (deps si')
let si'' = renameAll si'
let si'' = {-# SCC "renameAll" #-} renameAll si'
writeLoud $ "fq file after uniqify: \n" ++ render (toFixpoint cfg si'')
donePhase Loud "Uniqify"
si''' <- elim cfg si''
Result stat soln <- S.solve cfg si'''
si''' <- {-# SCC "elim" #-} elim cfg si''
Result stat soln <- {-# SCC "S.solve" #-} S.solve cfg si'''
donePhase Loud "Solve"
let stat' = sid <$> stat
putStrLn $ "Solution:\n" ++ showpp soln
-- render (pprintKVs $ hashMapToAscList soln) -- showpp soln
colorStrLn (colorResult stat') (show stat')
return $ Result (WrapC . (\i -> mlookup (cm fi) (mfromJust "WAT" i)) <$> stat') soln
return $ Result (WrapC . mlookup (cm fi) . mfromJust "WAT" <$> stat') soln

printElimStats :: Deps -> IO ()
printElimStats d = do
let postElims = length $ depCuts d
let total = postElims + (length $ depNonCuts d)
let total = postElims + length (depNonCuts d)
putStrLn $ "TOTAL KVars: " ++ show total
++ "\nPOST-ELIMINATION KVars: " ++ show postElims

Expand Down Expand Up @@ -169,7 +195,7 @@ solveFile cfg
where
fixCommand fp z3 verbosity
= printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s %s"
z3 fp verbosity rf newcheckf (command cfg)
z3 fp verbosity rf newcheckf (command cfg)
where
rf = if real cfg then realFlags else ""
newcheckf = if newcheck cfg then "-newcheck" else ""
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Fixpoint/Names.hs
View file
Expand Up @@ -229,7 +229,7 @@ isNontrivialVV = not . (vv Nothing ==)

dummySymbol = dummyName

intSymbol :: (Show a) => Symbol -> a -> Symbol
intSymbol :: (Show a) => Symbol -> a -> Symbol
intSymbol x i = x `mappend` symbol ('_' : show i)

tempSymbol, existSymbol :: Symbol -> Integer -> Symbol
Expand Down Expand Up @@ -282,7 +282,7 @@ propConName = "Prop"
hpropConName = "HProp"
strConName = "Str"
vvName = "VV"
symSepName = '#'
symSepName = '_'

nilName = "nil" :: Symbol
consName = "cons" :: Symbol
Expand Down
4 changes: 3 additions & 1 deletion src/Language/Fixpoint/Smt/Interface.hs
View file
Expand Up @@ -152,12 +152,14 @@ negativeP
{-@ pairs :: {v:[a] | (len v) mod 2 = 0} -> [(a,a)] @-}
pairs :: [a] -> [(a,a)]
pairs !xs = case L.splitAt 2 xs of
([],b) -> []
([],_) -> []
([x,y], zs) -> (x,y) : pairs zs

smtWriteRaw :: Context -> LT.Text -> IO ()
smtWriteRaw me !s = {-# SCC "smtWriteRaw" #-} do
hPutStrLnNow (cOut me) s
LTIO.appendFile "DEBUG.smt2" s
LTIO.appendFile "DEBUG.smt2" "\n"
maybe (return ()) (`hPutStrLnNow` s) (cLog me)

smtReadRaw :: Context -> IO Raw
Expand Down
18 changes: 10 additions & 8 deletions src/Language/Fixpoint/Smt/Serialize.hs
View file
Expand Up @@ -12,6 +12,7 @@ module Language.Fixpoint.Smt.Serialize where

import Control.Applicative ((<$>))
import Language.Fixpoint.Types
import Language.Fixpoint.Names
import Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy
import qualified Data.Text as T
Expand Down Expand Up @@ -53,15 +54,16 @@ instance SMTLIB2 Sort where
instance SMTLIB2 Symbol where
smt2 s
| Just t <- Thy.smt2Symbol s = LT.fromStrict t
smt2 s = LT.fromStrict . encode . symbolText $ s
smt2 s = LT.fromStrict . T.pack . encode . T.unpack . symbolText $ s

-- FIXME: this is probably too slow
encode :: T.Text -> T.Text
encode t = {-# SCC "encode" #-}
foldr (uncurry T.replace) t [("[", "ZM"), ("]", "ZN"), (":", "ZC")
,("(", "ZL"), (")", "ZR"), (",", "ZT")
,("|", "zb"), ("#", "zh"), ("\\","zr")
,("z", "zz"), ("Z", "ZZ"), ("%","zv")]

-- encode :: T.Text -> T.Text
-- encode t = {-# SCC "encode" #-}
-- foldr (uncurry T.replace) t [("[", "ZM"), ("]", "ZN"), (":", "ZC")
-- ,("(", "ZL"), (")", "ZR"), (",", "ZT")
-- ,("|", "zb"), ("#", "zh"), ("\\","zr")
-- ,("z", "zz"), ("Z", "ZZ"), ("%","zv")]

instance SMTLIB2 SymConst where
-- smt2 (SL s) = LT.fromStrict s
Expand Down Expand Up @@ -93,7 +95,7 @@ instance SMTLIB2 Brel where
smt2 _ = error "SMTLIB2 Brel"

instance SMTLIB2 Expr where
smt2 (ESym z) = smt2 z
smt2 (ESym z) = smt2 (symbol z)
smt2 (ECon c) = smt2 c
smt2 (EVar x) = smt2 x
-- smt2 (ELit x _) = smt2 x
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Fixpoint/Solver/Solution.hs
View file
Expand Up @@ -104,7 +104,7 @@ update1 s (k, qs) = (change, M.insert k qs s)
--------------------------------------------------------------------
init :: Config -> F.GInfo c a -> Solution
--------------------------------------------------------------------
init _ fi = tracepp "init solution" s
init _ fi = {- tracepp "init solution" -} s
where
s = L.foldl' (refine fi qs) s0 ws
s0 = M.empty
Expand Down Expand Up @@ -196,7 +196,7 @@ okInst env v t eq = isNothing tc
where
sr = F.RR t (F.Reft (v, F.Refa p))
p = eqPred eq
tc = tracepp msg $ So.checkSortedReftFull env sr
tc = {- tracepp msg $ -} So.checkSortedReftFull env sr
msg = "okInst [p := " ++ show p ++ " ]"

---------------------------------------------------------------------
Expand Down

0 comments on commit a1818aa

Please sign in to comment.