IORef

base_setup.sh

@@ -1,4 +1,4 @@
-base_commit=6b9c713
+base_commit=78ca88e
 stubs_commit=afb11e3
 
 get_base() {

exe/Main.hs

@@ -63,15 +63,12 @@ printFuncCalls :: Config -> Id -> Bindings -> [ExecRes t] -> IO ()
 printFuncCalls config entry b =
  mapM_ (\execr@(ExecRes { final_state = s}) -> do
  let pg = mkPrettyGuide (exprNames $ conc_args execr)
- let funcCall = printHaskellPG pg s
- . foldl (\a a' -> App a a') (Var entry) $ (conc_args execr)
-
- let funcOut = printHaskellPG pg s $ (conc_out execr)
+ let (mvp, inp, outp) = printInputOutput pg entry execr
  sym_gen_out = fmap (printHaskellPG pg s) $ conc_sym_gens execr
 
  case sym_gen_out of
- S.Empty -> T.putStrLn $ funcCall <> " = " <> funcOut
- _ -> T.putStrLn $ funcCall <> " = " <> funcOut <> "\t| generated: " <> T.intercalate ", " (toList sym_gen_out))
+ S.Empty -> T.putStrLn $ mvp <> inp <> " = " <> outp
+ _ -> T.putStrLn $ mvp <> inp <> " = " <> outp <> "\t| generated: " <> T.intercalate ", " (toList sym_gen_out))
 
 ppStatePiece :: Bool -> String -> String -> IO ()
 ppStatePiece b n res =

g2.cabal

@@ -72,8 +72,8 @@ library
  , G2.Initialization.Types
 
  , G2.Interface
+ , G2.Interface.ExecRes
  , G2.Interface.Interface
- , G2.Interface.OutputTypes
 
  , G2.Language
  , G2.Language.AlgDataTy
@@ -99,6 +99,7 @@ library
  , G2.Language.Monad.TypeClasses
  , G2.Language.Monad.TypeEnv
  , G2.Language.Monad.Typing
+ , G2.Language.MutVarEnv
  , G2.Language.Naming
  , G2.Language.PathConds
  , G2.Language.Primitives

src/G2/Data/Utils.hs

@@ -4,7 +4,9 @@ module G2.Data.Utils ( uncurry3
  , fst4
  , snd4
  , thd4
- , fth4) where
+ , fth4
+
+ , (==>)) where
 
 uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
 uncurry3 f (a, b, c) = f a b c
@@ -22,4 +24,9 @@ thd4 :: (a, b, c, d) -> c
 thd4 (_, _, c, _) = c
 
 fth4 :: (a, b, c, d) -> d
-fth4 (_, _, _, d) = d
+fth4 (_, _, _, d) = d
+
+infixr 1 ==>
+(==>) :: Bool -> Bool -> Bool
+True ==> False = False
+_ ==> _ = True

src/G2/Execution/PrimitiveEval.hs

@@ -1,10 +1,11 @@
 {-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts, OverloadedStrings #-}
 
-module G2.Execution.PrimitiveEval (evalPrims, maybeEvalPrim, evalPrimSymbolic) where
+module G2.Execution.PrimitiveEval (evalPrims, mutVarTy, evalPrimMutVar, newMutVar, maybeEvalPrim, evalPrimSymbolic) where
 
 import G2.Language.AST
 import G2.Language.Expr
+import qualified G2.Language.KnownValues as KV
 import G2.Language.Naming
 import G2.Language.Primitives
 import G2.Language.Support
@@ -17,6 +18,10 @@ import qualified Data.HashMap.Lazy as M
 import qualified Data.List as L
 import Data.Maybe
 import qualified G2.Language.ExprEnv as E
+import G2.Language.ExprEnv (deepLookupExpr)
+import G2.Language.MutVarEnv
+
+import Debug.Trace
 
 evalPrims :: ASTContainer m Expr => TypeEnv -> KnownValues -> m -> m
 evalPrims tenv kv = modifyContainedASTs (evalPrims' tenv kv . simplifyCasts)
@@ -56,6 +61,57 @@ maybeEvalPrim' tenv kv xs
 
  | otherwise = Nothing
 
+-- | Evaluate primitives that deal with mutable variables.
+-- See Note [MutVar Env] in G2.Language.Support.
+evalPrimMutVar :: State t -- ^ Context to evaluate expression `e` in
+ -> NameGen
+ -> Expr -- ^ The expression `e` to evaluate
+ -> Maybe (State t, NameGen) -- ^ `Just` if `e` is a primitive operation on mutable variable, `Nothing` otherwise
+evalPrimMutVar s ng (App (App (App (App (Prim NewMutVar _) (Type t)) (Type ts)) e) _) = Just $ newMutVar s ng MVConc ts t e
+evalPrimMutVar s ng (App (App (App (App (Prim ReadMutVar _) _) _) mv_e) _)
+ | Just (Prim (MutVar mv) _) <- deepLookupExpr mv_e (expr_env s)=
+ let
+ i = lookupMvVal mv (mutvar_env s)
+ s' = maybe (error "evalPrimMutVar: MutVar not found")
+ (\i' -> s { curr_expr = CurrExpr Evaluate (Var i') })
+ i
+ in
+ Just (s', ng)
+evalPrimMutVar s ng (App (App (App (App (App (Prim WriteMutVar _) _) (Type t)) mv_e) e) pr_s)
+ | Just (Prim (MutVar mv) _) <- deepLookupExpr mv_e (expr_env s) =
+ let
+ (i, ng') = freshId t ng
+ s' = s { expr_env = E.insert (idName i) e (expr_env s)
+ , mutvar_env = updateMvVal mv i (mutvar_env s)
+ , curr_expr = CurrExpr Evaluate pr_s }
+ in
+ Just (s', ng')
+evalPrimMutVar _ _ e | [Prim WriteMutVar _, _, _, _, _, _] <- unApp e = trace ("e = " ++ show e) Nothing
+evalPrimMutVar _ _ _ = Nothing
+
+mutVarTy :: KnownValues
+ -> Type -- ^ The State type
+ -> Type -- ^ The stored type
+ -> Type
+mutVarTy kv ts ta = TyApp (TyApp (TyCon (KV.tyMutVar kv) (TyFun TYPE (TyFun TYPE TYPE))) ts) ta
+
+newMutVar :: State t
+ -> NameGen
+ -> MVOrigin
+ -> Type -- ^ The State type
+ -> Type -- ^ The stored type
+ -> Expr
+ -> (State t, NameGen)
+newMutVar s ng org ts t e =
+ let
+ (mv_n, ng') = freshSeededName (Name "mv" Nothing 0 Nothing) ng
+ (i, ng'') = freshId t ng' 
+ s' = s { curr_expr = CurrExpr Evaluate (Prim (MutVar mv_n) $ mutVarTy (known_values s) ts t)
+ , expr_env = E.insert (idName i) e (expr_env s)
+ , mutvar_env = insertMvVal mv_n i org (mutvar_env s)}
+ in
+ (s', ng'')
+
 evalPrim1 :: Primitive -> Lit -> Maybe Expr
 evalPrim1 Negate (LitInt x) = Just . Lit $ LitInt (-x)
 evalPrim1 Negate (LitRational x) = Just . Lit $ LitRational (-x)

src/G2/Execution/Reducer.hs

@@ -68,6 +68,7 @@ module G2.Execution.Reducer ( Reducer (..)
  , prettyLogger
  , limLogger
  , LimLogger (..)
+ , currExprLogger
 
  , ReducerEq (..)
  , (.==)
@@ -94,6 +95,8 @@ module G2.Execution.Reducer ( Reducer (..)
  , stdTimerHalter
  , timerHalter
 
+ , printOnHaltC
+
  -- * Orderers
  , mkSimpleOrderer
  , (<->)
@@ -128,6 +131,7 @@ import qualified Data.Map as M
 import Data.Maybe
 import qualified Data.List as L
 import qualified Data.Text as T
+import qualified Data.Text.IO as T
 import Data.Tuple
 import Data.Time.Clock
 import System.Directory
@@ -802,6 +806,36 @@ getFile dn is n s = do
  let fn = dir ++ n ++ show (length $ rules s) ++ ".txt"
  return fn
 
+-- | Output each path and current expression on the command line
+currExprLogger :: (MonadIO m, SM.MonadState PrettyGuide m, Show t) => LimLogger -> Reducer m LLTracker t
+currExprLogger ll@(LimLogger { after_n = aft, before_n = bfr, down_path = down }) = 
+ (mkSimpleReducer (const $ LLTracker { ll_count = every_n ll, ll_offset = []}) rr)
+ { updateWithAll = updateWithAllLL
+ , onAccept = \s b llt -> do
+ liftIO . putStrLn $ "Accepted on path " ++ show (ll_offset llt)
+ return (s, b)
+ , onDiscard = \_ llt -> liftIO . putStrLn $ "Discarded path " ++ show (ll_offset llt)}
+ where
+ rr llt@(LLTracker { ll_count = 0, ll_offset = off }) s b
+ | down `L.isPrefixOf` off || off `L.isPrefixOf` down
+ , aft <= length_rules && maybe True (length_rules <=) bfr = do
+ liftIO $ print off
+ pg <- SM.get
+ let pg' = updatePrettyGuide (s { track = () }) pg
+ SM.put pg'
+ liftIO . T.putStrLn $ printHaskellDirtyPG pg' (getExpr s)
+ return (NoProgress, [(s, llt { ll_count = every_n ll })], b)
+ | otherwise =
+ return (NoProgress, [(s, llt { ll_count = every_n ll })], b)
+ where
+ length_rules = length (rules s)
+ rr llt@(LLTracker {ll_count = n}) s b =
+ return (NoProgress, [(s, llt { ll_count = n - 1 })], b)
+
+ updateWithAllLL [(_, l)] = [l]
+ updateWithAllLL ss =
+ map (\(llt, i) -> llt { ll_offset = ll_offset llt ++ [i] }) $ zip (map snd ss) [1..]
+
 -- We use C to combine the halter values for HCombiner
 -- We should never define any other instance of Halter with C, or export it
 -- because this could lead to undecidable instances
@@ -990,6 +1024,18 @@ timerHalter ms def ce = do
  | v >= ce = 0
  | otherwise = v + 1
 
+-- | Print a specified message if a specified HaltC is returned from the contained Halter
+printOnHaltC :: MonadIO m =>
+ HaltC -- ^ The HaltC to watch for
+ -> String -- ^ The message to print
+ -> Halter m hv t -- ^ The contained Halter
+ -> Halter m hv t
+printOnHaltC watch mes h =
+ h { stopRed = \hv pr s -> do
+ halt_c <- stopRed h hv pr s
+ if halt_c == watch then liftIO $ putStrLn mes else return ()
+ return halt_c }
+
 -- Orderer things
 (<->) :: Monad m => Orderer m sov1 b1 t -> Orderer m sov2 b2 t -> Orderer m (C sov1 sov2) (b1, b2) t
 or1 <-> or2 = Orderer {

src/G2/Execution/Rules.hs

@@ -39,6 +39,7 @@ import Data.Maybe
 import qualified Data.HashMap.Lazy as HM
 import qualified Data.List as L
 import qualified Data.Sequence as S
+import G2.Data.Utils
 
 import Control.Exception
 
@@ -153,6 +154,7 @@ evalApp s@(State { expr_env = eenv
  ng e1 e2
  | ac@(Prim Error _) <- appCenter e1 =
  (RuleError, [newPCEmpty $ s { curr_expr = CurrExpr Return ac }], ng)
+ | Just (s', ng') <- evalPrimMutVar s ng (App e1 e2) = (RuleEvalPrimToNorm, [newPCEmpty $ s'], ng')
  | Just (e, eenv', pc, ng') <- evalPrimSymbolic eenv tenv ng kv (App e1 e2) =
  ( RuleEvalPrimToNorm
  , [ (newPCEmpty $ s { expr_env = eenv'
@@ -256,7 +258,8 @@ evalLet s@(State { expr_env = eenv })
 -- | Handle the Case forms of Evaluate.
 evalCase :: State t -> NameGen -> Expr -> Id -> Type -> [Alt] -> (Rule, [NewPC t], NameGen)
 evalCase s@(State { expr_env = eenv
- , exec_stack = stck })
+ , exec_stack = stck
+ , known_values = kv })
  ng mexpr bind t alts
  -- Is the current expression able to match with a literal based `Alt`? If
  -- so, we do the cvar binding, and proceed with evaluation of the body.
@@ -335,7 +338,13 @@ evalCase s@(State { expr_env = eenv
 
  alt_res = dsts_cs ++ lsts_cs ++ def_sts
  in
- assert (length alt_res == length dalts + length lalts + length defs)
+ -- We return exactly one state per branch, unless we are concretizing a MutVar.
+ -- In that case, we will return at least one state, but might return an unbounded
+ -- number more- see Note [MutVar Copy Concretization].
+ assert (tyConName (tyAppCenter $ typeOf mexpr) == Just (KV.tyMutVar kv)
+ ==> length alt_res >= length dalts + length lalts + length defs)
+ assert (tyConName (tyAppCenter $ typeOf mexpr) /= Just (KV.tyMutVar kv)
+ ==> length alt_res == length dalts + length lalts + length defs)
  (RuleEvalCaseSym, alt_res, ng'')
 
  -- Case evaluation also uses the stack in graph reduction based evaluation
@@ -351,6 +360,9 @@ evalCase s@(State { expr_env = eenv
  , exec_stack = S.push frame stck }], ng)
 
  | otherwise = error $ "reduceCase: bad case passed in\n" ++ show mexpr ++ "\n" ++ show alts
+ where
+ tyConName (TyCon n _) = Just n
+ tyConName _ = Nothing
 
 -- | Remove everything from an [Expr] that are actually Types.
 removeTypes :: [Expr] -> E.ExprEnv -> [Expr]
@@ -649,9 +661,68 @@ liftSymDefAlt s ng mexpr cvar as =
  Just aexpr -> liftSymDefAlt' s ng mexpr aexpr cvar as -- (liftSymDefAlt'' s mexpr aexpr cvar as, ng)
  _ -> ([], ng)
 
+-- Note [MutVar Copy Concretization]
+-- We must consider two possibilities when concretizing a MutVar:
+--
+-- 1) The MutVar is a new MutVar, containing a fresh symbolic value
+--
+-- 2) The MutVar is the same as some other MutVar that was previously concretized from a symbolic
+-- variable, and thus refers to the same mutable value.
+--
+-- To see why each of these possibilities must be considered, refer to the below program:
+--
+-- @
+-- k :: MutVar# RealWorld Int -> MutVar# RealWorld Int -> (Int, Int)
+-- k mv1 mv2 =
+-- let
+-- s1 = writeMutVar# mv1 2 realWorld#
+-- s2 = writeMutVar# mv2 6 s1
+
+-- (# s3, x1 #) = readMutVar# mv1 s2
+-- (# s4, x2 #) = readMutVar# mv2 s3 
+-- in
+-- (x1, x2)
+-- @
+--
+-- If mv1 and mv2 are different mutable variables, the functuon `k` will return the tuple (2, 6).
+-- However, if mv1 and mv2 are the same mutable variable, then `k` will return the tuple (6, 6).
+--
+-- Note that possibility (2) only involves concretizing MutVars to other MutVars that were themselves
+-- concretized from symbolic variables, not MutVars introduced by newMutVar#. This is due to ordering:
+-- if we have a symbolic MutVar mv1, and then introduce a new MutVar mv2 via newMutVar#, clearly
+-- mv1 and mv2 must be distinct. We use `MVOrigin`, in G2.Language.MutVar, to track whether a MutVar
+-- came from concretization or newMutVar#. 
+
 -- | Concretize Symbolic variable to Case Expr on its possible Data Constructors
 liftSymDefAlt' :: State t -> NameGen -> Expr -> Expr -> Id -> [Alt] -> ([NewPC t], NameGen)
-liftSymDefAlt' s@(State {type_env = tenv, expr_env = eenv}) ng mexpr aexpr cvar alts
+liftSymDefAlt' s@(State {type_env = tenv}) ng mexpr aexpr cvar alts
+ | Var i:_ <- unApp mexpr
+ , TyApp (TyApp mvt realworld_ty) stored_ty <- typeOf i
+ , TyCon n _ <- tyAppCenter mvt
+ , n == KV.tyMutVar (known_values s) =
+ let
+ binds = [(cvar, getExpr nmv_s)]
+ aexpr' = liftCaseBinds binds aexpr
+
+ -- Create a new mutable variable with a symbolic stored value
+ (stored_var, ng') = freshSeededId (idName i) stored_ty ng
+ (nmv_s, ng'') = newMutVar s ng' MVSymbolic realworld_ty stored_ty (Var stored_var)
+
+ eenv' = E.insertSymbolic stored_var $ E.insert (idName i) (getExpr nmv_s) (expr_env nmv_s)
+ nmv_s' = nmv_s { curr_expr = CurrExpr Evaluate aexpr', expr_env = eenv' }
+
+ -- Consider that the new mutable variable might be some existing mutable variable.
+ -- See Note [MutVar Copy Concretization].
+ mv_ty = mutVarTy (known_values s) realworld_ty stored_ty
+ rel_mutvar = HM.keys
+ $ HM.filter (\MVInfo { mv_val_id = Id _ t
+ , mv_origin = org } -> t == stored_ty && org == MVSymbolic) (mutvar_env s)
+ copy_states = map (\mv -> s { curr_expr = CurrExpr Evaluate aexpr'
+ , expr_env = E.insert (idName i) (Prim (MutVar mv) mv_ty) (expr_env s)
+ }
+ ) rel_mutvar
+ in
+ (map newPCEmpty (nmv_s':copy_states), ng'')
  | (Var i):_ <- unApp $ unsafeElimOuterCast mexpr
  , isADTType (typeOf i)
  , (Var i'):_ <- unApp $ exprInCasts mexpr = -- Id with original Type

src/G2/Initialization/KnownValues.hs

@@ -61,6 +61,13 @@ initKnownValues eenv tenv tc =
  , tyUnit = typeWithStrName tenv "()"
  , dcUnit = dcWithStrName tenv "()" "()"
 
+ , tyMutVar = typeWithStrName tenv "MutVar#"
+ , dcMutVar = dcWithStrName tenv "MutVar#" "MutVar#"
+ , tyState = typeWithStrName tenv "State#"
+ , dcState = dcWithStrName tenv "State#" "State#"
+ , tyRealWorld = typeWithStrName tenv "RealWorld"
+ , dcRealWorld = dcWithStrName tenv "RealWorld" "RealWorld"
+
  , eqTC = eqT
  , numTC = numT
  , ordTC = ordT

src/G2/Interface.hs

@@ -1,5 +1,5 @@
-module G2.Interface ( module G2.Interface.Interface
- , module G2.Interface.OutputTypes ) where
+module G2.Interface ( module G2.Interface.ExecRes
+ , module G2.Interface.Interface ) where
 
+import G2.Interface.ExecRes
 import G2.Interface.Interface
-import G2.Interface.OutputTypes