debug

Author: lichye

src/main/scala/uclid/ConcreteSimulator.scala

@@ -65,6 +65,7 @@ case object Panic extends CmdsMod
     2. UninterpretedType
     3. FunctionCall
     4. evaluateBoolExpr
+    5. Json input support
 */
 
 sealed abstract class ConcreteValue{
@@ -125,9 +126,10 @@ object ConcreteSimulator {
     var undetCount: Int = 0;
     var cntInt:Int = 0;
     var terminateInt: Int = 0;
-    
+    var proofResults: ListBuffer[CheckResult] = ListBuffer[CheckResult]()
     //util
     val random = new Random()
+    
     case class ConcreteContext() {
         var varMap: scala.collection.mutable.Map[Identifier, ConcreteValue] = collection.mutable.Map();
         var varTypeMap: scala.collection.mutable.Map[Identifier, Type] = collection.mutable.Map();
@@ -143,13 +145,11 @@ object ConcreteSimulator {
             else if (inputMap.contains(variable)) inputMap(variable)
             else{
                 ConcreteUndef()
-                }
-            }
+            }}
         def write (variable: Identifier, value: ConcreteValue) {
             if (varMap.contains(variable)) varMap(variable) = value
             else if (inputMap.contains(variable)) inputMap(variable) = value
-            else throw new Error(f"Variable ${variable.toString} not found in context")
-        }
+            else throw new Error(f"Variable ${variable.toString} not found in context")}
         def updateVar (lhs: Lhs, value: ConcreteValue) {
             defaultLog.debug("Update "+lhs.toString+" With Value "+value.toString)
             lhs match {
@@ -247,9 +247,7 @@ object ConcreteSimulator {
                 varMap.-(variable_name)
             }}
 
-        def extendVarJson(frame:Int, vars: List[(Identifier, Type)]): Unit= {
-        ;}
-
+        def extendVarJson(frame:Int, vars: List[(Identifier, Type)]): Unit= {;}
         def assignUndefVar(vars: List[(Identifier, Type)],isInput: Boolean): Unit = {
             if(isInput){
                 var retContext = inputMap;
@@ -439,9 +437,7 @@ object ConcreteSimulator {
                 case _ => {
                     throw new Error("Hit unimplemented code part")
                 }
-            } 
-
-        }
+            } }
 
         //function gathring value as we want
         def generateValue(cValue:ConcreteValue,uclidType:Type,isInput:Boolean): ConcreteValue={      
@@ -588,8 +584,7 @@ object ConcreteSimulator {
                         case _ => ConcreteUndef()
                     }
                 }
-            }
-        }
+            }}
         //private Functions
         def updateRecordValue(fields: List[Identifier], value: ConcreteValue, 
             recordValue: ConcreteValue) : ConcreteRecord = {
@@ -643,11 +638,9 @@ object ConcreteSimulator {
             }
             for (variable <- vars){
                 println(variable._1+":  "+ConcreteSimulator.evaluate_expr(this,variable._1).toString)
-            }}
-    }
+            }}}
+    
 
-    var proofResults: ListBuffer[CheckResult] = ListBuffer[CheckResult]()
-
     def execute (module: Module, config: UclidMain.Config) : List[CheckResult] = {
         terminate = false;
         proofResults.clear();
@@ -853,7 +846,8 @@ object ConcreteSimulator {
                     }
                 }
                 case ConcreteUndef() => {
-                    true
+                    terminate = true
+                    return false
                 }
                 case _ => throw new NotImplementedError("Should not touch this line")
             }

test/concrete/concrete-0.ucl

@@ -1,3 +1,7 @@
+/*
+Test-conctete-0:
+1. test of property failure
+*/
 module main
 {
     var a : integer;
@@ -8,7 +12,6 @@ module main
     }
     next {
         a' = a + 1;
-    //    assert(a !=3);
     }
     property jump_a: a!=3;
 

test/concrete/concrete-1.ucl

@@ -1,3 +1,9 @@
+/* 
+  concrete-1.ucl
+  1. test of type of enum
+  2. test of procedure with modifies
+  3. test of assert
+*/
 module main
 {
     type color_t = enum { red, blue };

test/concrete/concrete-2.ucl

@@ -1,3 +1,9 @@
+/*
+  concrete-2.ucl
+  1. test of array
+  2. test of assert
+  3. test of touching undefine variable
+*/
 module main
 {
   type num_t = integer;
@@ -7,11 +13,16 @@ module main
   init {
     numbers[true] = 0;
     zero = numbers[true];
+    
+    // assert(read == 0);
   }
 
   next {
+    zero' = zero + read;
   }
 
+  // property p1: read == 1;
+
   control {
     v = concrete (5);
     check;