Implement 'whenSym' and hijack 'jumpZero' semantics.

iam.cabal

@@ -34,7 +34,7 @@ library
                      , pretty-simple
                      , algebraic-graphs
                      , process
-                     , selective
+                     , selective >= 0.1.0
                      , sbv
   default-language:    Haskell2010
 test-suite test-programs

src/Machine/Semantics.hs

@@ -15,7 +15,7 @@ import Prelude hiding (Monad, read, div, mod, abs, and, or)
 import qualified Prelude (Monad, div, mod, abs)
 import Data.Maybe (fromJust)
 import Control.Monad (join)
-import Data.SBV (Boolean (..))
+import Data.SBV hiding (Boolean)
 import Metalanguage
 import Machine.Types
 import Machine.Types.Value hiding (div, mod)
@@ -206,15 +206,27 @@ addS reg addr = \read write -> Just $
     let arg1   = read (Reg reg)
         arg2   = read (Addr addr)
         result = (+) <$> read (Reg reg) <*> read (Addr addr)
-        o1 = gt <$> arg2 <*> pure 0
-        o2 = gt <$> arg1 <*> ((-) <$> pure maxBound <*> arg2)
-        o3 = lt <$> arg2 <*> pure 0
-        o4 = lt <$> arg1 <*> ((-) <$> pure minBound <*> arg2)
-        o  = or <$> (and <$> o1 <*> o2)
-                <*> (and <$> o3 <*> o4)
+        o = willOverflowPure <$> arg1 <*> arg2
+        -- o1 = gt <$> arg2 <*> pure 0
+        -- o2 = gt <$> arg1 <*> ((-) <$> pure maxBound <*> arg2)
+        -- o3 = lt <$> arg2 <*> pure 0
+        -- o4 = lt <$> arg1 <*> ((-) <$> pure minBound <*> arg2)
+        -- o  = or <$> (and <$> o1 <*> o2)
+        --         <*> (and <$> o3 <*> o4)
     in  write (F Overflow) o *>
         write (Reg reg) result
 
+-- | A pure check for integer overflow during addition.
+willOverflowPure :: MachineValue a => a -> a -> a
+willOverflowPure x y =
+    let o1 = gt y 0
+        o2 = gt x((-) maxBound y)
+        o3 = lt y 0
+        o4 = lt x((-) minBound y)
+    in  or (and o1 o2)
+           (and o3 o4)
+
+
 -- | Sub a value from memory location to one in a register.
 --   Applicative.
 sub :: MachineValue a => Register -> MemoryAddress

src/Machine/Semantics/Symbolic.hs

@@ -79,13 +79,13 @@ symStep state =
               readRegister reg >>= writeMemory addr
           Add reg addr -> singleton . fromJust $ semanticsM i readKey writeKey
           Jump offset -> singleton . fromJust $ semanticsM i readKey writeKey
-          JumpZero offset ->
-            let isZero = SEq ((Map.!) (flags state) Zero) (SConst 0)
-            -- The computation branches and we return a list of two possible states:
-            in [ do appendConstraint isZero
-                    fromJust $ semanticsM (Jump offset) readKey writeKey
-               , appendConstraint (SNot isZero)
-               ]
+          JumpZero offset -> singleton . fromJust $ semanticsM i readKey writeKey
+            -- let isZero = SEq ((Map.!) (flags state) Zero) (SConst 0)
+            -- -- The computation branches and we return a list of two possible states:
+            -- in [ do appendConstraint isZero
+            --         fromJust $ semanticsM (Jump offset) readKey writeKey
+            --    , appendConstraint (SNot isZero)
+            --    ]
           Sub reg addr -> singleton . fromJust $ semanticsM i readKey writeKey
           Mod reg addr -> singleton . fromJust $ semanticsM i readKey writeKey
           Mul reg addr -> singleton . fromJust $ semanticsM i readKey writeKey
@@ -193,6 +193,7 @@ writeFlag flag value = do
     delay 1
     modify $ \currentState ->
         currentState {
+
             flags = Map.adjust (const value) flag (flags currentState)}
 
 -- --------------------------------------------------------------------------------

src/Machine/Semantics/Symbolic/SMT.hs

@@ -7,6 +7,7 @@ import Data.Monoid
 import Control.Monad.Reader (ask)
 import Control.Monad.Trans (liftIO)
 import qualified Data.SBV.Dynamic as SBV
+import Data.SBV (constrain, SBool)
 
 import Machine.Types
 import Machine.Instruction.Decode
@@ -102,7 +103,7 @@ sValToSWord :: SBV.SVal -> SBV.SVal
 sValToSWord w = SBV.svIte w (valueToSVal 1) (valueToSVal 0)
 
 renderSMTResult :: SBV.SMTResult -> String
-renderSMTResult (SBV.Unsatisfiable _) = "Unsatisfiable"
+renderSMTResult (SBV.Unsatisfiable _ _) = "Unsatisfiable"
 renderSMTResult s@(SBV.Satisfiable _ _) =
   let dict = SBV.getModelDictionary s
   in
@@ -128,7 +129,7 @@ data SolvedState = SolvedState SymState SBV.SMTResult
 solveSym :: Trace -> IO (Tree.Tree SolvedState)
 solveSym (Tree.Node state c) = do
     let smtExpr = toSMT (pathConstraintList state)
-    SBV.SatResult smtRes <- SBV.satWith prover smtExpr
+    SBV.SatResult smtRes <- SBV.satWith prover (smtExpr)
     children <- traverse solveSym c
     pure $ Tree.Node (SolvedState state smtRes) children