ccmp and rpo sort

UQ-PAC · Nov 13, 2024 · d3b8176 · d3b8176
1 parent 08af7a3
commit d3b8176
Show file tree

Hide file tree

Showing 9 changed files with 201 additions and 132 deletions.
diff --git a/src/main/scala/ir/Program.scala b/src/main/scala/ir/Program.scala
@@ -176,7 +176,7 @@ class ProgramThread(val entry: Procedure,
 */
 
 class Procedure private (
-                  var name: String,
+                  var procName: String,
                   var address: Option[BigInt],
                   private var _entryBlock: Option[Block],
                   private var _returnBlock: Option[Block],
@@ -188,6 +188,9 @@ class Procedure private (
                   var requires: List[BExpr],
                   var ensures: List[BExpr],
                 ) extends Iterable[CFGPosition] {
+
+  def name = procName + address.map("_" + _).getOrElse("") 
+
   private val _callers = mutable.HashSet[DirectCall]()
   _blocks.foreach(_.parent = this)
   // class invariant

diff --git a/src/main/scala/ir/Visitor.scala b/src/main/scala/ir/Visitor.scala
@@ -382,7 +382,7 @@ class Renamer(reserved: Set[String]) extends Visitor {
 
   override def visitProcedure(node: Procedure): Procedure = {
     if (reserved.contains(node.name)) {
-      node.name = s"#${node.name}"
+      node.procName = s"#${node.name}"
     }
     super.visitProcedure(node)
   }

diff --git a/src/main/scala/ir/eval/ExprEval.scala b/src/main/scala/ir/eval/ExprEval.scala
@@ -41,7 +41,7 @@ def evalBVBinExpr(b: BVBinOp, l: BitVecLiteral, r: BitVecLiteral): BitVecLiteral
 
 def evalBVLogBinExpr(b: BVBinOp, l: BitVecLiteral, r: BitVecLiteral): Boolean = b match {
   case BVULE => BitVectorEval.smt_bvule(l, r)
-  case BVUGT => BitVectorEval.smt_bvult(l, r)
+  case BVUGT => BitVectorEval.smt_bvugt(l, r)
   case BVUGE => BitVectorEval.smt_bvuge(l, r)
   case BVULT => BitVectorEval.smt_bvult(l, r)
   case BVSLT => BitVectorEval.smt_bvslt(l, r)