talos: comp;iles after muxvalue changess

talos/src/Talos.hs

@@ -48,7 +48,7 @@ import           Talos.Analysis.Monad         (makeDeclInvs)
 import           Talos.Monad                  (runTalosM, runTalosStream, LogKey, logKeyEnabled, getLogKey)
 import           Talos.Passes
 import           Talos.Strategy
-import           Talos.SymExec.Path           (ProvenanceMap)
+import           Talos.Path                  (ProvenanceMap)
 import qualified Talos.Synthesis              as T
 import Data.Text (Text)
 

talos/src/Talos/Strategy.hs

@@ -26,14 +26,14 @@ import           Talos.Strategy.BTRand
 import           Talos.Strategy.Monad        (LiftStrategyM (..), StratGen(..),
                                               Strategy (..), StrategyM, StrategyInstance (siFun), siName, getSlice)
 import           Talos.Strategy.PathSymbolic (pathSymbolicStrat)
-import           Talos.Strategy.Symbolic     (symbolicStrat)
-import           Talos.SymExec.Path
-import           Talos.SymExec.SolverT       (SolverState, runSolverT)
+-- import           Talos.Strategy.Symbolic     (symbolicStrat)
+import           Talos.Path
+import           Talos.Solver.SolverT       (SolverState, runSolverT)
 import qualified Talos.Strategy.Monad as M
 
 
 allStrategies :: [Strategy]
-allStrategies = [ randRestart, randMaybeT, randDFS, pathSymbolicStrat, symbolicStrat] {- , backwardSymbolicStrat -}
+allStrategies = [ randRestart, randMaybeT, randDFS, pathSymbolicStrat] {- , backwardSymbolicStrat -}
 
 parseStrategies :: [String] -> Either String [StrategyInstance]
 parseStrategies ss = M.parseStrategies ss allStrategies

talos/src/Talos/Strategy/PathSymbolic.hs

@@ -248,20 +248,6 @@ stratSlice = go
             venv <- traverse getName fvM
             ptag <- asks sProvenance
             pure (n', SelectedBytes ptag (InverseResult venv ifn))
-
--- This function runs the given monadic action under the current pathc
--- extended with the give path condition.  In practice, it will run
--- the action, collect any assertions, predicate them by the path
--- condition, and also update the value.  If the computation fails,
--- then the negated path condition will be asserted and 
--- guardedChoice :: PathVar -> Int -> SymbolicM Result ->
---                  SymbolicM (Maybe ((PathSet, MuxValue), (Int, PathBuilder)))
--- guardedChoice pv i m =
---   handleUnreachable ps $ do
---     (v, p) <- m
---     pure ((ps, v), (i, p))
---   where
---     ps = PS.choiceConstraint pv i
 
 stratChoice :: [ExpSlice] -> Maybe (Set SliceId) -> SymbolicM Result
 -- stratChoice ptag sls (Just sccs)
@@ -275,17 +261,18 @@ stratChoice sls _
   | Nothing   <- NE.nonEmpty sls = unreachable
   | Just sls' <- NE.nonEmpty sls = do
       pv <- freshPathVar (length sls)
+
       let mk i sl = (PS.choiceConstraint pv i, over _2 ((,) i) <$> stratSlice sl)
       b <- branching $ B.branchingNE $ imap mk sls'
-      let (vs, paths) = B.unzip b
-          paths' = toList paths -- Ignore branching around paths.
-          
-      v <- liftSemiSolverM (MV.mux vs)
-      let feasibleIxs = map fst paths'
+      v <- liftSemiSolverM (MV.mux (fst <$> b))
+
+      let paths = map snd (toList b)
+          feasibleIxs = map fst paths
+
       -- Record that we have this choice variable, and the possibilities
       recordChoice pv feasibleIxs
 
-      pure (v, SelectedChoice (SymbolicChoice pv paths'))
+      pure (v, SelectedChoice (SymbolicChoice pv paths))
 
   -- liftIO $ print ("choice " <> block "[" "," "]" (map (pp . length . MV.guardedValues) vs)
   --                 <> " ==> " <> pp (length (MV.guardedValues v)))
@@ -576,12 +563,33 @@ guardedLoopCollection vsm lc m i el
 --     pathGuard = MV.orMany (map PS.toSExpr (NE.toList gs))
 --     notFeasible _ = mempty { smGuardedAsserts = [S.not pathGuard] }
 
+-- c.f. stratChoice
 stratCase ::  Bool -> Case ExpSlice -> Maybe (Set SliceId) -> SymbolicM Result
-stratCase _total cs m_sccs = do
-  v <- getName (caseVar cs)
-  pv <- freshPathVar (length (casePats cs))
-  let (pred, missing) = MV.semiExecPatterns v pv (map fst (casePats cs))
-  undefined
+stratCase _total cs@(Case n pats) m_sccs
+  | Nothing   <- NE.nonEmpty pats = unreachable
+  | Just pats' <- NE.nonEmpty pats = do
+      v <- getName n
+      pv <- freshPathVar (length pats)
+
+      let (assn, missing) = MV.semiExecPatterns v pv (map fst (casePats cs))
+
+      let go i sl | i `elem` missing = unreachable -- short-circuit, maybe tell the user?
+                  | otherwise = over _2 ((,) i) <$> stratSlice sl
+          mk i (_pat, sl) = (PS.choiceConstraint pv i, go i sl)
+
+      b <- branching $ B.branchingNE $ imap mk pats'
+      v <- liftSemiSolverM (MV.mux (fst <$> b))
+
+      let paths = map snd (toList b)
+          feasibleIxs = map fst paths
+
+      assertSExpr assn -- FIXME: generate a Branching in semiExecPatterns
+
+      -- FIXME: we are pretending that we are a choice
+      -- Record that we have this choice variable, and the possibilities
+      recordChoice pv feasibleIxs
+
+      pure (v, SelectedCase (SymbolicChoice pv paths))
 
   -- (alts, preds) <- liftSemiSolverM (MV.semiExecCase cs)
   -- -- liftIO $ printf "Length alts is %d\n\t%s\n" (length alts)

talos/src/Talos/Synthesis.hs

@@ -13,8 +13,8 @@
 
 module Talos.Synthesis (synthesise) where
 
-import           Control.Lens                    (at, (%=), (?~))
-import           Control.Monad                   (replicateM, when)
+import           Control.Lens                    (at, (%=), (?~), imap)
+import           Control.Monad                   (replicateM, when, guard)
 import           Control.Monad.Reader
 import           Control.Monad.State
 import           Data.ByteString                 (ByteString)
@@ -59,16 +59,16 @@ import           Talos.Analysis.Exported         (SliceId, esRootSlices)
 import           Talos.Analysis.Merge            (merge)
 import           Talos.Analysis.Slice
 -- import Talos.SymExec
-import           Talos.SymExec.Path
-import           Talos.SymExec.SolverT           (emptySolverState)
-import           Talos.SymExec.StdLib
+import           Talos.Path
+import           Talos.Solver.SolverT           (emptySolverState)
 
 import           Data.Functor.Of                 (Of ((:>)))
 import           Talos.Analysis.AbsEnv           (AbsEnvTy (AbsEnvTy))
 import           Talos.Monad                     (TalosM, getGFun, getIEnv,
                                                   getModule)
 import           Talos.Strategy
 import           Talos.Strategy.Monad
+import Data.Functor (($>))
 
 
 data Stream = Stream { streamOffset :: Integer
@@ -252,10 +252,6 @@ synthesise m_seed solv (AbsEnvTy p) strats root = S.effect $ do
   let solvSt0 = emptySolverState solv
       mc0 = newModelCache strats solvSt0
 
-  -- Init solver stdlib
-  -- FIXME: probably move?
-  liftIO $ makeStdLib solv 
-
   md <- getModule
   let Just rootDecl = find (\d -> fName d == root) (mGFuns md)
 
@@ -549,11 +545,16 @@ synthesiseG (SelectedChoice (PathIndex n sp)) (Choice _biased gs)
   | n < length gs = synthesiseG sp (gs !! n)
   | otherwise     = panic "Index out of bounds" []
 
-synthesiseG (SelectedCase (Identity sp)) (GCase cs) = do
+synthesiseG (SelectedCase (PathIndex n sp)) (GCase cs) = do
   let v = Var (caseVar cs)
   env <- projectEnvForM v
-  let base = panic "Failed to match pattern" [showPP cs]
-  I.evalCase (\g _ -> synthesiseG sp g) base cs env 
+  -- check interpreter agrees
+  let numberedCase = Case (caseVar cs) (imap (\i (pat, g) -> (pat, (i, g))) (casePats cs))
+      agrees = I.evalCase (\(i, g) _ -> guard (i == n) $> g) Nothing numberedCase env
+
+  case agrees of
+    Nothing -> panic "Mismatch in case" []
+    Just g -> synthesiseG sp g
 
 synthesiseG (SelectedCall fid sp) (Call fn args) = synthesiseCallG sp fn fid args