g2-0.2.0.0: src/G2/Language/Approximation.hs
module G2.Language.Approximation ( GenerateLemma
, Lookup
, MRCont
, moreRestrictive
, moreRestrictive'
, moreRestrictivePC
, applySolver
, inlineEquiv) where
import G2.Execution.NormalForms
import G2.Language.Expr
import qualified G2.Language.ExprEnv as E
import G2.Language.Naming
import qualified G2.Language.PathConds as P
import G2.Language.Support
import G2.Language.Syntax
import G2.Language.Typing as T
import qualified G2.Solver as S
import Control.Monad.Extra
import Control.Monad.IO.Class
import qualified Data.HashSet as HS
import qualified Data.HashMap.Lazy as HM
type GenerateLemma t l = State t -> State t -> (HM.HashMap Id Expr, HS.HashSet (Expr, Expr)) -> Expr -> Expr -> l
type Lookup t = Name -> State t -> Maybe E.ConcOrSym
type MRCont t l = State t
-> State t
-> HS.HashSet Name
-> (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
-> Bool -- ^ indicates whether this is part of the "active expression"
-> [(Name, Expr)] -- ^ variables inlined previously on the LHS
-> [(Name, Expr)] -- ^ variables inlined previously on the RHS
-> Expr
-> Expr
-> Either [l] (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
-------------------------------------------------------------------------------
-- [Inlining]
-- We keep two separate lists of variables that have been inlined previously on
-- the LHS and RHS. This means that inlinings on one side do not block any inlinings
-- that need to happen on the other side.
--
-- Whenever a variable is inlined, we record the expression that was on the
-- opposite side at the time. Not allowing a variable to be inlined at all on one
-- side in any sub-expressions that resulted from an inlining of it is too restrictive
-- in practice. We allow repeated inlinings of a variable as long as the expression on
-- the opposite side is not the same as it was when a previous inlining of the
-- same variable happened.
-------------------------------------------------------------------------------
-- | Check is s1 is an approximation of s2 (if s2 is more restrictive than s1.)
moreRestrictive :: MRCont t l -- ^ For special case handling - what to do if we don't match elsewhere in moreRestrictive
-> GenerateLemma t l
-> Lookup t -- ^ How to lookup variable names
-> State t -- ^ s1
-> State t -- ^ s2
-> HS.HashSet Name -- ^ Names that should not be inlined (often: top level names from the original source code)
-> (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
-> Either [l] (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
moreRestrictive mr_cont gen_lemma lkp s1 s2 ns hm =
moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm True [] [] (getExpr s1) (getExpr s2)
moreRestrictive' :: MRCont t l -- ^ For special case handling - what to do if we don't match elsewhere in moreRestrictive'
-> GenerateLemma t l
-> Lookup t
-> State t
-> State t
-> HS.HashSet Name -- ^ Names that should not be inlined (often: top level names from the original source code)
-> (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
-> Bool -- ^ indicates whether this is part of the "active expression"
-> [(Name, Expr)] -- ^ variables inlined previously on the LHS (see [Inlining])
-> [(Name, Expr)] -- ^ variables inlined previously on the RHS
-> Expr
-> Expr
-> Either [l] (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
moreRestrictive' mr_cont gen_lemma lkp s1@(State {expr_env = h1}) s2@(State {expr_env = h2}) ns hm active n1 n2 e1 e2 =
case (e1, e2) of
(Var i, _) | m <- idName i
, not $ HS.member m ns
, not $ (m, e2) `elem` n1
, Just (E.Conc e) <- lkp m s1 ->
moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active ((m, e2):n1) n2 e e2
(_, Var i) | m <- idName i
, not $ HS.member m ns
, not $ (m, e1) `elem` n2
, Just (E.Conc e) <- lkp m s2 ->
moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active n1 ((m, e1):n2) e1 e
(Var i1, Var i2) | HS.member (idName i1) ns
, idName i1 == idName i2 -> Right hm
| HS.member (idName i1) ns -> Left []
| HS.member (idName i2) ns -> Left []
(Var i, _) | Just (E.Sym _) <- lkp (idName i) s1
, (hm', hs) <- hm
, Nothing <- HM.lookup i hm' -> Right (HM.insert i (inlineEquiv lkp s2 ns e2) hm', hs)
| Just (E.Sym _) <- lkp (idName i) s1
, Just e <- HM.lookup i (fst hm)
, e == inlineEquiv lkp s2 ns e2 -> Right hm
-- this last case means there's a mismatch
| Just (E.Sym _) <- lkp (idName i) s1 -> Left []
| not $ (idName i, e2) `elem` n1
, not $ HS.member (idName i) ns -> error $ "unmapped variable " ++ (show i)
(_, Var i) | Just (E.Sym _) <- lkp (idName i) s2 -> Left [] -- sym replaces non-sym
| not $ (idName i, e1) `elem` n2
, not $ HS.member (idName i) ns -> error $ "unmapped variable " ++ (show i)
(App f1 a1, App f2 a2) | Right hm_fa <- moreResFA -> Right hm_fa
-- don't just choose the minimal conflicting expressions
-- collect all suitable pairs for potential lemmas
| not (hasFuncType e1)
, not (hasFuncType e2)
, not active
, Var (Id m1 _):_ <- unApp (modifyASTs stripTicks e1)
, Var (Id m2 _):_ <- unApp (modifyASTs stripTicks e2)
, nameOcc m1 == nameOcc m2
, Left lems <- moreResFA ->
Left $ (gen_lemma s1 s2 hm e1 e2):lems
| Left (_:_) <- moreResFA -> moreResFA
where
moreResFA = do
hm_f <- moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active n1 n2 f1 f2
moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm_f False n1 n2 a1 a2
-- These two cases should come after the main App-App case. If an
-- expression pair fits both patterns, then discharging it in a way that
-- does not add any extra proof obligations is preferable.
--
-- We use an empty HashSet when inlining because when generating a path constraint
-- we DO NOT want any top level names being preserved- these would just confuse the SMT solver.
(App _ _, _) | e1':_ <- unApp e1
, (Prim _ _) <- inlineEquiv lkp s1 HS.empty e1'
, T.isPrimType $ typeOf e1
, T.isPrimType $ typeOf e2
, isSWHNF $ (s2 { curr_expr = CurrExpr Evaluate e2 }) ->
let (hm', hs) = hm
in Right (hm', HS.insert (inlineEquiv lkp s1 HS.empty e1, inlineEquiv lkp s2 HS.empty e2) hs)
(_, App _ _) | e2':_ <- unApp e2
, (Prim _ _) <- inlineEquiv lkp s2 HS.empty e2'
, T.isPrimType $ typeOf e2
, T.isPrimType $ typeOf e1
, isSWHNF $ (s1 { curr_expr = CurrExpr Evaluate e1 }) ->
let (hm', hs) = hm
in Right (hm', HS.insert (inlineEquiv lkp s1 HS.empty e1, inlineEquiv lkp s2 HS.empty e2) hs)
-- We just compare the names of the DataCons, not the types of the DataCons.
-- This is because (1) if two DataCons share the same name, they must share the
-- same type, but (2) "the same type" may be represented in different syntactic
-- ways, most significantly bound variable names may differ
-- "forall a . a" is the same type as "forall b . b", but fails a syntactic check.
(Data (DataCon d1 _), Data (DataCon d2 _))
| d1 == d2 -> Right hm
| otherwise -> Left []
-- We neglect to check type equality here for the same reason.
(Prim p1 _, Prim p2 _) | p1 == p2 -> Right hm
| otherwise -> Left []
(Lit l1, Lit l2) | l1 == l2 -> Right hm
| otherwise -> Left []
(Lam lu1 i1 b1, Lam lu2 i2 b2)
| lu1 == lu2
, i1 == i2 ->
let ns' = HS.insert (idName i1) ns
-- no need to insert twice over because they're equal
in moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns' hm active n1 n2 b1 b2
| otherwise -> Left []
-- ignore types, like in exprPairing
(Type _, Type _) -> Right hm
-- only works if both binding lists are the same length
(Let binds1 e1', Let binds2 e2') ->
let pairs = (e1', e2'):(zip (map snd binds1) (map snd binds2))
ins (i_, e_) h_ = E.insert (idName i_) e_ h_
h1_ = foldr ins h1 binds1
h2_ = foldr ins h2 binds2
s1' = s1 { expr_env = h1_ }
s2' = s2 { expr_env = h2_ }
mf hm_ (e1_, e2_) = moreRestrictive' mr_cont gen_lemma lkp s1' s2' ns hm_ active n1 n2 e1_ e2_
in
if length binds1 == length binds2
then foldM mf hm pairs
else Left []
-- id equality never checked directly, but it's covered indirectly
(Case e1' i1 _ a1, Case e2' i2 _ a2)
| Right hm' <- b_mr ->
let h1_ = E.insert (idName i1) e1' h1
h2_ = E.insert (idName i2) e2' h2
s1' = s1 { expr_env = h1_ }
s2' = s2 { expr_env = h2_ }
mf hm_ (e1_, e2_) = moreRestrictiveAlt mr_cont gen_lemma lkp s1' s2' ns hm_ False n1 n2 e1_ e2_
l = zip a1 a2
in foldM mf hm' l
| otherwise -> b_mr
where
b_mr = moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active n1 n2 e1' e2'
(Cast e1' c1, Cast e2' c2) | c1 == c2 ->
moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active n1 n2 e1' e2'
-- ignore all Ticks
_ -> mr_cont s1 s2 ns hm active n1 n2 e1 e2
-- check only the names for DataAlt
altEquiv :: AltMatch -> AltMatch -> Bool
altEquiv (DataAlt dc1 ids1) (DataAlt dc2 ids2) =
let DataCon dn1 _ = dc1
DataCon dn2 _ = dc2
n1 = map idName ids1
n2 = map idName ids2
in
dn1 == dn2 && n1 == n2
altEquiv (LitAlt l1) (LitAlt l2) = l1 == l2
altEquiv Default Default = True
altEquiv _ _ = False
inlineEquiv :: Lookup t -> State t -> HS.HashSet Name -> Expr -> Expr
inlineEquiv lkp s ns v@(Var (Id n _))
| Just (E.Sym _) <- cs = v
| HS.member n ns = v
| Just (E.Conc e) <- cs = inlineEquiv lkp s (HS.insert n ns) e
where
cs = lkp n s
inlineEquiv lkp s ns e = modifyChildren (inlineEquiv lkp s ns) e
-- ids are the same between both sides; no need to insert twice
moreRestrictiveAlt :: MRCont t l
-> GenerateLemma t l
-> Lookup t
-> State t
-> State t
-> HS.HashSet Name
-> (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
-> Bool -- ^ active expression?
-> [(Name, Expr)] -- ^ variables inlined previously on the LHS
-> [(Name, Expr)] -- ^ variables inlined previously on the RHS
-> Alt
-> Alt
-> Either [l] (HM.HashMap Id Expr, HS.HashSet (Expr, Expr))
moreRestrictiveAlt mr_cont gen_lemma lkp s1 s2 ns hm active n1 n2 (Alt am1 e1) (Alt am2 e2) =
if altEquiv am1 am2 then
case am1 of
DataAlt _ t1 -> let ns' = foldr HS.insert ns $ map idName t1
in moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns' hm active n1 n2 e1 e2
_ -> moreRestrictive' mr_cont gen_lemma lkp s1 s2 ns hm active n1 n2 e1 e2
else Left []
-- s1 is old state, s2 is new state
-- only apply to old-new state pairs for which moreRestrictive' works
moreRestrictivePC :: (MonadIO m, S.Solver solver) =>
solver ->
State t ->
State t ->
HM.HashMap Id Expr ->
m Bool
moreRestrictivePC solver s1 s2 hm = do
let new_conds = map extractCond (P.toList $ path_conds s2)
old_conds = map extractCond (P.toList $ path_conds s1)
l = map (\(i, e) -> (Var i, e)) $ HM.toList hm
-- this should only be used with primitive types
-- no apparent problems come from using TyUnknown
l' = map (\(e1, e2) ->
if (T.isPrimType $ typeOf e1) && (T.isPrimType $ typeOf e2)
then Just $ App (App (Prim Eq TyUnknown) e1) e2
else Nothing) l
l'' = [c | Just c <- l']
new_conds' = l'' ++ new_conds
-- not safe to use unless the lists are non-empty
conj_new = foldr1 (\o1 o2 -> App (App (Prim And TyUnknown) o1) o2) new_conds'
conj_old = foldr1 (\o1 o2 -> App (App (Prim And TyUnknown) o1) o2) old_conds
imp = App (App (Prim Implies TyUnknown) conj_new) conj_old
neg_imp = ExtCond (App (Prim Not TyUnknown) imp) True
neg_conj = ExtCond (App (Prim Not TyUnknown) conj_old) True
res <- if null old_conds
then return $ S.UNSAT ()
else if null new_conds'
then liftIO $ applySolver solver (P.insert neg_conj P.empty) s1 s2
else liftIO $ applySolver solver (P.insert neg_imp P.empty) s1 s2
case res of
S.UNSAT () -> return True
_ -> return False
-- shortcut: don't invoke Z3 if there are no path conds
applySolver :: S.Solver solver =>
solver ->
PathConds ->
State t ->
State t ->
IO (S.Result () () ())
applySolver solver extraPC s1 s2 =
let unionEnv = E.union (expr_env s1) (expr_env s2)
rightPC = P.toList $ path_conds s2
unionPC = foldr P.insert (path_conds s1) rightPC
-- adding extraPC in here may be redundant
allPC = foldr P.insert unionPC (P.toList extraPC)
newState = s1 { expr_env = unionEnv, path_conds = extraPC }
in case (P.toList allPC) of
[] -> return $ S.SAT ()
_ -> S.check solver newState allPC
-- All the PathConds that this receives are generated by symbolic execution.
-- Consequently, non-primitive types are not an issue here.
extractCond :: PathCond -> Expr
extractCond (ExtCond e True) = e
extractCond (ExtCond e False) = App (Prim Not TyUnknown) e
extractCond (AltCond l e True) =
App (App (Prim Eq TyUnknown) e) (Lit l)
extractCond (AltCond l e False) =
App (App (Prim Neq TyUnknown) e) (Lit l)
extractCond _ = error "Not Supported"