support for switch

cc-parser/concurrentC.cf

@@ -191,7 +191,7 @@ DecS.     Stm ::= Dec ; -- beyond ANSI-C
 AtomicS.  Stm ::= Atomic_stm ;
 
 SlabelOne.   Labeled_stm ::= CIdent ":" Stm ;
--- SlabelTwo.   Labeled_stm ::= "case" Constant_expression ":" Stm ;
+SlabelTwo.   Labeled_stm ::= "case" Constant_expression ":" Stm ;
 SlabelThree. Labeled_stm ::= "default" ":" Stm;
 
 ScompOne.   Compound_stm ::= "{" "}" ;

regression-tests/horn-hcc-2/Answers

@@ -227,6 +227,29 @@ Final:
 typedef1.hcc
 SAFE
 
+switch1.hcc
+UNSAFE
+
+--------------
+Init:
+ main4(0, 10) 
+--------------
+      |       
+      |       
+      V       
+ main5(0, 0)  
+--------------
+Final:
+ main5(0, 0)  
+--------------
+
+switch2.hcc
+Warning: no definition of function "nondet" available
+Warning: no definition of function "nondet" available
+Warning: no definition of function "nondet" available
+Warning: no definition of function "nondet" available
+SAFE
+
 hints.hcc
 SAFE
 

regression-tests/horn-hcc-2/runtests

@@ -8,7 +8,7 @@ TESTS="atomic3e.hcc atomic3f.hcc \
        channels.hcc channels-2.hcc channels-2b.hcc channels-3.hcc \
        duration1.hcc duration2.hcc \
        duration3.hcc duration3b.hcc duration3c.hcc duration3d.hcc \
-       nonlinear1.hcc nonlinear2.hcc typedef1.hcc"
+       nonlinear1.hcc nonlinear2.hcc typedef1.hcc switch1.hcc switch2.hcc"
 
 for name in $TESTS; do
     echo

regression-tests/horn-hcc-2/switch1.hcc

@@ -0,0 +1,20 @@
+
+
+void main() {
+  int x;
+  int y = 10;
+
+  switch(x) {
+    case 1: case 2:
+      y = 42;
+      break;
+    case 3:
+      y = 43;
+      break;
+    default:
+      y = 0;
+      break;
+  }
+
+  assert(y >= 1);
+}

regression-tests/horn-hcc-2/switch2.hcc

@@ -0,0 +1,26 @@
+
+int N = _;
+
+int nondet();
+
+void main() {
+  int x = 0, y = 0;
+  int s = 0;
+
+  loop : while (s != 3) {
+
+  switch(s) {
+                         s = 0; case 0: if (nondet()) goto loop;
+      while (x <= N) {
+                         s = 1; case 1: if (nondet()) goto loop;
+        x++;
+                         s = 2; case 2: if (nondet()) goto loop;
+        y++;
+      }
+                         s = 3; case 3: if (nondet()) goto loop;
+  }
+
+  }
+
+  assert(x == y);
+}

src/lazabs/horn/concurrency/CCReader.scala

@@ -898,6 +898,18 @@ class CCReader private (prog : Program,
 
   //////////////////////////////////////////////////////////////////////////////
 
+  private def translateConstantExpr(expr : Constant_expression) : CCExpr = {
+    val symex = Symex(null)
+    symex.saveState
+    val res = symex eval expr.asInstanceOf[Especial].exp_
+    if (!symex.atomValuesUnchanged)
+      throw new TranslationException(
+        "constant expression is not side-effect free")
+    res
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+
   private object Symex {
     def apply(initPred : Predicate) = {
       val values = new ArrayBuffer[CCExpr]
@@ -1048,6 +1060,11 @@ class CCReader private (prog : Program,
       outputClause(elsePred)
     }
 
+    def assertProperty(property : IFormula) : Unit = {
+      import HornClauses._
+      assertionClauses += (property :- (initAtom, guard))
+    }
+
     def addValue(t : CCExpr) = {
       values += t
       touchedGlobalState = touchedGlobalState || !freeFromGlobal(t)
@@ -1352,15 +1369,12 @@ class CCReader private (prog : Program,
 
       case exp : Efunkpar => (printer print exp.exp_) match {
         case "__VERIFIER_error" if (exp.listexp_.isEmpty) => {
-          import HornClauses._
-          assertionClauses += (false :- (initAtom, guard))
+          assertProperty(false)
           pushVal(CCFormula(true, CCInt))
         }
         case "assert" | "static_assert" | "__VERIFIER_assert"
                           if (exp.listexp_.size == 1) => {
-          import HornClauses._
-          val property = atomicEval(exp.listexp_.head).toFormula
-          assertionClauses += (property :- (initAtom, guard))
+          assertProperty(atomicEval(exp.listexp_.head).toFormula)
           pushVal(CCFormula(true, CCInt))
         }
         case "assume" | "__VERIFIER_assume"
@@ -1808,8 +1822,15 @@ class CCReader private (prog : Program,
         labelledLocs.put(stm.cident_, (entry, allFormalVars))
         translate(stm.stm_, entry, exit)
       }
-      //-- SlabelTwo.   Labeled_stm ::= "case" Constant_expression ":" Stm ;
-      //SlabelThree. Labeled_stm ::= "default" ":" Stm;
+      case stm : SlabelTwo => { // Labeled_stm ::= "case" Constant_expression ":" Stm ;
+        val caseVal = translateConstantExpr(stm.constant_expression_)
+        innermostSwitchCaseCollector += ((caseVal, entry))
+        translate(stm.stm_, entry, exit)
+      }
+      case stm : SlabelThree => { // . Labeled_stm ::= "default" ":" Stm;
+        innermostSwitchCaseCollector += ((null, entry))
+        translate(stm.stm_, entry, exit)
+      }
     }
 
     private def translateWithEntryClause(
@@ -1905,8 +1926,11 @@ class CCReader private (prog : Program,
         }
     }
 
+    type SwitchCaseCollector = ArrayBuffer[(CCExpr, Predicate)]
+
     var innermostLoopCont : Predicate = null
     var innermostLoopExit : Predicate = null
+    var innermostSwitchCaseCollector : SwitchCaseCollector = null
 
     private def withinLoop[A](
                      loopCont : Predicate, loopExit : Predicate)
@@ -1923,6 +1947,22 @@ class CCReader private (prog : Program,
       }
     }
 
+    private def withinSwitch[A](
+                     switchExit : Predicate,
+                     caseCollector : SwitchCaseCollector)
+                     (comp : => A) : A = {
+      val oldExit = innermostLoopExit
+      val oldCollector = innermostSwitchCaseCollector
+      innermostLoopExit = switchExit
+      innermostSwitchCaseCollector = caseCollector
+      try {
+        comp
+      } finally {
+        innermostLoopExit = oldExit
+        innermostSwitchCaseCollector = oldCollector
+      }
+    }
+
     private def translate(stm : Iter_stm,
                           entry : Predicate,
                           exit : Predicate) : Unit = stm match {
@@ -1993,7 +2033,7 @@ class CCReader private (prog : Program,
     private def translate(stm : Selection_stm,
                           entry : Predicate,
                           exit : Predicate) : Unit = stm match {
-      case _ : SselOne | _ : SselTwo => {
+      case _ : SselOne | _ : SselTwo => { // if
         val first, second = newPred
         val vars = allFormalVars
         val condSymex = Symex(entry)
@@ -2013,7 +2053,44 @@ class CCReader private (prog : Program,
           }
         }
       }
-//      case stm : SselThree.  Selection_stm ::= "switch" "(" Exp ")" Stm ;
+
+      case stm : SselThree => {  // switch
+        val selectorSymex = Symex(entry)
+        val selector = (selectorSymex eval stm.exp_).toTerm
+
+        val newEntry = newPred
+        val collector = new SwitchCaseCollector
+
+        withinSwitch(exit, collector) {
+          translate(stm.stm_, newEntry, exit)
+        }
+
+        // add clauses for the various cases of the switch
+        val (defaults, cases) = collector partition (_._1 == null)
+        val guards = for ((value, _) <- cases) yield (selector === value.toTerm)
+
+        for (((_, target), guard) <- cases.iterator zip guards.iterator) {
+          selectorSymex.saveState
+          selectorSymex addGuard guard
+          selectorSymex outputClause target
+          selectorSymex.restoreState
+        }
+
+        defaults match {
+          case Seq() =>
+            // add an assertion that we never try to jump to a case that
+            // does not exist. TODO: add a parameter for this?
+            selectorSymex assertProperty or(guards)
+          case Seq((_, target)) => {
+            selectorSymex.saveState
+            selectorSymex addGuard ~or(guards)
+            selectorSymex outputClause target
+            selectorSymex.restoreState
+          }
+          case _ =>
+            throw new TranslationException("multiple default cases in switch")
+        }
+      }
     }
 
     private def translate(jump : Jump_stm,

src/lazabs/horn/concurrency/ReplacingLexer.scala

@@ -40,10 +40,10 @@ object TypedefReplacingLexer {
   //   cc-parser/lazabs/horn/concurrency/concurrentC/Yylex
   // ?
 
-  val Typedef_num   = sym._SYMB_76;
-  val Struct_num    = sym._SYMB_73;
-  val Enum_num      = sym._SYMB_60;
-  val Union_num     = sym._SYMB_77;
+  val Typedef_num   = sym._SYMB_77;
+  val Struct_num    = sym._SYMB_74;
+  val Enum_num      = sym._SYMB_61;
+  val Union_num     = sym._SYMB_78;
   val Semicolon_num = sym._SYMB_2;
   val LBrace_num    = sym._SYMB_7;
   val RBrace_num    = sym._SYMB_8;