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 post": re.compile(r"(.*)Postcondition of (.*) cannot be evaluated(.*)"),
  31     "cannot decide pre": re.compile(r"(.*)Precondition of (.*) cannot be evaluated(.*)"),
  32     "cannot decide": re.compile(r"(.*)cannot be evaluated(.*)"),
  33     "cannot import": re.compile(r"(.*)cannot import value(.*)"),
  34     "cannot evaluate builtin": re.compile(r"(.*)cannot evaluate builtin(.*)"),
  35     "missing return value": re.compile(r"(.*)missing value for return value(.*)"),
  36     "many args for exec": re.compile(r"(.*)many args for exec fun(.*)"),
  37     "uncaught exception": re.compile(r"(.*)uncaught exception(.*)"),
  38     "undefined argument": re.compile(r"(.*)undefined argument(.*)"),
  39     "unexpected arguments": re.compile(r"(.*)unexpected arguments(.*)"),
  40     "missing global": re.compile(r"(.*)missing value for global(.*)"),
  41 }
  42 list_of_verdicts = [
  43     "INCOMPLETE",
  44     "NC",
  45     "BAD_CE",
  46     "NC_SW",
  47     "SW",
  48 ]
  49
  50 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")
  51
  52 def _parse_line(line,rx):
  53     match = rx.search(line)
  54     if match:
  55         return match
  56     return None
  57
  58 def _parse_reason(reason, rx_dict):
  59     for key, rx in rx_dict.items():
  60         match = rx.search(reason)
  61         if match:
  62             return key
  63     print ("WARNING! Unknown reason: " + reason)
  64     return reason
  65
  66 def _add_reason(res, reason, rx_dict):
  67     if res in ["FAILURE", "NORMAL", "STUCK"]:
  68         return res
  69     elif res in ["INCOMPLETE"]:
  70         return (res + " " + _parse_reason(reason, rx_dict))
  71     else:
  72         print("WARNING! Unknown RAC result: " + res)
  73         return res
  74
  75
  76 def parse_file(filepath, data, date):
  77     # print("entering parse_file with filepath=" + filepath)
  78     with open(filepath, "r") as file_object:
  79         filepath = _parse_line(filepath,rx_filepath)
  80         if filepath is not None:
  81             file = filepath.group("f")
  82             prover = filepath.group("p")
  83             line = file_object.readline()
  84         else:
  85             print("WARNING! Could not parse filepath")
  86         while line:
  87             match = _parse_line(line,rx_model)
  88             if match is not None:
  89                 verdict = match.group("v")
  90                 line = file_object.readline()
  91                 match_concrete = _parse_line(line,rx_concrete_RAC)
  92                 line = file_object.readline()
  93                 match_abstract = _parse_line(line,rx_abstract_RAC)
  94                 if (match_concrete is not None) & (match_abstract is not None):
  95                     concrete_RAC = match_concrete.group("c")
  96                     reason_concrete = match_concrete.group("cr")
  97                     abstract_RAC = match_abstract.group("a")
  98                     reason_abstract = match_abstract.group("ar")
  99                     if verdict in list_of_verdicts:
 100                         concrete_RAC = _add_reason(concrete_RAC, reason_concrete, rx_dict_incomplete)
 101                         abstract_RAC = _add_reason(abstract_RAC, reason_abstract, rx_dict_incomplete)
 102                     else:
 103                         print("WARNING! Unknown verdict: " + verdict)
 104                     data.append(
 105                         {
 106                             "date": date,
 107                             "file": file,
 108                             "prover": prover,
 109                             "verdict": verdict,
 110                             "concrete_RAC": concrete_RAC,
 111                             "abstract_RAC": abstract_RAC,
 112                         }
 113                     )
 114             line = file_object.readline()
 115
 116 data = []
 117 date = date.today()
 118 print(date)
 119 for filename in os.listdir(dir):
 120     f = os.path.join(dir, filename)
 121     if os.path.isfile(f):
 122         if f.endswith(".oracle"):
 123             parse_file(f, data, date.strftime("%Y%m%d"))
 124 data = pd.DataFrame(data)
 125 data.to_csv(export_file_raw, mode="w", header=True)
 126
 127 agg_data = data.groupby("date")["verdict"].value_counts().rename("nb")
 128 agg_data = pd.DataFrame(agg_data)
 129 agg_data.to_csv(export_file, mode="w", header=True)
 130
 131 agg_data_incomplete_small_step = data.query('verdict == "INCOMPLETE"').groupby("date")["concrete_RAC"].value_counts().rename("nb")
 132 agg_data_incomplete_small_step = pd.DataFrame(agg_data_incomplete_small_step)
 133 agg_data_incomplete_small_step.to_csv(export_file_incomplete_small_step, mode="w", header=True)
 134
 135 agg_data_incomplete_giant_step = data.query('verdict == "INCOMPLETE"').groupby("date")["abstract_RAC"].value_counts().rename("nb")
 136 agg_data_incomplete_giant_step = pd.DataFrame(agg_data_incomplete_giant_step)
 137 agg_data_incomplete_giant_step.to_csv(export_file_incomplete_giant_step, mode="w", header=True)