chore: clean up folders

agurfinkel · Jan 10, 2024 · 868af7e · 868af7e
1 parent 5293e5f
commit 868af7e
Show file tree

Hide file tree

Showing 18 changed files with 22 additions and 17 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -34,10 +34,10 @@ add_definitions(${LLVM_DEFINITIONS})
 add_subdirectory(include)
 add_subdirectory(lib)
 add_subdirectory(test)
-add_subdirectory(cex)
-add_subdirectory(btor2mlir-opt)
-add_subdirectory(btor2mlir-translate)
-add_subdirectory(smt2mlir-opt)
-add_subdirectory(smt2mlir-translate)
+add_subdirectory(utils/cex)
+add_subdirectory(tools/btor2mlir-opt)
+add_subdirectory(tools/btor2mlir-translate)
+add_subdirectory(tools/smt2mlir-opt)
+add_subdirectory(tools/smt2mlir-translate)
 add_subdirectory(crab2mlir-opt)
 add_subdirectory(crab2mlir-translate)
diff --git a/README.md b/README.md
@@ -36,15 +36,15 @@ Using the command `build/bin/btor2mlir-translate --import-btor counter.btor2 > c
 ```mlir
 module {
   func @main() {
-    %0 = btor.constant 0 : i4
-    br ^bb1(%0 : i4)
-  ^bb1(%1: i4):  // 2 preds: ^bb0, ^bb1
-    %2 = btor.constant 1 : i4
-    %3 = btor.add %1, %2 : i4
-    %4 = btor.constant -1 : i4
-    %5 = btor.cmp eq, %1, %4 : i4
-    btor.assert_not(%5)
-    br ^bb1(%3 : i4)
+    %0 = btor.constant 0 : i4 !btor.bv<4>
+    br ^bb1(%0 : !btor.bv<4>)
+  ^bb1(%1: !btor.bv<4>):  // 2 preds: ^bb0, ^bb1
+    %2 = btor.constant 1 : i4 !btor.bv<4>
+    %3 = btor.add %1, %2 : !btor.bv<4>
+    %4 = btor.constant -1 : i4 !btor.bv<4>
+    %5 = btor.cmp eq, %1, %4 : !btor.bv<4>
+    btor.assert_not(%5), 0 : i64 !btor.bv<1>
+    br ^bb1(%3 : !btor.bv<4>)
   }
 }
 ```
@@ -54,6 +54,7 @@ Then, using the command  `build/bin/btor2mlir-opt  --convert-std-to-llvm --conve
 ```mlir
 module attributes {llvm.data_layout = ""} {
   llvm.func @__VERIFIER_error()
+  llvm.func @__VERIFIER_assert(i1, i64)
   llvm.func @main() {
     %0 = llvm.mlir.constant(0 : i4) : i4
     llvm.br ^bb1(%0 : i4)
@@ -68,6 +69,8 @@ module attributes {llvm.data_layout = ""} {
   ^bb2:  // pred: ^bb1
     llvm.br ^bb1(%3 : i4)
   ^bb3:  // pred: ^bb1
+    %8 = llvm.mlir.constant(0 : i64) : i64
+    llvm.call @__VERIFIER_assert(%7, %8) : (i1, i64) -> ()
     llvm.call @__VERIFIER_error() : () -> ()
     llvm.unreachable
   }
@@ -78,6 +81,7 @@ Finally, using the command `build/bin/btor2mlir-translate --mlir-to-llvmir count
 
 ```llvm
 declare void @__VERIFIER_error()
+declare void @__VERIFIER_assert(i1, i64)
 define void @main() !dbg !3 {
   br label %1, !dbg !7
 1:                                                ; preds = %6, %0
@@ -89,16 +93,17 @@ define void @main() !dbg !3 {
 6:                                                ; preds = %1
   br label %1, !dbg !13
 7:                                                ; preds = %1
-  call void @__VERIFIER_error(), !dbg !14
-  unreachable, !dbg !15
+  call void @__VERIFIER_assert(i1 %5, i64 0), !dbg !14
+  call void @__VERIFIER_error(), !dbg !15
+  unreachable, !dbg !16
 }
 ```
 
 If you have SeaHorn installed locally (a distribution is included in the Docker), we can show that the bad state in the original circuit is reached using SeaHorn's Bounded Model Checking engine. This is indicated by the output **sat** when we run the command: `sea bpf counter.ll`
 
 ## Witness Generation
 
-Run the shell script [`./get_cex_seahorn.sh $btor2_file`](cex/witness/get_cex_seahorn.sh) to:
+Run the shell script [`./get_cex_seahorn.sh $btor2_file`](utils/cex/witness/get_cex_seahorn.sh) to:
 
 a) extract a counter example from SeaHorn \
 b) generate a Btor2 Witness \

diff --git a/btor2mlir-opt/CMakeLists.txt → tools/btor2mlir-opt/CMakeLists.txt b/btor2mlir-opt/CMakeLists.txt → tools/btor2mlir-opt/CMakeLists.txt
diff --git a/btor2mlir-opt/btor2mlir-opt.cpp → tools/btor2mlir-opt/btor2mlir-opt.cpp b/btor2mlir-opt/btor2mlir-opt.cpp → tools/btor2mlir-opt/btor2mlir-opt.cpp
diff --git a/btor2mlir-translate/CMakeLists.txt → tools/btor2mlir-translate/CMakeLists.txt b/btor2mlir-translate/CMakeLists.txt → tools/btor2mlir-translate/CMakeLists.txt
diff --git a/btor2mlir-translate/btor2mlir-translate.cpp → ...or2mlir-translate/btor2mlir-translate.cpp b/btor2mlir-translate/btor2mlir-translate.cpp → ...or2mlir-translate/btor2mlir-translate.cpp
diff --git a/smt2mlir-opt/CMakeLists.txt → tools/smt2mlir-opt/CMakeLists.txt b/smt2mlir-opt/CMakeLists.txt → tools/smt2mlir-opt/CMakeLists.txt
diff --git a/smt2mlir-opt/smt2mlir-opt.cpp → tools/smt2mlir-opt/smt2mlir-opt.cpp b/smt2mlir-opt/smt2mlir-opt.cpp → tools/smt2mlir-opt/smt2mlir-opt.cpp
diff --git a/smt2mlir-translate/CMakeLists.txt → tools/smt2mlir-translate/CMakeLists.txt b/smt2mlir-translate/CMakeLists.txt → tools/smt2mlir-translate/CMakeLists.txt
diff --git a/smt2mlir-translate/smt2mlir-translate.cpp → ...smt2mlir-translate/smt2mlir-translate.cpp b/smt2mlir-translate/smt2mlir-translate.cpp → ...smt2mlir-translate/smt2mlir-translate.cpp
diff --git a/cex/CMakeLists.txt → utils/cex/CMakeLists.txt b/cex/CMakeLists.txt → utils/cex/CMakeLists.txt
diff --git a/cex/cex.cpp → utils/cex/cex.cpp b/cex/cex.cpp → utils/cex/cex.cpp
diff --git a/cex/cex.h → utils/cex/cex.h b/cex/cex.h → utils/cex/cex.h
diff --git a/cex/witness/configs/sea-cex.yaml → utils/cex/witness/configs/sea-cex.yaml b/cex/witness/configs/sea-cex.yaml → utils/cex/witness/configs/sea-cex.yaml
diff --git a/cex/witness/configs/sea-vac.yaml → utils/cex/witness/configs/sea-vac.yaml b/cex/witness/configs/sea-vac.yaml → utils/cex/witness/configs/sea-vac.yaml
diff --git a/cex/witness/configs/sea.yaml → utils/cex/witness/configs/sea.yaml b/cex/witness/configs/sea.yaml → utils/cex/witness/configs/sea.yaml
diff --git a/cex/witness/get_cex_seahorn.sh → utils/cex/witness/get_cex_seahorn.sh b/cex/witness/get_cex_seahorn.sh → utils/cex/witness/get_cex_seahorn.sh
diff --git a/cex/witness/witness_generator.py → utils/cex/witness/witness_generator.py b/cex/witness/witness_generator.py → utils/cex/witness/witness_generator.py