[WIP] CBMC loops

Strata/Backends/CBMC/BoogieToCBMC.lean

@@ -41,7 +41,6 @@ def myProc : Boogie.Procedure := match SimpleTestEnvAST.fst.decls.head!.getProc?
   | .some p => p
   | .none => panic! "Expected procedure"
 
-
 class IdentToStr (I : Type) where
   toStr : I → String
 
@@ -60,23 +59,14 @@ instance : HasLExpr Boogie.Expression BoogieIdent where
 def exprToJson (I : Type) [IdentToStr I] (e : Lambda.LExpr Lambda.LMonoTy I) (loc: SourceLoc) : Json :=
   match e with
   | .app (.app (.op op _) left) right =>
-    let leftJson := match left with
-      | .fvar varName _ =>
-        if IdentToStr.toStr varName == "z" then
-          mkLvalueSymbol s!"{loc.functionName}::1::z" loc.lineNum loc.functionName
-        else
-          mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr varName}" loc.lineNum loc.functionName
-      | _ => exprToJson (I:=I) left loc
-    let rightJson := match right with
-      | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr varName}" loc.lineNum loc.functionName
-      | .const value _ => mkConstant value "10" (mkSourceLocation "ex_prog.c" loc.functionName loc.lineNum)
-      | _ => exprToJson (I:=I) right loc
+    let leftJson := exprToJson (I:=I) left loc
+    let rightJson := exprToJson (I:=I) right loc
     mkBinaryOp (opToStr (IdentToStr.toStr op)) loc.lineNum loc.functionName leftJson rightJson
   | .const "true" _ => mkConstantTrue (mkSourceLocation "ex_prog.c" loc.functionName "3")
   | .const n _ =>
     mkConstant n "10" (mkSourceLocation "ex_prog.c" loc.functionName "14")
   | .fvar name _ =>
-    mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr name}" loc.lineNum loc.functionName
+    mkLvalueSymbol (getIdent (IdentToStr.toStr name) loc.functionName) loc.lineNum loc.functionName
   | _ => panic! "Unimplemented"
 
 def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
@@ -90,7 +80,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
           ("id", "symbol"),
           ("namedSub", Json.mkObj [
             ("#source_location", mkSourceLocation "ex_prog.c" loc.functionName "5"),
-            ("identifier", Json.mkObj [("id", s!"{loc.functionName}::1::{name.toPretty}")]),
+            ("identifier", Json.mkObj [("id", getIdent name.toPretty loc.functionName)]),
             ("type", mkIntType)
           ])
         ]
@@ -101,7 +91,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
       let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" }
       mkCodeBlock "expression" "6" loc.functionName #[
         mkSideEffect "assign" "6" loc.functionName mkIntType #[
-          mkLvalueSymbol s!"{loc.functionName}::1::{name.toPretty}" "6" loc.functionName,
+          mkLvalueSymbol (getIdent name.toPretty loc.functionName) "6" loc.functionName,
           exprToJson (I:=BoogieIdent) expr exprLoc
         ]
       ]
@@ -195,6 +185,20 @@ partial def stmtToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr I] [HasL
         blockToJson (I:=I) elseb loc,
       ])
     ]
+  | .loop guard _ _ body _ =>
+    let converted_guard : Lambda.LExpr Lambda.LMonoTy I := @HasLExpr.expr_eq P (I:=I) _ ▸ guard
+    Json.mkObj [
+      ("id", "code"),
+      ("namedSub", Json.mkObj [
+        ("#source_location", mkSourceLocation "from_andrew.c" loc.functionName "8"),
+        ("statement", Json.mkObj [("id", "while")]),
+        ("type", emptyType)
+      ]),
+      ("sub", Json.arr #[
+        exprToJson (I:=I) converted_guard loc,
+        blockToJson (I:=I) body loc
+      ])
+    ]
   | _ => panic! "Unimplemented"
 end
 
@@ -368,6 +372,8 @@ def testSymbols (proc: Boogie.Procedure) : String := Id.run do
 
   -- Hardcode local variable for now
   let zSymbol := createLocalSymbol "z" proc.header.name.toPretty
+  let sumSymbol := createLocalSymbol "sum" proc.header.name.toPretty
+  let countSymbol := createLocalSymbol "count" proc.header.name.toPretty
 
   -- Build symbol map
   let mut m : Map String CBMCSymbol := Map.empty
@@ -377,10 +383,12 @@ def testSymbols (proc: Boogie.Procedure) : String := Id.run do
   -- Add parameter symbols
   for paramName in paramNames do
     let paramSymbol := createParameterSymbol paramName proc.header.name.toPretty
-    m := m.insert s!"{proc.header.name.snd}::{paramName}" paramSymbol
+    m := m.insert (getIdent paramName proc.header.name.snd) paramSymbol
 
   -- Add local variable
   m := m.insert s!"{proc.header.name.snd}::1::z" zSymbol
+  m := m.insert s!"{proc.header.name.snd}::1::sum" sumSymbol
+  m := m.insert s!"{proc.header.name.snd}::1::count" countSymbol
   toString (toJson m)
 
 end Boogie

Strata/Backends/CBMC/Common.lean

@@ -230,6 +230,19 @@ def mkSymbol (identifier : String) (symbolType : Json) : Json :=
     ])
   ]
 
+def createParameterSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol :=
+  createSymbol baseName "1" true true s!"{functionName}::" functionName config
+
+def createLocalSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol :=
+  let fullName := s!"{functionName}::1::{baseName}"
+  createSymbol baseName "5" false false s!"{functionName}::1::" functionName config fullName
+
+def getIdent (varName: String) (functionName: String) : String :=
+  if varName == "x" ∨ varName == "y" then
+    s!"{functionName}::{varName}"
+  else
+    s!"{functionName}::1::{varName}"
+
 -------------------------------------------------------------------------------
 
 /-! # Constants -/
@@ -342,7 +355,7 @@ def mkParameter (baseName : String) (functionName : String) (line : String) (con
     ("id", "parameter"),
     ("namedSub", Json.mkObj [
       ("#base_name", Json.mkObj [("id", baseName)]),
-      ("#identifier", Json.mkObj [("id", s!"{functionName}::{baseName}")]),
+      ("#identifier", Json.mkObj [("id", (getIdent baseName functionName))]),
       ("#source_location", mkSourceLocation config.sourceFile functionName line config),
       ("type", mkIntType config)
     ])
@@ -429,7 +442,9 @@ def opToStr (op: String) : String :=
   | "Int.Le" => "<="
   | "Int.Add" => "+"
   | "Int.Sub" => "-"
-  | _ => panic! "Unimplemented"
+  | "Bool.And" => "&&"
+  | "Bool.Or" => "||"
+  | _ => panic! s!"Unimplemented: {op}"
 
 def opToOutTypeJson (op: String) (config : CBMCConfig := .empty): Json :=
   match op with
@@ -439,7 +454,9 @@ def opToOutTypeJson (op: String) (config : CBMCConfig := .empty): Json :=
   | "<=" => boolType
   | "+" => mkIntType config
   | "-" => mkIntType config
-  | _ => panic! "Unimplemented"
+  | "&&" => boolType
+  | "||" => boolType
+  | _ => panic! s!"Unimplemented: {op}"
 
 
 def mkBinaryOp (op : String) (line : String) (functionName : String) (left : Json) (right : Json) (config : CBMCConfig := .empty) : Json :=
@@ -452,13 +469,6 @@ def mkBinaryOp (op : String) (line : String) (functionName : String) (left : Jso
     ("sub", Json.arr #[left, right])
   ]
 
-def createParameterSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol :=
-  createSymbol baseName "1" true true s!"{functionName}::" functionName config
-
-def createLocalSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol :=
-  let fullName := s!"{functionName}::1::{baseName}"
-  createSymbol baseName "5" false false s!"{functionName}::1::" functionName config fullName
-
 -------------------------------------------------------------------------------
 
 /-! # Code -/

Strata/Backends/CBMC/StrataToCBMC.lean

@@ -50,20 +50,6 @@ def myFunc : Strata.C_Simp.Function := SimpleTestEnvAST.fst.funcs.head!
 def lexprToCBMC (expr : Strata.C_Simp.Expression.Expr) (functionName : String) : Json :=
   let cfg := CBMCConfig.empty
   match expr with
-  | .app (.app (.op op _) (.fvar varName _)) (.const value _) =>
-    mkBinaryOp (opToStr op) "2" functionName (config := cfg)
-      (Json.mkObj [
-        ("id", "symbol"),
-        ("namedSub", Json.mkObj [
-          ("#base_name", Json.mkObj [("id", varName)]),
-          ("#id_class", Json.mkObj [("id", "1")]),
-          ("#lvalue", Json.mkObj [("id", "1")]),
-          ("#source_location", mkSourceLocation "from_andrew.c" functionName "2" cfg),
-          ("identifier", Json.mkObj [("id", s!"{functionName}::{varName}")]),
-          ("type", mkIntType cfg)
-        ])
-      ])
-      (mkConstant value "10" (mkSourceLocation "from_andrew.c" functionName "2" cfg) cfg)
   | .const "true" _ =>
     Json.mkObj [
       ("id", "notequal"),
@@ -82,7 +68,23 @@ def lexprToCBMC (expr : Strata.C_Simp.Expression.Expr) (functionName : String) :
         ]
       ])
     ]
-  | _ => panic! "Unimplemented"
+  | (.const value _) => (mkConstant value "10" (mkSourceLocation "from_andrew.c" functionName "2" cfg) cfg)
+  | (.fvar varName _) => (Json.mkObj [
+        ("id", "symbol"),
+        ("namedSub", Json.mkObj [
+          ("#base_name", Json.mkObj [("id", varName)]),
+          ("#id_class", Json.mkObj [("id", "1")]),
+          ("#lvalue", Json.mkObj [("id", "1")]),
+          ("#source_location", mkSourceLocation "from_andrew.c" functionName "2" cfg),
+          ("identifier", Json.mkObj [("id", getIdent varName functionName)]),
+          ("type", mkIntType cfg)
+        ])
+      ])
+  | .app (.app (.op op _) lhs) rhs =>
+    mkBinaryOp (opToStr op) "2" functionName (config := cfg)
+      (lexprToCBMC lhs functionName)
+      (lexprToCBMC rhs functionName)
+  | _ => panic! s!"Unimplemented {expr}"
 
 def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=
   let cfg := CBMCConfig.empty
@@ -196,11 +198,10 @@ def exprToJson (e : Strata.C_Simp.Expression.Expr) (loc: SourceLoc) : Json :=
   match e with
   | .app (.app (.op op _) left) right =>
     let leftJson := match left with
-      | .fvar "z" _ => mkLvalueSymbol s!"{loc.functionName}::1::z" loc.lineNum loc.functionName cfg
-      | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{varName}" loc.lineNum loc.functionName cfg
+      | .fvar varName _ => mkLvalueSymbol (getIdent varName loc.functionName) loc.lineNum loc.functionName cfg
       | _ => exprToJson left loc
     let rightJson := match right with
-      | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{varName}" loc.lineNum loc.functionName cfg
+      | .fvar varName _ => mkLvalueSymbol (getIdent varName loc.functionName) loc.lineNum loc.functionName cfg
       | .const value _ => mkConstant value "10" (mkSourceLocation "from_andrew.c" loc.functionName loc.lineNum cfg) cfg
       | _ => exprToJson right loc
     mkBinaryOp (opToStr op) loc.lineNum loc.functionName leftJson rightJson cfg
@@ -319,6 +320,19 @@ partial def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Json :=
         blockToJson elseb loc,
       ])
     ]
+  | .loop guard _ _ body _ =>
+    Json.mkObj [
+      ("id", "code"),
+      ("namedSub", Json.mkObj [
+        ("#source_location", mkSourceLocation "from_andrew.c" loc.functionName "8"),
+        ("statement", Json.mkObj [("id", "while")]),
+        ("type", emptyType)
+      ]),
+      ("sub", Json.arr #[
+        exprToJson guard loc,
+        blockToJson body loc
+      ])
+    ]
   | _ => panic! "Unimplemented"
 end
 
@@ -382,6 +396,8 @@ def testSymbols (myFunc: Strata.C_Simp.Function) : String := Id.run do
 
   -- Hardcode local variable for now
   let zSymbol := createLocalSymbol "z" myFunc.name
+  let sumSymbol := createLocalSymbol "sum" myFunc.name
+  let countSymbol := createLocalSymbol "count" myFunc.name
 
   -- Build symbol map
   let mut m : Map String CBMCSymbol := Map.empty
@@ -395,6 +411,8 @@ def testSymbols (myFunc: Strata.C_Simp.Function) : String := Id.run do
 
   -- Add local variable
   m := m.insert s!"{myFunc.name}::1::z" zSymbol
+  m := m.insert s!"{myFunc.name}::1::sum" sumSymbol
+  m := m.insert s!"{myFunc.name}::1::count" countSymbol
 
   toString (toJson m)
 

Strata/Backends/CBMC/compare_cbmc_json.sh

@@ -2,8 +2,8 @@
 
 # This is useful if e.g., you ask Claude to refactor your code and want it to test the refactoring doesn't change the test file.
 
-lake exe StrataToCBMC Strata/Backends/CBMC/tests/simpleTest.csimp.st > foo.json
+lake exe StrataToCBMC Strata/Backends/CBMC/tests/testLoop.csimp.st > foo.json
 python3 Strata/Backends/CBMC/resources/process_json.py combine Strata/Backends/CBMC/resources/defaults.json foo.json > full.json
-python3 Strata/Backends/CBMC/resources/process_json.py compare StrataTest/Backends/CBMC/simple_test_goto.json full.json
+python3 Strata/Backends/CBMC/resources/process_json.py compare StrataTest/Backends/CBMC/simple_test_loop_goto.json full.json
 
 rm foo.json full.json

Strata/Backends/CBMC/run_strata_cbmc.sh

@@ -7,7 +7,11 @@ lake exe StrataToCBMC $1 > foo.json
 python3 Strata/Backends/CBMC/resources/process_json.py combine Strata/Backends/CBMC/resources/defaults.json foo.json > full.json
 
 $CBMC_DIR/symtab2gb full.json --out full.goto
-$CBMC_DIR/goto-instrument --enforce-contract simpleTest full.goto full_checking.goto
-$CBMC_DIR/cbmc full_checking.goto --function simpleTest --trace
 
-rm foo.json full.json full.goto full_checking.goto
+
+$CBMC_DIR/goto-harness --function simpleTest --harness-function-name harness --harness-type call-function full.goto b.out
+$CBMC_DIR/goto-cc b.out --function harness -o c.out
+$CBMC_DIR/goto-instrument --dfcc harness --enforce-contract simpleTest c.out d.out
+$CBMC_DIR/cbmc d.out
+
+rm foo.json full.json full.goto b.out c.out d.out

Strata/Backends/CBMC/tests/testLoop.boogie.st

@@ -0,0 +1,22 @@
+program Boogie;
+
+procedure simpleTest (x: int, y: int) returns (ret : int)
+spec {
+}
+{
+  assume [assume_pos]: (x > 0);
+  assume [assume_smol]: (x < 10);
+  var sum : int;
+  sum := 0;
+  var count : int;
+  count := 0;
+  while
+  (count < x)
+  invariant (sum == count * x);
+  {
+    count := count + 1;
+    sum := sum + x;
+  }
+  assert [assert_pos]: (sum > 0);
+  ret := sum;
+};

Strata/Backends/CBMC/tests/testLoop.c

@@ -0,0 +1,15 @@
+int simpleTest(int x)
+  __CPROVER_requires((x > 0) && (x < 10))
+  __CPROVER_ensures(1)
+{
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(x < 10);
+  int sum = 0;
+  int count = 0;
+  while(count < 5) {
+    count++;
+    sum += x;
+  }
+  __CPROVER_assert(sum > 0, "sum_pos");
+  return sum;
+}

Strata/Backends/CBMC/tests/testLoop.csimp.st

@@ -0,0 +1,23 @@
+program C_Simp;
+
+int procedure simpleTest (x: int, y: int)
+  //@pre ((x > 0) && (x < 10));
+  //@post true;
+{
+  //@assume [assume_pos] (x > 0);
+  //@assume [assume_smol] (x < 10);
+  var sum : int;
+  sum = 0;
+  var count : int;
+  count = 0;
+  while
+  (count < x)
+  //@decreases (x-count)
+  //@invariant (count <= x && (sum == (count * x)))
+  {
+    count = count + 1;
+    sum = sum + x;
+  }
+  //@assert [assert_pos] (sum > 0);
+  return sum;
+}