minor edits to the parsing

westtide · Feb 8, 2024 · cd38db2 · cd38db2
1 parent 9537562
commit cd38db2
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 16 deletions.
diff --git a/examples/copy.c b/examples/copy.c
@@ -3,18 +3,17 @@ void main() {
     int a[n];
     int b[n];
     int i=0;
-    int k;
-    assume(0 <= k && k < n);
 
     assume(0 <= n);
 
     while(i<n)
-      // invariant $main_inv1
     {
         b[i] = a[i];
         i++;
     }
-    // assert $main_sum1
+
+    int k;
     assert(i == n);
+    assume(0 <= k && k < n);
     assert(a[k] == b[k]);
 }
diff --git a/korn/src/korn/Main.scala b/korn/src/korn/Main.scala
@@ -200,11 +200,12 @@ object Main {
 
   def run(file: String) {
     info("program:      " + file)
+    val stmts = Tool.parse(file)
 
     if (dry) {
-      Tool.parse(file)
+      // do nothing
     } else if (tools.isEmpty) {
-      val unit = Tool.translate(file)
+      val unit = Tool.translate(file, stmts)
 
       if (write) {
         val to = write_smt2 getOrElse smt2(file)
@@ -217,6 +218,7 @@ object Main {
       }
     } else {
       import scala.util.control.Breaks._
+      val unit = Tool.translate(file, stmts)
 
       breakable {
         for (tool <- tools) {
@@ -225,8 +227,6 @@ object Main {
 
           info("running:      " + tool.how)
 
-          val unit = Tool.translate(file)
-
           val to = write_smt2 getOrElse smt2(file)
           if (tool.write)
             info("clauses:      " + to)

diff --git a/korn/src/korn/horn/Unit.scala b/korn/src/korn/horn/Unit.scala
@@ -163,9 +163,11 @@ class Unit(val file: String, stmts: List[Stmt]) {
 
       case FunDef(ret, "reach_error", formals, body) =>
       // built-in
+
       case stmt @ FunDef(ret, name, formals, body) =>
         val loc = korn.unpack(stmt.loc, "no location for while loop")
         define(loc, name, formals, ret, body)
+
       case _ =>
       // nothing to do
     }

diff --git a/korn/src/korn/tool/Solve.scala b/korn/src/korn/tool/Solve.scala
@@ -64,6 +64,8 @@ abstract class Solve extends Tool {
   }
 
   def check(unit: Unit, smt2: String) = {
+    unit.run()
+
     val (in, err, proc) = if (write) {
       val out = new PrintStream(new File(smt2))
       write(out, unit)

diff --git a/korn/src/korn/tool/Tool.scala b/korn/src/korn/tool/Tool.scala
@@ -4,11 +4,11 @@ import java.io.BufferedReader
 import java.io.InputStreamReader
 import java.io.PrintStream
 import korn.Main
+import korn.horn.Unit
 import korn.smt.Model
 import scala.concurrent.duration.Duration
 import korn.smt.Scanner
 import korn.smt.Parser
-import korn.horn.Unit
 
 sealed trait Result
 case class Unknown(status: String) extends Result
@@ -72,15 +72,12 @@ object Tool {
     status == 0
   }
 
-  def parse(file: String) {
-    val stmts = korn.c.parse(file)
+  def parse(file: String) = {
+    korn.c.parse(file)
   }
 
-  def translate(file: String) = {
-    val stmts = korn.c.parse(file)
-    object unit extends Unit(file, stmts)
-    unit.run()
-    unit
+  def translate(file: String, stmts: List[korn.c.Stmt]) = {
+    new korn.horn.Unit(file, stmts)
   }
 
   def model(in: BufferedReader): Model = {