Change simplification logic for two's complement negation and fix applyTransform method to generate IL.

Author: morriisw

scripts/tnum_test_z3.py

@@ -47,14 +47,6 @@ def subset(self, other):
         val_cmp = ((self.v & ~other.m) == other.v)
         return mask_cmp & val_cmp
 
-        # self_m_extended = ZeroExt(self.w - self.m.size(), self.m)
-        # other_m_extended = ZeroExt(self.w - other.m.size(), other.m)
-        # self_v_extended = ZeroExt(self.w - self.v.size(), self.v)
-        # other_v_extended = ZeroExt(self.w - other.v.size(), other.v)
-        # mask_cmp = (self_m_extended & ~other_m_extended) == BitVecVal(0, self.w)
-        # val_cmp = (self_v_extended & ~other_m_extended) == other_v_extended
-        # return mask_cmp & val_cmp
-
     def union(self,other):
         mask = self.m | other.m | (self.v ^ other.v)
         val = self.v & ~mask
@@ -64,12 +56,9 @@ def __invert__(self):
         return TNum(~self.v & ~self.m, self.m)
 
     def __neg__(self):
-        return TNum(-self.v & ~self.m, self.m)
+        tnum = TNum(BitVecVal(0, self.w), BitVecVal(0, self.w))
+        return tnum - self
 
-        # val = If(-self.v & ~self.m == self.v, ZeroExt(1, -self.v & ~self.m), ZeroExt(1, -self.v & ~self.m))
-        # mask = If(-self.v & ~self.m == self.v, ZeroExt(1, self.m), ZeroExt(1, self.m))
-        # return TNum(val, mask)
-    
     def __and__(self, other):
         alpha = self.v | self.m
         beta = other.v | other.m
@@ -398,7 +387,6 @@ def test_uop(name, tf, tf_c=None, prec=False, width=4):
 test_bop("TXNOR", lambda x, y: xnor_tnum(x, y), xnor_bitvec, prec=True)
 test_bop("TNAND", lambda x, y: nand_tnum(x, y), nand_bitvec, prec=True)
 test_bop("TADD", lambda x, y: x + y,  prec=True)
-
 test_bop("TSUB", lambda x, y: x - y,  prec=True)
 test_bop("TSHL", lambda x, y: x << y,  prec=True)
 test_bop("TASHR", lambda x, y: x >> y,  prec=True)
@@ -408,5 +396,5 @@ def test_uop(name, tf, tf_c=None, prec=False, width=4):
 test_bop("CONCAT", lambda x, y: concat_tnum(x, y), concat_bitvec, prec=True)
 
 test_uop("INV", lambda x: ~x, prec=True)
-# test_uop("NEG", lambda x: -x, prec=True)
+test_uop("NEG", lambda x: -x, prec=True)
 # test_bop("TMUL", lambda x, y: x * y,  prec=True)

src/main/scala/ir/transforms/SimplifyKnownBits.scala

@@ -1,5 +1,6 @@
 package ir.transforms
 import ir.*
+import util.writeToFile
 
 // A = definite 1 bits, B = unknown bits
 // A_[i] = 1, B_[i] = 0 -> Bit i of TNum _ is definitely 1
@@ -78,6 +79,7 @@ case class TNumValue(value: BigInt, mask: BigInt) extends TNum {
   override def toString() = {
     "v.%#016x m.%#016x".format(value, mask)
   }
+
   // Bitwise AND
   def TAND(that: TNumValue): TNumValue = {
     val alpha = this.value | this.mask
@@ -428,7 +430,7 @@ case class TNumValue(value: BigInt, mask: BigInt) extends TNum {
 
   // Two's complement negation
   def TNEG(): TNumValue = {
-    TNumValue(-this.value & ~this.mask, this.mask)
+    TNumValue(BigInt(0), BigInt(0)).TSUB(this)
   }
 
   // Bitwise Not
@@ -596,7 +598,6 @@ class TNumDomain extends AbstractDomain[Map[Variable, TNum]] {
       case IntLE => tn1.TSLE(tn2)
       case IntGT => tn1.TSGT(tn2)
       case IntGE => tn1.TSGE(tn2)
-      case _ => TNumValue(BigInt(0), BigInt(-1))
     }
   }
 
@@ -805,7 +806,7 @@ class SimplifyKnownBits() {
 
   def applyTransform(procedure: Procedure): Unit = {
     val (beforeIn, afterIn) = solver.solveProc(procedure, backwards = false)
-    util.writeToFile(
+    writeToFile(
       translating.PrettyPrinter.pp_proc_with_analysis_results(beforeIn, afterIn, procedure, x => x.toString),
       s"${procedure.name}_known_bits.il"
     )