From 48932114d121b5c3e27eb42cdecc92dd9e9b9470 Mon Sep 17 00:00:00 2001
From: zhuyt <zhuyutian57@gmail.com>
Date: Mon, 14 Oct 2024 14:11:06 +0800
Subject: [PATCH] update x.py

---
 README.md |  2 +-
 x.py      | 31 ++++++++++++++-----------------
 2 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/README.md b/README.md
index 52b01b88..703cd83c 100644
--- a/README.md
+++ b/README.md
@@ -96,7 +96,7 @@ We also provide a simple script `x.py`. We can easily to run SELO on a single fi
 ```sh
 ./x.py --run ./benchmark/tests/case_1.c
 ```
-Mor details can be found by `./x.py --help`
+Output of SELO will be stored in `./output/t.log`. More details can be found by `./x.py --help`
 
 ### TODO
 Adjust the script later.
\ No newline at end of file
diff --git a/x.py b/x.py
index c515967a..7aa57e97 100755
--- a/x.py
+++ b/x.py
@@ -20,11 +20,9 @@
 
 
 def compile():
-  os.system(f"cd {selo_build } && cmake --build .")
+  os.system(f"cd {selo_build} && cmake --build .")
 
 def help():
-  os.system(f"{selo} -h")
-
   cmds = {
     "--compile" : ('',"Compile esbmc"),
     "--run" : ("file extra_args","Only test a single file 'file'"),
@@ -35,10 +33,11 @@ def help():
   args = {
     "--esbmc" : "Disable SLHV and use default esbmc with solver Z3",
     "--debug" : "Output debug info of SLHV",
-    "--std-out" : "Output info in std::out"
+    "--std-out" : "Output info in std::out",
+    "--vcc" : "Save VCC in output",
   }
 
-  print("Commands for x.py:")
+  print("Args for x.py:")
   for cmd in cmds.items():
     cmdline = [cmd[0] + ' ' + cmd[1][0], cmd[1][1]]
     print(" {:<35} {:<50}".format(*cmdline))
@@ -58,8 +57,6 @@ def collect_one_assert(info, aht):
     res["Line"] = location[4]
     res["Column"] = location[6]
 
-
-
   # Property
   prt = info[2].split(" ")
   res["Property"] = prt[1]
@@ -112,7 +109,6 @@ def run_on(cprog, extra_args):
   cprog_name = os.path.basename(cprog)
   print(f"Verifying program: {cprog_name}")
 
-  # TODO: add more extra args
   args = [
     selo,
     cprog,
@@ -120,9 +116,6 @@ def run_on(cprog, extra_args):
     "--force-malloc-success",
     "--memory-leak-check",
     "--result-only",
-    "--show-vcc",
-    "--output",
-    vcc_log,
     "--multi-property",
   ]
 
@@ -130,6 +123,9 @@ def run_on(cprog, extra_args):
     args.append("--z3")
   else:
     args.append("--z3-slhv")
+  
+  if "--vcc" in extra_args:
+    args += ["--show-vcc", "--output", vcc_log]
 
   if "--debug" in extra_args:
     args.append("--verbosity SLHV:8")
@@ -151,6 +147,11 @@ def run_on(cprog, extra_args):
   return result
 
 def collect_results(cprog):
+  if not os.path.exists(log_root):
+    os.mkdir(log_root)
+  if not os.path.exists(vcc_log):  
+    os.mkdir(vcc_root)
+
   cprog_name = cprog.split('.')[0]
 
   log_file = cprog_name + "_log.log"
@@ -320,7 +321,7 @@ def run_expriment_on(benchmark_root, extra_args):
   results = {}
   for cprog in cprogs:
     cprog_path = os.path.join(benchmark_root, cprog)
-    results[cprog] = run_on(cprog_path, extra_args)
+    results[cprog] = run_on(cprog_path, extra_args + ["--vcc"])
     collect_results(cprog)
 
   generate_csv(results)
@@ -330,14 +331,10 @@ def run_expriment_on(benchmark_root, extra_args):
 if __name__ == '__main__':
   if not os.path.exists(output_root):
     os.mkdir(output_root)
-  if not os.path.exists(log_root):
-    os.mkdir(log_root)
-  if not os.path.exists(vcc_log):  
-    os.mkdir(vcc_root)
 
   if "--esbmc" in sys.argv:
     csv_file = os.path.join(output_root, "results_esbmc.csv")
-  
+
   if sys.argv[1] == "--compile":
     compile()
   elif sys.argv[1] == "--run":