talos: fixed up Case (Patterns) for muxvalue

talos/src/Talos/Lib.hs

@@ -0,0 +1,44 @@
+
+-- Functions which should be in other libraries but aren't
+
+module Talos.Lib where
+
+import qualified SimpleSMT                    as S
+import           SimpleSMT                    (SExpr)
+import Data.Foldable (toList)
+
+-- -----------------------------------------------------------------------------
+-- base
+
+-- short-circuiting
+andM :: Monad m => [m Bool] -> m Bool
+andM [] = pure True
+andM (m : ms) = do
+  b <- m
+  if b then andM ms else pure False
+
+orM :: Monad m => [m Bool] -> m Bool
+orM [] = pure False
+orM (m : ms) = do
+  b <- m
+  if b then pure True else orM ms
+
+findM :: (Foldable t, Monad m) => (a -> m Bool) -> t a -> m (Maybe a)
+findM f = go . toList
+  where
+    go [] = pure Nothing
+    go (x : xs) = do
+      b <- f x
+      if b then pure (Just x) else findM f xs
+
+-- -----------------------------------------------------------------------------
+-- simple-smt
+
+orMany :: [SExpr] -> SExpr
+orMany [x] = x
+orMany xs  = S.orMany xs
+
+andMany :: [SExpr] -> SExpr
+andMany [x] = x
+andMany xs  = S.andMany xs
+

talos/src/Talos/Path.hs

@@ -56,7 +56,9 @@ data SelectedPathF ch ca lp a =
 data PathIndex a  = PathIndex { pathIndex :: Int, pathIndexPath :: a }
   deriving (Eq, Ord, Functor, Foldable, Traversable, Generic, NFData)
 
-type SelectedPath = SelectedPathF PathIndex Identity SelectedLoopF ByteString
+-- We don't really need the index for cases, but it makes life a bit
+-- easier if we can just copy choice.
+type SelectedPath = SelectedPathF PathIndex PathIndex SelectedLoopF ByteString
 
 deriving instance NFData SelectedPath
 

talos/src/Talos/Strategy/PathSymbolic.hs

@@ -55,11 +55,11 @@ import qualified Talos.Strategy.OptParser                  as P
 import           Talos.Strategy.OptParser                  (Opt, parseOpts)
 import           Talos.Strategy.PathSymbolic.Monad
 import qualified Talos.Strategy.PathSymbolic.MuxValue      as MV
-import           Talos.Strategy.PathSymbolic.MuxValue      (GuardedSemiSExprs,
+import           Talos.Strategy.PathSymbolic.MuxValue      (MuxValue,
                                                             MuxValue (..),
-                                                            VSequenceMeta (..),
-                                                            ValueMatchResult (..),
-                                                            vUInt, vUnit)
+                                                            VSequenceMeta (..)
+--                                                           , vUInt, vUnit
+                                                           )
 import           Talos.Strategy.PathSymbolic.PathBuilder   (buildPaths)
 import qualified Talos.Strategy.PathSymbolic.PathSet as PS
 import           Talos.Strategy.PathSymbolic.PathSet (PathSet,
@@ -251,7 +251,7 @@ stratSlice = go
 -- 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 (GuardedSemiSExprs, (Int, PathBuilder)))
+                 SymbolicM (Maybe (MuxValue, (Int, PathBuilder)))
 guardedChoice pv i m = pass $ do
   m_r <- getMaybe m
   pure $ case m_r of
@@ -521,7 +521,7 @@ stratLoop lclass =
 
       pure (v, SelectedLoop node')
   where
-    execBnd :: (NonEmpty Int -> Int) -> Expr -> SymbolicM (GuardedSemiSExprs, Maybe Int)
+    execBnd :: (NonEmpty Int -> Int) -> Expr -> SymbolicM (MuxValue, Maybe Int)
     execBnd g bnd = do
       sbnd <- synthesiseExpr bnd
       let m_cbnd = fmap (g . fmap (fromIntegral . V.valueToSize)) (MV.asValues sbnd)
@@ -541,7 +541,7 @@ guardedLoopCollection :: VSequenceMeta ->
                          LoopCollection' e ->
                          SymbolicM b ->
                          Int ->
-                         GuardedSemiSExprs ->
+                         MuxValue ->
                          SymbolicM b
 guardedLoopCollection vsm lc m i el = do
   el' <- hoistMaybe (MV.refine g el)
@@ -571,90 +571,94 @@ guardedLoopCollection vsm lc m i el = do
 -- This can greatly increase the number of values
 
 -- FIXME: merge with the above?
-guardedCase :: NonEmpty PathCondition -> Pattern -> SymbolicM Result ->
-               SymbolicM (Maybe (GuardedSemiSExprs, (Pattern, PathBuilder)))
-guardedCase gs pat m = pass $ do
-  m_r <- getMaybe m
-  -- when (isNothing m_r) $ liftIO $ print ("Infeasible case: " ++ S.ppSExpr pathGuard "" ++ "\n")
-
-  pure $ case m_r of
-           Just r  -> (mk r, extendPath pathGuard)
-           Nothing -> (Nothing, notFeasible)
-  where
-    mk (v, pb) = do
-      x <-  MV.unions' (mapMaybe (flip MV.refine v) (NE.toList gs))
-      pure (x, (pat, pb))
+-- guardedCase :: NonEmpty PathCondition -> Pattern -> SymbolicM Result ->
+--                SymbolicM (Maybe (MuxValue, (Pattern, PathBuilder)))
+-- guardedCase gs pat m = pass $ do
+--   m_r <- getMaybe m
+--   -- when (isNothing m_r) $ liftIO $ print ("Infeasible case: " ++ S.ppSExpr pathGuard "" ++ "\n")
+
+--   pure $ case m_r of
+--            Just r  -> (mk r, extendPath pathGuard)
+--            Nothing -> (Nothing, notFeasible)
+--   where
+--     mk (v, pb) = do
+--       x <-  MV.unions' (mapMaybe (flip MV.refine v) (NE.toList gs))
+--       pure (x, (pat, pb))
 
-    pathGuard = MV.orMany (map PC.toSExpr (NE.toList gs))
-    notFeasible _ = mempty { smGuardedAsserts = [S.not pathGuard] }
+--     pathGuard = MV.orMany (map PC.toSExpr (NE.toList gs))
+--     notFeasible _ = mempty { smGuardedAsserts = [S.not pathGuard] }
 
 stratCase ::  Bool -> Case ExpSlice -> Maybe (Set SliceId) -> SymbolicM Result
 stratCase _total cs m_sccs = do
-  inv <- getName (caseVar cs)
-  (alts, preds) <- liftSemiSolverM (MV.semiExecCase cs)
-  -- liftIO $ printf "Length alts is %d\n\t%s\n" (length alts)
-  --                 (show $ commaSep [ pp p <> " => " <> pp vmr | (p, vmr) <- preds ])
-  let mk1 (gs, (pat, a)) = guardedCase gs pat (stratSlice a)
-  case m_sccs of
-    Just sccs
-      | any (hasRecCall sccs . snd . snd) alts -> do
-          -- In this case we just pick a random alt (and maybe
-          -- backtrack at some point?).  We ignore preds, as we assert
-          -- that the alt is reachable.
-
-          -- FIXME(!): this is incomplete
-          (v, (_pat, pb)) <- putMaybe . mk1 =<< randL alts
-          pure (v, SelectedCase (ConcreteCase pb))
-
-    _ -> do
-      stag <- freshSymbolicCaseTag
-
-      (vs, paths) <- unzip . catMaybes <$> mapM mk1 alts
-
-      v <- hoistMaybe (MV.unions' vs)
-      -- liftIO $ print ("case " <> pp (caseVar cs) <> " " <> block "[" "," "]" (map (pp . length . MV.guardedValues) vs)
-      --                 <> " ==> " <> pp (length (MV.guardedValues v))
-      --                 <> pp (text . typedThing <$> snd (head (MV.guardedValues v))))
-
-      -- preds here is a list [(PathCondition, SExpr)] where the PC is the
-      -- condition for the value, and the SExpr is a predicate on when
-      -- that value is enabled (matches some guard).  We require that at
-      -- least 1 alternative is enabled, so we assert the disjunction of
-      -- (g <-> s) for (g,s) in preds.  We could also assert the
-      -- conjunction of (g --> s), which does not assert that the guard
-      -- holds (only that the enabling predicate holds when that value is
-      -- enabled).
-
-      liftIO $ printf "Case on %s: %d -> %d\n" (showPP (caseVar cs)) (length (MV.guardedValues inv)) (length (MV.guardedValues v))
-
-      enabledChecks preds
-      recordCase stag (caseVar cs) [ (pcs, pat) | (pcs, (pat, _)) <- alts ]
-
-      pure (v, SelectedCase (SymbolicCase stag inv paths))
-
-  where
-    enabledChecks preds = do
-      --  | total     = pure ()
-      -- FIXME: Is it OK to omit this if the case is total?      
-      --  | otherwise = do
-          let preds' = over (each . _1) PC.toSExpr preds
-              patConstraints =
-                MV.andMany ([ g `sImplies` c | (g, SymbolicMatch c) <- preds' ]
-                            ++ [ S.not g | (g, NoMatch) <- preds' ])
-
-          oneEnabled <- case [ g | (g, vmr) <- preds', vmr /= NoMatch ] of
-                          [] -> do
-                            inv <- getName (caseVar cs)
-                            liftIO $ putStrLn ("No matches " ++ showPP cs ++ "\nValue\n"
-                                               ++ showPP (text . typedThing <$> inv)
-                                               ++ "\n" ++ show preds')
-                            infeasible
-                          ps -> pure (MV.orMany ps)
-
-          assertSExpr oneEnabled
-          assertSExpr patConstraints
-
-    hasRecCall sccs = \sl -> not (sliceToCallees sl `Set.disjoint` sccs)
+  v <- getName (caseVar cs)
+  pv <- freshPathVar
+  let (pred, missing) = MV.semiExecPatterns v pv (map fst (caseAlts cs))
+  undefined
+
+  -- (alts, preds) <- liftSemiSolverM (MV.semiExecCase cs)
+  -- -- liftIO $ printf "Length alts is %d\n\t%s\n" (length alts)
+  -- --                 (show $ commaSep [ pp p <> " => " <> pp vmr | (p, vmr) <- preds ])
+  -- let mk1 (gs, (pat, a)) = guardedCase gs pat (stratSlice a)
+  -- case m_sccs of
+  --   Just sccs
+  --     | any (hasRecCall sccs . snd . snd) alts -> do
+  --         -- In this case we just pick a random alt (and maybe
+  --         -- backtrack at some point?).  We ignore preds, as we assert
+  --         -- that the alt is reachable.
+
+  --         -- FIXME(!): this is incomplete
+  --         (v, (_pat, pb)) <- putMaybe . mk1 =<< randL alts
+  --         pure (v, SelectedCase (ConcreteCase pb))
+
+  --   _ -> do
+  --     stag <- freshSymbolicCaseTag
+
+  --     (vs, paths) <- unzip . catMaybes <$> mapM mk1 alts
+
+  --     v <- hoistMaybe (MV.unions' vs)
+  --     -- liftIO $ print ("case " <> pp (caseVar cs) <> " " <> block "[" "," "]" (map (pp . length . MV.guardedValues) vs)
+  --     --                 <> " ==> " <> pp (length (MV.guardedValues v))
+  --     --                 <> pp (text . typedThing <$> snd (head (MV.guardedValues v))))
+
+  --     -- preds here is a list [(PathCondition, SExpr)] where the PC is the
+  --     -- condition for the value, and the SExpr is a predicate on when
+  --     -- that value is enabled (matches some guard).  We require that at
+  --     -- least 1 alternative is enabled, so we assert the disjunction of
+  --     -- (g <-> s) for (g,s) in preds.  We could also assert the
+  --     -- conjunction of (g --> s), which does not assert that the guard
+  --     -- holds (only that the enabling predicate holds when that value is
+  --     -- enabled).
+
+  --     liftIO $ printf "Case on %s: %d -> %d\n" (showPP (caseVar cs)) (length (MV.guardedValues inv)) (length (MV.guardedValues v))
+
+  --     enabledChecks preds
+  --     recordCase stag (caseVar cs) [ (pcs, pat) | (pcs, (pat, _)) <- alts ]
+
+  --     pure (v, SelectedCase (SymbolicCase stag inv paths))
+
+  -- where
+  --   enabledChecks preds = do
+  --     --  | total     = pure ()
+  --     -- FIXME: Is it OK to omit this if the case is total?      
+  --     --  | otherwise = do
+  --         let preds' = over (each . _1) PC.toSExpr preds
+  --             patConstraints =
+  --               MV.andMany ([ g `sImplies` c | (g, SymbolicMatch c) <- preds' ]
+  --                           ++ [ S.not g | (g, NoMatch) <- preds' ])
+
+  --         oneEnabled <- case [ g | (g, vmr) <- preds', vmr /= NoMatch ] of
+  --                         [] -> do
+  --                           inv <- getName (caseVar cs)
+  --                           liftIO $ putStrLn ("No matches " ++ showPP cs ++ "\nValue\n"
+  --                                              ++ showPP (text . typedThing <$> inv)
+  --                                              ++ "\n" ++ show preds')
+  --                           infeasible
+  --                         ps -> pure (MV.orMany ps)
+
+  --         assertSExpr oneEnabled
+  --         assertSExpr patConstraints
+
+  --   hasRecCall sccs = \sl -> not (sliceToCallees sl `Set.disjoint` sccs)
 
 -- FIXME: this is copied from BTRand
 stratCallNode :: ExpCallNode ->
@@ -846,12 +850,12 @@ stratCallNode cn = do
 -- ----------------------------------------------------------------------------------------
 -- Solver helpers
 
-synthesiseExpr :: Expr -> SymbolicM GuardedSemiSExprs
+synthesiseExpr :: Expr -> SymbolicM MuxValue
 synthesiseExpr e = do
   r <- liftSemiSolverM . MV.semiExecExpr $ e
-  let vs = MV.guardedValues r
-      numSymb = length [ () | (_, MV.VOther _) <- vs ]
-  T.statS (pathKey <> "exprsize") (length vs, numSymb)
+  -- let vs = MV.guardedValues r
+  --     numSymb = length [ () | (_, MV.VOther _) <- vs ]
+  -- T.statS (pathKey <> "exprsize") (length vs, numSymb)
   pure r
 
 synthesiseByteSet :: ByteSet -> S.SExpr -> SymbolicM S.SExpr

talos/src/Talos/Strategy/PathSymbolic/Monad.hs

@@ -103,7 +103,8 @@ data SymbolicEnv = SymbolicEnv
 data SolverResult =
   ByteResult SMTVar
   | InverseResult (Map Name MuxValue) Expr -- The env. includes the result var.
- -- Not all paths are necessarily feasible.
+
+-- Not all paths are necessarily feasible.
 data PathChoiceBuilder a =
   SymbolicChoice   PathVar           [(Int, a)]
   | ConcreteChoice Int               a
@@ -112,11 +113,6 @@ data PathChoiceBuilder a =
 -- Used to tag cases so we can iterate through models
 type SymbolicCaseTag = GUID
 
-data PathCaseBuilder a   =
-  SymbolicCase   SymbolicCaseTag MuxValue [(Pattern, a)]
-  | ConcreteCase                   a
-  deriving (Functor)
-
 -- | When we see a loop while parsing a model we either suspend the
 -- loop (for pooling) and just record the loop's tag, or we have
 -- elements we just inline (for non-pooling loops).
@@ -126,9 +122,10 @@ data PathLoopBuilder a =
                       (Maybe LoopCountVar) -- 0 or 1
                       a
   | PathLoopMorphism SymbolicLoopTag
-                     [ (PathSet, MV.VSequenceMeta, [a]) ]
-
-type PathBuilder = SelectedPathF PathChoiceBuilder PathCaseBuilder PathLoopBuilder SolverResult
+                     [ (PathSet, (MV.VSequenceMeta, [a]) ) ]
+                     (MV.VSequenceMeta, [a])
+
+type PathBuilder = SelectedPathF PathChoiceBuilder PathChoiceBuilder PathLoopBuilder SolverResult
 
 emptySymbolicEnv :: Int -> Int -> ProvenanceTag -> SymbolicEnv
 emptySymbolicEnv maxRecDepth nLoopElements ptag = SymbolicEnv