Bug fix2 (Generative-Program-Analysis#26)

* removed quoted string case in label identifier (for sha256sum) * not generate block when isConc has IntV * implement IEEE floating point visitor * added floating point test * minor fix * added fp80 benchmark
mkhan45 · Jan 13, 2022 · 8eb28cb · 8eb28cb
1 parent e8bfa0c
commit 8eb28cb
Show file tree

Hide file tree

Showing 9 changed files with 1,504 additions and 1,481 deletions.
diff --git a/dev-clean/benchmarks/llvm/floatFp80.c b/dev-clean/benchmarks/llvm/floatFp80.c
@@ -0,0 +1,10 @@
+int main()
+{
+  long double a = 0x1e1;
+  long double b = 0x1e2;
+  long double c = 0x1e3;
+  sym_print(a);
+  sym_print(b);
+  sym_print(c);
+  return 0;
+}
diff --git a/dev-clean/grammar/LLVMLexer.g4 b/dev-clean/grammar/LLVMLexer.g4
@@ -649,5 +649,5 @@ LOCAL_ID
 
 LABEL_IDENT
     : ( LETTER | DECIMAL_DIGIT ) ( LETTER | DECIMAL_DIGIT ) * ':'
-    | QUOTED_STRING ':'
+    /* | QUOTED_STRING ':' */
 ;
diff --git a/dev-clean/grammar/Makefile b/dev-clean/grammar/Makefile
@@ -2,6 +2,6 @@ all:
 	./generate.sh
 
 clean:
-	rm *.java
-	rm *.interp
-	rm *.tokens
+	rm -f *.java
+	rm -f *.interp
+	rm -f *.tokens
diff --git a/dev-clean/src/main/java/LLVMLexer.java b/dev-clean/src/main/java/LLVMLexer.java
diff --git a/dev-clean/src/main/scala/sai/lang/LLVM.scala b/dev-clean/src/main/scala/sai/lang/LLVM.scala
@@ -179,6 +179,7 @@ package IR {
 
   abstract class FloatKind extends LAST
   case object FK_Half extends FloatKind
+  case object FK_BFloat extends FloatKind
   case object FK_Float extends FloatKind
   case object FK_Double extends FloatKind
   case object FK_X86_FP80 extends FloatKind
@@ -792,10 +793,9 @@ class MyVisitor extends LLVMParserBaseVisitor[LAST] {
     val floatStr = ctx.FLOAT_LIT.getText
     if (floatStr.contains('.')) FloatConst(floatStr.toFloat)
     else if (floatStr.startsWith("0x")) {
-      // Does not work, need to parse "0x3FF4CCCCC0000000" as 1.3
-      // val i = java.lang.Long.parseLong(floatStr.substring(2), 16)
-      // FloatConst(java.lang.Float.intBitsToFloat(i.intValue()))
-      ???
+      val hexString = floatStr.substring(2)
+      val longBits = java.lang.Long.parseUnsignedLong(hexString, 16)
+      FloatConst(java.lang.Double.longBitsToDouble(longBits).asInstanceOf[Float])
     } 
     else ???
   }

diff --git a/dev-clean/src/main/scala/sai/llsc/EngineBase.scala b/dev-clean/src/main/scala/sai/llsc/EngineBase.scala
@@ -91,6 +91,18 @@ trait EngineBase extends SAIOps { self: BasicDefs with ValueDefs =>
       (size + BYTE_SIZE - 1) / BYTE_SIZE
     case PtrType(ty, addrSpace) =>
       ARCH_WORD_SIZE / BYTE_SIZE
+    case FloatType(fk) => {
+      val rawSize = fk match {
+        case FK_Half => 16
+        case FK_BFloat => 16
+        case FK_Float => 32
+        case FK_Double => 64
+        case FK_X86_FP80 => 80
+        case FK_FP128 => 128
+        case FK_PPC_FP1289 => 128
+      }
+      (rawSize + BYTE_SIZE - 1) / BYTE_SIZE
+    }
     case _ => ???
   }
 

diff --git a/dev-clean/src/main/scala/sai/llsc/states/GenericDefs.scala b/dev-clean/src/main/scala/sai/llsc/states/GenericDefs.scala
@@ -212,7 +212,10 @@ trait ValueDefs { self: SAIOps with BasicDefs =>
     def bv_sext(bw: Rep[Int]): Rep[Value] =  "bv_sext".reflectWith[Value](v, bw)
     def bv_zext(bw: Rep[Int]): Rep[Value] =  "bv_zext".reflectWith[Value](v, bw)
 
-    def isConc: Rep[Boolean] = "is-conc".reflectWith[Boolean](v)
+    def isConc: Rep[Boolean] = v match {
+      case IntV(_, _) => unit(true)
+      case _ => "is-conc".reflectWith[Boolean](v)
+    }
     def toSMTBool: Rep[SMTBool] = "to-SMT".reflectWith[SMTBool](v)
     def toSMTBoolNeg: Rep[SMTBool] = "to-SMTNeg".reflectWith[SMTBool](v)
 

diff --git a/dev-clean/src/main/scala/sai/prototypes/llvm/Benchmarks.scala b/dev-clean/src/main/scala/sai/prototypes/llvm/Benchmarks.scala
@@ -41,6 +41,7 @@ object Benchmarks {
   lazy val varArgInt = parseFile("benchmarks/llvm/varArgInt.ll")
   lazy val trunc = parseFile("benchmarks/llvm/trunc.ll")
   lazy val floatArith = parseFile("benchmarks/llvm/floatArith.ll")
+  lazy val floatFp80 = parseFile("benchmarks/llvm/floatFp80.ll")
 
   lazy val runCommandLine = parseFile("benchmarks/llvm/runCommandLine.ll")
 

diff --git a/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala b/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala
@@ -31,6 +31,9 @@ object TestCases {
     TestPrg(ptrpred, "ptrPredTest", "@main", 0, 1),
     TestPrg(switchTestConc, "switchConcreteTest", "@main", 0, 1),
     TestPrg(trunc, "truncTest", "@main", 0, 1),
+    TestPrg(floatArith, "floatArithTest", "@main", 0, 1),
+    // FIXME: Support parsing fp80 literals <2022-01-12, David Deng> //
+    // TestPrg(floatFp80, "floatFp80Test", "@main", 0, 1),
 
     TestPrg(arrayAccess, "arrayAccTest", "@main", 0, 1),
     TestPrg(arrayAccessLocal, "arrayAccLocalTest", "@main", 0, 1),
@@ -84,8 +87,6 @@ object TestCases {
   // TestPrg(largeStackArray, "largeStackArrayTest", "@main", 0, 1),
   // TestPrg(makeSymbolicArray, "makeSymbolicArrayTest", "@main", 0, 1),
   // TestPrg(ptrtoint, "ptrToIntTest", "@main", 0, 1)
-  // FIXME: parsing error
-  // TestPrg(floatArith, "floatArithTest", "@main", 0, 1),
 }
 
 import TestCases._