chore: normalize directories in tests, add clean results and fixed sc…

…ripts (#856)
opencompl · Nov 15, 2024 · abf2f5a · abf2f5a
1 parent 1694b03
commit abf2f5a
Show file tree

Hide file tree

Showing 29 changed files with 4,464 additions and 13,632 deletions.
diff --git a/bv-evaluation/collect-data-alive.py b/bv-evaluation/collect-data-alive.py
@@ -4,9 +4,10 @@
 import os 
 import re
 
+paper_directory = '../../paper-lean-bitvectors/'
 benchmark_dir = "../SSA/Projects/InstCombine/"
-res_dir = "results/alive-symbolic/"
-raw_data_dir = '../../paper-lean-bitvectors/raw-data/alive-symbolic/'
+res_dir = "results/AliveSymbolic/"
+raw_data_dir = paper_directory + 'raw-data/AliveSymbolic/'
 reps = 1
 
 
@@ -69,7 +70,7 @@ def run():
         out = pd.concat([out, df])
 
     print(out)
-    out.to_csv(raw_data_dir + 'alive_symbolic.csv')
+    out.to_csv(raw_data_dir + 'aliveSymbolic.csv')
 
 if __name__ == "__main__":
     run()

diff --git a/bv-evaluation/collect-data-hdel-symbolic.py b/bv-evaluation/collect-data-hdel-symbolic.py
@@ -4,9 +4,10 @@
 import os 
 import re
 
+paper_directory = '../../paper-lean-bitvectors/'
 benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
 res_dir = "results/HackersDelightSymbolic/"
-raw_data_dir = '../../paper-lean-bitvectors/raw-data/HackersDelight/'
+raw_data_dir = paper_directory + 'raw-data/HackersDelightSymbolic/'
 reps = 1
 
 
@@ -69,7 +70,7 @@ def run():
             out = pd.concat([out, df])
 
     print(out)
-    out.to_csv(raw_data_dir + 'hdel_symbolic.csv')
+    out.to_csv(raw_data_dir + 'hackersDelightSymbolic.csv')
 
 if __name__ == "__main__":
     run()

diff --git a/bv-evaluation/collect-data-hdel.py b/bv-evaluation/collect-data-hdel.py
@@ -3,9 +3,10 @@
 import pandas as pd
 import os 
 
+paper_directory = '../../paper-lean-bitvectors/'
 benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
 res_dir = "results/HackersDelight/"
-raw_data_dir = '../../paper-lean-bitvectors/raw-data/HackersDelight/'
+raw_data_dir = paper_directory + 'raw-data/HackersDelight/'
 reps = 1
 
 bv_width = [4, 8, 16, 32, 64]
@@ -230,3 +231,4 @@
 
         df.to_csv(raw_data_dir+'bvw'+str(bvw)+'_'+file.split('.')[0]+'_proved_data.csv')
         df_ceg.to_csv(raw_data_dir+'bvw'+str(bvw)+'_'+file.split('.')[0]+'_ceg_data.csv')
+        df_err_sorted.to_csv(raw_data_dir+'bvw'+str(bvw)+'_'+file.split('.')[0]+'_err_data.csv')
diff --git a/bv-evaluation/collect-data-llvm-symbolic.py b/bv-evaluation/collect-data-llvm-symbolic.py
@@ -4,9 +4,10 @@
 import os 
 import re
 
+paper_directory = '../../paper-lean-bitvectors/'
 benchmark_dir = "../SSA/Projects/InstCombine/tests/proofs/"
-res_dir = "results/llvm-sym/"
-raw_data_dir = '../../paper-lean-bitvectors/raw-data/instcombine-sym/'
+res_dir = "results/InstCombineSymbolic/"
+raw_data_dir = paper_directory + 'raw-data/InstCombineSymbolic/'
 reps = 1
 
 
@@ -70,7 +71,7 @@ def run():
                 out = pd.concat([out, df])
 
     print(out)
-    out.to_csv(raw_data_dir + 'instcombine_symbolic.csv')
+    out.to_csv(raw_data_dir + 'instcombineSymbolic.csv')
 
 if __name__ == "__main__":
     run()

diff --git a/bv-evaluation/collect-data-llvm.py b/bv-evaluation/collect-data-llvm.py
@@ -3,9 +3,10 @@
 import pandas as pd
 import os 
 
+paper_directory = '../../paper-lean-bitvectors/'
 benchmark_dir = "../SSA/Projects/InstCombine/tests/proofs/"
-res_dir = "results/llvm/"
-raw_data_dir = "raw-data/"
+res_dir = "results/InstCombine/"
+raw_data_dir = paper_directory + "raw-data/InstCombine/"
 
 
 reps = 1

diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-alive-sym.py b/bv-evaluation/compare-leansat-vs-bitwuzla-alive-sym.py
@@ -6,7 +6,7 @@
 
 ROOT_DIR = subprocess.check_output(['git', 'rev-parse', '--show-toplevel']).decode('utf-8').strip()
 
-RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/alive-symbolic/'
+RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/AliveSymbolic/'
 
 BENCHMARK_DIR = ROOT_DIR + '/SSA/Projects/InstCombine/'
 

diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py b/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py
@@ -12,23 +12,23 @@
 
 bv_width = [4, 8, 16, 32, 64]
 
-for file in os.listdir(results_dir):
-    file_path = os.path.join(results_dir, file)
-    try:
-        if os.path.isfile(file_path) or os.path.islink(file_path):
-            os.unlink(file_path)
-        elif os.path.isdir(file_path):
-            shutil.rmtree(file_path)
-    except Exception as e:
-        print('Failed to delete %s. Reason: %s' % (file_path, e))
+# for file in os.listdir(results_dir):
+#     file_path = os.path.join(results_dir, file)
+#     try:
+#         if os.path.isfile(file_path) or os.path.islink(file_path):
+#             os.unlink(file_path)
+#         elif os.path.isdir(file_path):
+#             shutil.rmtree(file_path)
+#     except Exception as e:
+#         print('Failed to delete %s. Reason: %s' % (file_path, e))
 
 for file in os.listdir(benchmark_dir_list):
     print(file)
     for bvw in bv_width:
         subprocess.Popen('sed -i -E \'s/variable \\{x y z : BitVec .+\\}/variable \\{x y z : BitVec '+str(bvw)+'\\}/g\' '+benchmark_dir_list+file, shell=True).wait()
         # replace any sorrys with bv_compare'
-        subprocess.Popen('sed -i -E \'s,all_goals sorry,bv_compare\'\\\'\',g\' '+benchmark_dir_list+file, shell=True).wait()
+        subprocess.Popen('sed -i -E \'s,sorry,bv_compare\'\\\'\',g\' '+benchmark_dir_list+file, shell=True).wait()
         for r in range(reps):
             print(f'cd .. && lake lean '+benchmark_dir+file+' 2>&1 > '+results_dir+file.split(".")[0]+'_'+str(bvw)+'_'+'r'+str(r)+'.txt')
             subprocess.Popen(f'cd .. && lake lean '+benchmark_dir+file+' 2>&1 > '+results_dir+file.split(".")[0]+'_'+str(bvw)+'_'+'r'+str(r)+'.txt', shell=True).wait()
-        subprocess.Popen('sed -i -E \'s,bv_compare\'\\\'\',all_goals sorry,g\' '+benchmark_dir_list+file, shell=True).wait()
+        subprocess.Popen('sed -i -E \'s,bv_compare\'\\\'\',sorry,g\' '+benchmark_dir_list+file, shell=True).wait()
diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm-sym.py
@@ -6,7 +6,7 @@
 
 ROOT_DIR = subprocess.check_output(['git', 'rev-parse', '--show-toplevel']).decode('utf-8').strip()
 
-RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/llvm-bench/'
+RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/InstCombineSymbolic/'
 
 BENCHMARK_DIR = ROOT_DIR + '/SSA/Projects/InstCombine/tests/proofs/'
 

diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py
@@ -6,7 +6,7 @@
 
 ROOT_DIR = subprocess.check_output(['git', 'rev-parse', '--show-toplevel']).decode('utf-8').strip()
 
-RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/llvm/'
+RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/InstCombine/'
 
 BENCHMARK_DIR = ROOT_DIR + '/SSA/Projects/InstCombine/tests/proofs/'