bench/ce-stats.py

   1 #!/usr/bin/env python
   2
   3 # Helper script to compute statistics about checking counterexamples.
   4
   5 # The script creates 4 files:
   6 # - [export_file_raw], a CSV file with columns date / file / prover /
   7 #   verdict / concrete_RAC / abstract_RAC for each CE that is checked
   8 # - [export_file], the same data aggregated according to the verdict
   9 # - [export_file_incomplete_small_step], only the data corresponding
  10 #   to incomplete verdicts, grouped by small-step RAC result
  11 # - [export_file_incomplete_giant_step], only the data corresponding
  12 #   to incomplete verdicts, grouped by giant-step RAC result
  13
  14 from datetime import date
  15 import os
  16 import pandas as pd
  17 import re
  18
  19 dir = "./bench/check-ce/oracles"
  20 export_file_raw = "./data_raw.csv"
  21 export_file = "./data.csv"
  22 export_file_incomplete_small_step = "./data_incomplete_small_step.csv"
  23 export_file_incomplete_giant_step = "./data_incomplete_giant_step.csv"
  24
  25 rx_model = re.compile(r"Selected model [0|1]: (?P<v>[A-Z_]*)\n")
  26 rx_concrete_RAC = re.compile(r"Concrete RAC: (?P<c>[A-Z_]*)(?P<cr>.*)\n")
  27 rx_abstract_RAC = re.compile(r"Abstract RAC: (?P<a>[A-Z_]*)(?P<ar>.*)\n")
  28
  29 rx_dict_incomplete = {
  30     "cannot decide": re.compile(r"(.*)cannot be evaluated(.*)"),
  31     "cannot import": re.compile(r"(.*)cannot import value(.*)"),
  32     "missing return value": re.compile(r"(.*)missing value for return value(.*)"),
  33     "many args for exec": re.compile(r"(.*)many args for exec fun(.*)"),
  34     "uncaught exception": re.compile(r"(.*)uncaught exception(.*)"),
  35     "undefined argument": re.compile(r"(.*)undefined argument(.*)"),
  36 }
  37 list_of_verdicts = [
  38     "INCOMPLETE",
  39     "NC",
  40     "BAD_CE",
  41     "NC_SW",
  42     "SW",
  43 ]
  44
  45 rx_filepath = re.compile(r"bench/check-ce/oracles/(?P<f>[a-zA-Z0-9-_]*)_(?P<p>[a-zA-Z0-9,.\-]*)_[W|S]P.oracle")
  46
  47 def _parse_line(line,rx):
  48     match = rx.search(line)
  49     if match:
  50         return match
  51     return None
  52
  53 def _parse_reason(reason, rx_dict):
  54     for key, rx in rx_dict.items():
  55         match = rx.search(reason)
  56         if match:
  57             return key
  58     print ("WARNING! Unknown reason: " + reason)
  59     return reason
  60
  61 def _add_reason(res, reason, rx_dict):
  62     if res in ["FAILURE", "NORMAL", "STUCK"]:
  63         return res
  64     elif res in ["INCOMPLETE"]:
  65         return (res + " " + _parse_reason(reason, rx_dict))
  66     else:
  67         print("WARNING! Unknown RAC result: " + res)
  68         return res
  69
  70
  71 def parse_file(filepath, data, date):
  72     print("entering parse_file with filepath=" + filepath)
  73     with open(filepath, "r") as file_object:
  74         filepath = _parse_line(filepath,rx_filepath)
  75         if filepath is not None:
  76             file = filepath.group("f")
  77             prover = filepath.group("p")
  78             line = file_object.readline()
  79         else:
  80             print("WARNING! Could not parse filepath")
  81         while line:
  82             match = _parse_line(line,rx_model)
  83             if match is not None:
  84                 verdict = match.group("v")
  85                 line = file_object.readline()
  86                 match_concrete = _parse_line(line,rx_concrete_RAC)
  87                 line = file_object.readline()
  88                 match_abstract = _parse_line(line,rx_abstract_RAC)
  89                 if (match_concrete is not None) & (match_abstract is not None):
  90                     concrete_RAC = match_concrete.group("c")
  91                     reason_concrete = match_concrete.group("cr")
  92                     abstract_RAC = match_abstract.group("a")
  93                     reason_abstract = match_abstract.group("ar")
  94                     if verdict in list_of_verdicts:
  95                         concrete_RAC = _add_reason(concrete_RAC, reason_concrete, rx_dict_incomplete)
  96                         abstract_RAC = _add_reason(abstract_RAC, reason_abstract, rx_dict_incomplete)
  97                     else:
  98                         print("WARNING! Unknown verdict: " + verdict)
  99                     data.append(
 100                         {
 101                             "date": date,
 102                             "file": file,
 103                             "prover": prover,
 104                             "verdict": verdict,
 105                             "concrete_RAC": concrete_RAC,
 106                             "abstract_RAC": abstract_RAC,
 107                         }
 108                     )
 109             line = file_object.readline()
 110
 111 data = []
 112 date = date.today()
 113 print(date)
 114 for filename in os.listdir(dir):
 115     f = os.path.join(dir, filename)
 116     if os.path.isfile(f):
 117         if f.endswith(".oracle"):
 118             parse_file(f, data, date.strftime("%Y%m%d"))
 119 data = pd.DataFrame(data)
 120 data.to_csv(export_file_raw, mode="w", header=True)
 121
 122 agg_data = data.groupby("date")["verdict"].value_counts().rename("nb")
 123 agg_data = pd.DataFrame(agg_data)
 124 agg_data.to_csv(export_file, mode="w", header=True)
 125
 126 agg_data_incomplete_small_step = data.query('verdict == "INCOMPLETE"').groupby("date")["concrete_RAC"].value_counts().rename("nb")
 127 agg_data_incomplete_small_step = pd.DataFrame(agg_data_incomplete_small_step)
 128 agg_data_incomplete_small_step.to_csv(export_file_incomplete_small_step, mode="w", header=True)
 129
 130 agg_data_incomplete_giant_step = data.query('verdict == "INCOMPLETE"').groupby("date")["abstract_RAC"].value_counts().rename("nb")
 131 agg_data_incomplete_giant_step = pd.DataFrame(agg_data_incomplete_giant_step)
 132 agg_data_incomplete_giant_step.to_csv(export_file_incomplete_giant_step, mode="w", header=True)