Updated library

subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.cpp

@@ -10,6 +10,10 @@ std::unordered_map<llvm::BasicBlock *, std::shared_ptr < BasicBlock>>
 BasicBlock::LUT = std::unordered_map < llvm::BasicBlock *, std::shared_ptr<BasicBlock>>
 ();
 
+void BasicBlock::reset() {
+    LUT = std::unordered_map < llvm::BasicBlock *, std::shared_ptr<BasicBlock>>();
+}
+
 void BasicBlock::init() {
     initialized = true;
     numOfInstructions = 0;

subprojects/frontends/llvm/src/main/cpp/types/BasicBlock.h

@@ -32,6 +32,8 @@ class BasicBlock {
         }
     }
 
+    static void reset();
+
     void init();
 
     int getNumOfInstructions() { return numOfInstructions; }

subprojects/frontends/llvm/src/main/cpp/types/Module.cpp

@@ -56,6 +56,11 @@ Module::Module() {
 }
 
 void Module::parseLLVMModule(std::shared_ptr <llvm::Module> llvmModule) {
+    instance = Module();
+    Analysis::reset();
+    BasicBlock::reset();
+    Register::reset();
+
     // Analyze module first
     Analysis::checkModule(llvmModule.get());
 

subprojects/frontends/llvm/src/main/cpp/types/Module.h

@@ -10,6 +10,8 @@
 #include <iostream>
 #include "Function.h"
 #include "BasicBlock.h"
+#include "operands/Register.h"
+#include "../utilities/Analysis.h"
 #include "GlobalVariable.h"
 
 // Global context

subprojects/frontends/llvm/src/main/cpp/types/operands/Register.cpp

@@ -8,6 +8,10 @@ std::unordered_map<llvm::Value *, std::shared_ptr < Register>>
 Register::LUT = std::unordered_map < llvm::Value *, std::shared_ptr<Register>>
 ();
 
+void Register::reset() {
+    LUT = std::unordered_map < llvm::Value *, std::shared_ptr<Register>>();
+}
+
 Register::Register(llvm::Value &llvmRegister) {
     if(llvmRegister.getName() == "") name = "register_" + std::to_string(nameCounter);
     else {

subprojects/frontends/llvm/src/main/cpp/types/operands/Register.h

@@ -67,6 +67,8 @@ class Register : public Operand {
         }
     }
 
+    static void reset();
+
     static std::shared_ptr <Register> findRegister(llvm::Value *key);
 };
 

subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.cpp

@@ -96,4 +96,9 @@ bool Analysis::checkIfAndOrXor(const llvm::BinaryOperator *binOp) {
     if(opname=="or") return true;
     if(opname=="xor") return true;
     return false;
-}
+}
+
+void Analysis::reset() {
+//    hasIntInBitwiseBinaryOp = false;
+//    hasStructs = false;
+}

subprojects/frontends/llvm/src/main/cpp/utilities/Analysis.h

@@ -26,6 +26,7 @@ class Analysis {
 public:
     static void checkInstruction(llvm::Instruction* instruction); // when parsing, every instruction should be checked with this
     static void checkModule(const llvm::Module*); // before parsing module, this should be called on it
+    static void reset();
 
     static bool getStructAnalysisResult() {
         return hasStructs;

subprojects/xcfa/llvm2xcfa/src/test/java/hu/bme/mit/theta/llvm2xcfa/TestLlvm2Xcfa.kt

@@ -41,6 +41,32 @@ class TestLlvm2Xcfa {
                 arrayOf("/c/example_struct.c"),
                 arrayOf("/c/example_void_func.c"),
                 arrayOf("/c/test_locks_14-2.c"),
+
+                arrayOf("/c/dekker.i"),
+                arrayOf("/c/00assignment.c"),
+//                    arrayOf("/c/01cast.c"),
+                arrayOf("/c/02types.c"),
+                arrayOf("/c/03bitwise.c"),
+//                    arrayOf("/c/04real.c"),
+//                    arrayOf("/c/05math.c"),
+                arrayOf("/c/06arrays.c"),
+                arrayOf("/c/07arrayinit.c"),
+                arrayOf("/c/08vararray.c"),
+//                    arrayOf("/c/09struct.c"),
+                arrayOf("/c/10ptr.c"),
+                arrayOf("/c/11ptrs.c"),
+                arrayOf("/c/12ptrtypes.c"),
+                arrayOf("/c/13typedef.c"),
+                arrayOf("/c/14ushort.c"),
+                arrayOf("/c/15addition.c"),
+                arrayOf("/c/16loop.c"),
+//                    arrayOf("/c/17recursive.c"),
+                arrayOf("/c/18multithread.c"),
+                arrayOf("/c/19dportest.c"),
+                arrayOf("/c/20testinline.c"),
+                arrayOf("/c/21namecollision.c"),
+//                    arrayOf("/c/22nondet.c"),
+                arrayOf("/c/23overflow.c"),
             )
         }
 

subprojects/xcfa/llvm2xcfa/src/test/resources/c/00assignment.c

@@ -0,0 +1,5 @@
+void reach_error(){}
+int main() {
+    int a = 1;
+    if(a) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/01cast.c

@@ -0,0 +1,6 @@
+void reach_error(){}
+int __VERIFIER_nondet();
+int main() {
+    int a = __VERIFIER_nondet();
+    if(((char)a) != 0) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/02types.c

@@ -0,0 +1,15 @@
+void reach_error(){}
+int main() {
+    _Bool a;
+    unsigned char uc;
+    signed char c;
+    unsigned short us;
+    short s;
+    unsigned int ui;
+    int i;
+    unsigned long ul;
+    long l;
+    unsigned long long ull;
+    long long ll;
+    if(a+uc+c+us+s+ui+i+ul+l+ull+ll) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/03bitwise.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+int __VERIFIER_nondet_int();
+int main() {
+    int a = __VERIFIER_nondet_int();
+    a = a | 0;
+    if(a == -10) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/04real.c

@@ -0,0 +1,8 @@
+void reach_error(){}
+extern float __VERIFIER_nondet_float();
+int main() {
+    float f = __VERIFIER_nondet_float();
+    double d = f;
+    long double ld = d;
+    if(ld > 0.28f && ld < 0.32f) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/05math.c

@@ -0,0 +1,22 @@
+void reach_error(){}
+float fabs(float);
+float floor(float);
+float round(float);
+float fmax(float, float);
+float fmin(float, float);
+float sqrt(float);
+int isnan(float);
+
+int main() {
+    float f = 12.65f;
+    float f1 = fabs(f);
+    float f2 = floor(f);
+    float f3 = round(f);
+    float f4 = fmax(f2, f3);
+    float f5 = fmin(f2, f3);
+    float f6 = sqrt(f);
+    float f7 = isnan(f);
+    f = 0.0f;
+    float f8 = isnan(0.0f/0.0f);
+    if(f8) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/06arrays.c

@@ -0,0 +1,8 @@
+void reach_error(){}
+
+int main() {
+    int a[2], b[3];
+    a[0] = 12;
+    b[3] = a[0];
+    if(b[3] > 11) reach_error();
+}

subprojects/xcfa/llvm2xcfa/src/test/resources/c/07arrayinit.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+
+int main() {
+    int x;
+    int a[3] = {2, x+1, 4};
+    if(a[1] > 2) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/08vararray.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+
+int main() {
+    int x;
+    int a[3] = {1, 2, 3};
+    if(a[x] == 2) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/09struct.c

@@ -0,0 +1,16 @@
+void reach_error(){}
+
+struct A{
+    int a;
+    char c;
+    struct {
+        int a;
+    } b;
+};
+
+int main() {
+    struct A a;
+    a.a = 3;
+    a.c = 1;
+    if(a.a + a.c + a.b.a < 4) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/10ptr.c

@@ -0,0 +1,13 @@
+void reach_error(){}
+
+int main() {
+    int a = 110;
+    int *b = &a;
+    char *c = (char*)b;
+    a = 90;
+    char d = *c;
+    if(d > 100) reach_error();
+    *b = 120;
+    d = *c;
+    if(d > 100) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/11ptrs.c

@@ -0,0 +1,12 @@
+void reach_error(){}
+
+void check_geq_110(int* param) {
+    if(*param >= 110) reach_error();
+}
+
+int main() {
+    int a = 100, b = 110, c = 120;
+    check_geq_110(&a);
+    check_geq_110(&b);
+    check_geq_110(&c);
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/12ptrtypes.c

@@ -0,0 +1,11 @@
+void reach_error(){}
+
+void check_geq_110(void* param) {
+    if(*(unsigned int*)param <= 110) reach_error();
+}
+
+int main() {
+    float f = 0.3f;
+    unsigned int all = -1;
+    check_geq_110(&all);
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/13typedef.c

@@ -0,0 +1,8 @@
+void reach_error(){}
+
+
+char char1;
+int main() {
+    char char2;
+    if(char1 + char2 > 256) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/14ushort.c

@@ -0,0 +1,10 @@
+void reach_error(){}
+
+extern unsigned short __VERIFIER_nondet_ushort();
+
+int main() {
+    short ush;
+    long c;
+    ush = __VERIFIER_nondet_ushort();
+    if(ush) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/15addition.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+
+int main() {
+    int z = 6;
+    int y = 1;
+    if((z*z) - 12 * y - 6 * z + 12 == 0) reach_error();
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/16loop.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+
+int main() {
+    for(int i = 0; i < 30; i++) {
+        if(i == 28) reach_error();
+    }
+ }

subprojects/xcfa/llvm2xcfa/src/test/resources/c/17recursive.c

@@ -0,0 +1,11 @@
+void reach_error(){}
+
+int fibonacci(int i) {
+    if(i == 0) return 0;
+    else if(i == 1) return 1;
+    else return fibonacci(i-1) + fibonacci(i-2);
+}
+
+int main() {
+    if(fibonacci(8) != 21) reach_error();
+}