Can't handle 'switch' statements with more than one 'case'.

[ntc2]

It appears that JSS can't handle switch statements with more than one case. I ran into this when I tried to add a new Java example to the tutorial in doc/tutorial/code/FFS.java in the saw-script repo and it made SAW crash:

static int ffs_imp2(int i) {
    switch (((~i) + 1) ^ i) {
    case 0b11111111111111111111111111111110: return 1;
    case 0b11111111111111111111111111111100: return 2;
    case 0b11111111111111111111111111111000: return 3;
    case 0b11111111111111111111111111110000: return 4;
    case 0b11111111111111111111111111100000: return 5;
    case 0b11111111111111111111111111000000: return 6;
    case 0b11111111111111111111111110000000: return 7;
    case 0b11111111111111111111111100000000: return 8;
    case 0b11111111111111111111111000000000: return 9;
    case 0b11111111111111111111110000000000: return 10;
    case 0b11111111111111111111100000000000: return 11;
    case 0b11111111111111111111000000000000: return 12;
    case 0b11111111111111111110000000000000: return 13;
    case 0b11111111111111111100000000000000: return 14;
    case 0b11111111111111111000000000000000: return 15;
    case 0b11111111111111110000000000000000: return 16;
    case 0b11111111111111100000000000000000: return 17;
    case 0b11111111111111000000000000000000: return 18;
    case 0b11111111111110000000000000000000: return 19;
    case 0b11111111111100000000000000000000: return 20;
    case 0b11111111111000000000000000000000: return 21;
    case 0b11111111110000000000000000000000: return 22;
    case 0b11111111100000000000000000000000: return 23;
    case 0b11111111000000000000000000000000: return 24;
    case 0b11111110000000000000000000000000: return 25;
    case 0b11111100000000000000000000000000: return 26;
    case 0b11111000000000000000000000000000: return 27;
    case 0b11110000000000000000000000000000: return 28;
    case 0b11100000000000000000000000000000: return 29;
    case 0b11000000000000000000000000000000: return 30;
    case 0b10000000000000000000000000000000: return 31;
    case 0b00000000000000000000000000000000: return i == 0 ? 0 : 32;
    }
    return 0; // Unreachable.
}

Here are simple crashing and non-crashing examples:

// Crash.
static int ffs_imp3_4(int i) {
    switch (i) {
    case 0: break;
    case 1: break;
    }
    return 0;
}

// No crash, compare bytecode with ffs_imp3_4.
static int ffs_imp3(int i) {
    switch (i) {
    case 0: break;
    }
    return 0;
}

And here is the corresponding Java bytecode -- extracted with javap -c FFS -- which is what JSS is actually processing. Crash:

static int ffs_imp3_4(int);
  Code:
     0: iload_0
     1: lookupswitch  { // 2
                   0: 28
                   1: 31
             default: 31
        }
    28: goto          31
    31: iconst_0
    32: ireturn

No crash:

static int ffs_imp3(int);
  Code:
     0: iload_0
     1: lookupswitch  { // 1
                   0: 20
             default: 20
        }
    20: iconst_0
    21: ireturn

The lookupswitch JVM bytecode is processed by switch in src/Data/JVM/Symbolic/Translation.hs, and the problem manifests as an empty stack pop in popValue in src/Verifier/Java/Simulator.hs.

I pushed a debug-broken-java-switch-statements branch with these examples and some printf debugging inserted; I got side tracked failing to build SAW with profiling support to get stack traces. Run saw ffs_java.saw to see the crash.

[ntc2]

A patch with some relevant debug code:

commit 0321741a19c31fada029a3d45f9d424b2b99d391
Author: Nathan Collins <nathan.collins@gmail.com>
Date:   4 months ago

    WIP: debugging the java switch statement problem.

    My Java example could go in the tutorial if it worked.

diff --git src/Data/JVM/Symbolic/AST.hs src/Data/JVM/Symbolic/AST.hs
index a1f9d83..0e735e4 100644
--- src/Data/JVM/Symbolic/AST.hs
+++ src/Data/JVM/Symbolic/AST.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE StandaloneDeriving #-}

 -- | This module defines the main data types for the AST interpreted
 -- by the symbolic simulator. It enriches the JVM instruction set with
@@ -73,6 +74,11 @@ data SymInsn
   | NormalInsn J.Instruction
   deriving (Eq)

+deriving instance Show SymInsn
+deriving instance Show InvokeType
+deriving instance Show SymCond
+deriving instance Show CmpType
+
 ppSymInsn :: SymInsn -> Doc
 ppSymInsn stmt = case stmt of
     PushInvokeFrame it ty key bid -> 
diff --git src/Data/JVM/Symbolic/Translation.hs src/Data/JVM/Symbolic/Translation.hs
index 049ae0b..f4060cf 100644
--- src/Data/JVM/Symbolic/Translation.hs
+++ src/Data/JVM/Symbolic/Translation.hs
@@ -22,6 +22,8 @@ module Data.JVM.Symbolic.Translation
   , SymTransWarning
   ) where

+import Debug.Trace
+
 import Control.Applicative
 import Control.Monad
 import Control.Monad.RWS hiding ((<>))
@@ -168,7 +170,7 @@ liftBB cfg bb = do
              -> [Int32] 
              -> [(Int32, PC)]
              -> SymTrans ()
-      switch currId il d is cs = do
+      switch currId il d is cs = traceShow (currId, il, d, is, cs) $ do
         defineBlock currId $ reverse il ++ cases
         zipWithM_ defineBlock caseBlockIds (brSymInstrs cfg <$> targets)
           where targets = getBlock . snd <$> cs
diff --git src/Verifier/Java/Simulator.hs src/Verifier/Java/Simulator.hs
index f7b1f2b..2165292 100644
--- src/Verifier/Java/Simulator.hs
+++ src/Verifier/Java/Simulator.hs
@@ -92,6 +92,8 @@ module Verifier.Java.Simulator
   , module Verifier.Java.Codebase
   ) where

+import GHC.Stack
+
 import Prelude hiding (EQ, LT, GT)

 import Control.Applicative hiding (empty)
@@ -1497,7 +1499,7 @@ instance MonadSim sbe m => JavaSemantics (Simulator sbe m) where
   -- Pop value off top of stack.
   popValue = modifyCallFrameM "popValue" $ \cf -> 
                case cf^.cfOpds of
-                 [] -> err "empty operand stack"
+                 [] -> errorWithStackTrace "empty operand stack"
                  (x:xs) -> return (x, cf & cfOpds .~ xs)

   -- Push value onto top of stack.