tools/validator.py
Rama main · réplica de lectura del repositorio original.
#!/usr/bin/env python3
# #################### INFO ###########################################################
# This program is written as part of Christoph Siller's bachelor thesis.
# Validator is an automated checker for error inputs of C* code.
# It contains a parser for Boolectors witness format.
# A C* file is taken as input.
# The C* code is converted into a BTOR2 model using selfie -mc.
# The BTOR2 file is then checked using BtorMC.
# The resulting Witness is parsed to get the error generating input.
# The C* file is executed on Mipster (selfie) with the calculated input.
# The resulting error is compared to the predicted error.
#
# -----------------------------------------------------------------------------
# usage: validator.py [-h] [-d] [-e BAD_EXIT_CODE] [-s SELFIE_PATH]
# [-m BEATOR_PATH] [-b BTORMC_PATH] [-ts SELFIE_TIMEOUT]
# [-tb BTORMC_TIMEOUT] [-kmax KMAX] [-mem MEMORY]
# in_file
#
# positional arguments:
# in_file input C* file
#
# optional arguments:
# -h, --help show this help message and exit
# -d, --debug debug mode (generated files are kept)
# -e BAD_EXIT_CODE, --exitcode BAD_EXIT_CODE
# value for non-zero exit code bad-state
# -s SELFIE_PATH, --selfie SELFIE_PATH
# path to selfie executable
# -m BEATOR_PATH, --beator BEATOR_PATH
# path to beator.selfie
# -b BTORMC_PATH, --btormc BTORMC_PATH
# path to btormc executable
# -ts SELFIE_TIMEOUT, --timeout_selfie SELFIE_TIMEOUT
# timeout for execution of in_file on mipster (example:
# 10s, 5m, 1h)
# -tb BTORMC_TIMEOUT, --timeout_btormc BTORMC_TIMEOUT
# timeout for execution of btormc with the generated
# btor2 file (example: 10s, 10m, 1h)
# -kmax KMAX -kmax parameter for btormc
# -mem MEMORY, --memory MEMORY
# memory [MB] for mipster
# -----------------------------------------------------------------------------------
#
# Exitcodes:
# 0 - Error successfully verified
# 1 - Could not verify predicted error
# 2 - File Not Found
# 3 - Parser error
# 4 - Timeout
# 5 - Internal error
# #################### IMPORT ##########################################################
from sys import exit
from re import match
from os import system, stat, popen, path
from argparse import ArgumentParser
# ##################### GLOBALS ########################################################
witness = None # input stream
output = None # output stream
symbols = [] # holds current line of the input file split by blanks
symbol = "" # holds the current symbol
props = [] # holds properties of the witness
memory_constraints = [] # memory assignments encoded in the witness
frame_content = [] # holds the content of the current frame
frame_number = -1 # number of current frame
# bad states are defined in the BTOR2 file and generated by selfie
bad_states = { "b0" : "ecall invalid syscall",
"b1" : "non-zero exit code",
"b2" : "division by zero",
"b3" : "remainder by zero",
"b4" : "memory access below lower bound",
"b5" : "memory access at or above upper bound",
"b6" : "word-unaligned memory access",
"b7" : "memory access below lower bound",
"b8" : "memory access at or above upper bound",
"b9" : "word-unaligned memory access"}
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY LIBRARY
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# returns the next symbol of the input file
def get_symbol():
global symbols
global symbol
# read next line
if len(symbols) == 0:
symbols = witness.readline().strip().split(" ")
symbols.append("\n")
# according to EBNF, semicolons can only appear at start of line
# ";" starts a comment -> ignore line after ;
while symbols[0][0] == ";":
symbols.clear()
symbols = witness.readline().strip().split(" ")
symbols.append("\n")
# write next symbol in symbol variable
symbol = symbols.pop(0)
# writes error-causing program-input to file
def generate_output(frame):
global output
# (0*) bit-vectors are filtered out
frame = list(filter(lambda x: int(x, 2) != 0, frame))
if len(frame) > 1:
print("\033[91mWarning: Frame " + frame_number + " is invalid due to multiple input values!\033[0m")
elif len(frame) == 1:
frame = frame[0] # simplification since only one element in list
if args.debug:
print("\033[94mValue: " + str(int(frame, 2)) + " at frame " + frame_number + "\033[0m")
try:
# split into bytes
for i in range(int(len(frame)/8), 0, -1):
if args.debug:
print("\033[94mByte#" + str(i) + " = " + str(frame[(i-1)*8: i*8]) + "\033[0m")
output.write(chr(int(frame[(i-1)*8 : i*8], 2))) # write corresponding char to file
except OverflowError:
print("\033[91mInput Overflow at Frame " + frame_number + "\033[0m")
# ################### PARSER FUNCTIONS ###############################################
# throws an parser error and exits the program
def parser_error(expected: str):
global symbol
if type(expected) == str:
print("\033[91mParser Error: '" + expected + "' expected but '" + symbol + "' found!\033[0m")
exit(3)
else:
print("\033[91mInternal error: argument is not a String!\033[0m")
# EBNF: "[" binary_string "]" binary_string
def parse_array_assignment():
global memory_constraints
memory_address = int(symbol.strip("[]"), 2)
get_symbol()
if match(r'[01]+', symbol):
value = int(symbol, 2)
get_symbol()
else:
parser_error("binary string")
memory_constraints.append([memory_address, value])
# EBNF: binary_string
def parse_bv_assignment():
global frame_content
if match(r'[01]+', symbol):
frame_content.append(symbol)
get_symbol()
else:
parser_error("binary string")
# EBNF: uint ( bv_assignment | array_assignment ) [ symbol ]
def parse_assignment():
if match(r'\[[01]+\]', symbol):
parse_array_assignment()
else:
parse_bv_assignment()
if len(symbols) == 1:
# symbol holds optional symbol after assignment
get_symbol()
# EBNF: { comment "\n" | assignment "\n" }
def parse_model():
# comments are handled globally
while symbol.isnumeric():
get_symbol()
parse_assignment()
if symbol == "\n":
get_symbol()
else:
parser_error("\n")
# EBNF: "#" uint "\n" model
def parse_state_part():
if match(r'#[0-9]+', symbol):
get_symbol()
if symbol == "\n":
get_symbol()
parse_model()
# EBNF: "@" uint "\n" model
def parse_input_part():
global frame_number
if match(r'@[0-9]+', symbol):
frame_number = symbol.strip('@')
get_symbol()
if symbol == "\n":
get_symbol()
parse_model()
else:
parser_error("\n")
else:
parser_error("@uint")
# EBNF: [ state_part ] input_part
def parse_frame():
global frame_content
frame_content = []
parse_state_part()
parse_input_part()
generate_output(frame_content)
# EBNF: ( "b" | "j" ) uint
def parse_prop():
if match(r'([bj][0-9]+\n?)', symbol):
props.append(symbol.strip())
get_symbol()
else:
parser_error("Witness Property")
# EBNF: "sat\n" { prop } "\n"
def parse_header():
if symbol == "sat":
get_symbol()
if symbol == "\n":
get_symbol()
while symbol != "\n":
parse_prop()
get_symbol()
if args.debug:
print("\033[94mProperties: " + str(props) + "\033[0m")
else:
parser_error("\n")
else:
parser_error("sat")
# EBNF: { comment "\n" } | header { frame } "."
def parse_witness():
# comments are handled globally
# get initial symbol
get_symbol()
parse_header()
while symbol != ".":
parse_frame()
if args.debug:
print("\033[94mParsing Witness finished\033[0m")
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN MAIN
# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# ################### READ ARGS #######################################################
arguments = ArgumentParser()
arguments.add_argument("-d", "--debug", dest="debug", action="store_const", const=True, default=False,
help="debug mode (generated files are kept)")
arguments.add_argument("-e", "--exitcode", dest="bad_exit_code", type=int, default=1,
help="value for non-zero exit code bad-state")
arguments.add_argument("-s", "--selfie", dest="selfie_path", default="./selfie",
help="path to selfie executable")
arguments.add_argument("-m", "--beator", dest="beator_path", default="./beator",
help="path to beator")
arguments.add_argument("-b", "--btormc", dest="btormc_path", default="btormc",
help="path to btormc executable")
arguments.add_argument("-ts", "--timeout_selfie", dest="selfie_timeout", default="10s",
help="timeout for execution of in_file on mipster (example: 10s, 5m, 1h)")
arguments.add_argument("-tb", "--timeout_btormc", dest="btormc_timeout", default="10m",
help="timeout for execution of btormc with the generated btor2 file (example: 10s, 10m, 1h)")
arguments.add_argument("-kmax", dest="kmax", type=int, default=10000, help="-kmax parameter for btormc")
arguments.add_argument("-mem", "--memory", dest="memory", type=int, default="2", help="memory [MB] for mipster")
arguments.add_argument(dest="in_file", help="input C* file")
args = arguments.parse_args()
# ################### GENERATING WITNESS ##############################################
# directory for temporary files
system("mkdir -p temp")
if args.debug:
print("\033[94mtemp directory built")
# --------- generating btor2 file -----------------------------
print("\033[93mgenerating BTOR2 file using beator...\033[0m")
if args.debug:
system(args.beator_path + " -c " + args.in_file + " - " + str(args.bad_exit_code))
else:
# beator output is discarded
system(args.beator_path + " -c " + args.in_file + " - " + str(args.bad_exit_code) + " 1 > /dev/null")
btor_name = path.splitext(args.in_file)[0] + "-beaten"
system("mv " + btor_name + ".btor2 ./temp/model.btor2")
if args.debug:
print("\033[94mBTOR2 model written to ./temp/model.btor2\033[0m")
# --------- generating witness ----------------------------------
print("\033[93mgenerating witness using btormc...\033[0m")
system('timeout ' + args.btormc_timeout + ' ' + args.btormc_path + ' -kmax ' + str(args.kmax)
+ ' ./temp/model.btor2 > ./temp/witness.wit ; if [ $? = 124 ]; then echo "btormc timed out" ; '
'fi >> ./temp/witness.wit')
if args.debug:
print("\033[94mwitness written to ./temp/witness.wit\033[0m")
# ################### PARSER ##########################################################
# open witness -------------------------------
try:
# check if an error was found
if stat("./temp/witness.wit").st_size == 0:
print("\033[92mNo error state found!\033[0m")
exit(0)
# popen returns an iterabel objects of stdout lines
result = [line.strip("\n") for line in popen('cat ./temp/witness.wit | grep -c "btormc timed out"')]
if result[0] == '1':
print("\033[91mError: btormc timed out!\033[0m")
exit(4)
witness = open("./temp/witness.wit", "r")
if args.debug:
print("\033[94mWitness file opened.\033[0m")
except FileNotFoundError as e:
print(e.strerror + ": " + args.in_file)
exit(2)
# open output file -----------------------------
output = open("./temp/error_input.txt", "w")
if args.debug:
print("\033[94mOutput file opened.\033[0m")
print("\033[93mparsing witness...\033[0m")
parse_witness()
if args.debug:
print("\033[94mNumber of Frames parsed: " + frame_number + "\033[0m")
for b in props:
print("\033[93m" + bad_states[b] + " error state found!\033[0m")
if len(memory_constraints) > 0:
print("\033[93mMemory constraints:\033[0m")
for x in memory_constraints:
print("\033[93m Value: " + str(x[1]) + " at address " + str(x[0]) + "\033[0m")
if args.debug:
print("\033[94mError causing input written to " + output.name + "\033[0m")
witness.close()
output.close()
if args.debug:
print("\033[94mInput and Output Stream closed.\033[0m")
# #################### EXECUTE CODE WITH CALCULATED INPUT #####################################
print("\033[93mExecuting " + args.in_file + " on Mipster with calculated input...\033[0m")
# if selfie times out, the exitcode generated by the timeout tool is 124
system('timeout ' + args.selfie_timeout + ' ' + args.selfie_path + ' -c ' + args.in_file + ' -m ' + str(args.memory)
+ ' < ./temp/error_input.txt > ./temp/selfie_out.txt ; if [ $? = 124 ]; then echo "selfie timed out" ;'
' fi >> ./temp/selfie_out.txt')
# check if selfie timed out --------------------------------------------------
# popen returns an iterabel objects of stdout lines
result = [line.strip("\n") for line in popen('cat ./temp/selfie_out.txt | grep -c "selfie timed out"')]
if result[0] == '1':
print("\033[91mError: Selfie timed out!\033[0m")
exit(4)
# ##################### SEARCH FOR EXPECTED ERROR ####################################
for b in props:
if b == 'b0':
print("\033[91mHow the Hell did you get this error?\n\033[0m")
error_text = '"unknown system call"'
elif b == 'b1':
error_text = '"exit code ' + str(args.bad_exit_code) + '"'
elif b == 'b2' or b == 'b3':
error_text = '"division by zero"'
elif b == 'b4' or b == 'b5' or b == 'b6' or b == 'b7' or b == 'b8' or b == 'b9':
error_text = '"uncaught invalid address"'
else:
# this should be unreachable
print("\033[91mInternal Error - unknown bad state!\033[0m")
exit(5)
if args.debug:
print("\033[94mError text: " + error_text + "\033[0m")
# search for error text is selfie output
result = [line.strip("\n") for line in popen('cat temp/selfie_out.txt | grep -c ' + error_text)]
if int(result[0]) > 0:
print("\033[92m" + bad_states[b] + " error verified!\033[0m")
exitcode = 0
else:
# if the file is reading from stdout, a wrong input is taken from "selfie_out.txt" and no timeout is triggered
print("\033[91m" + bad_states[b] + " error could not be verified. \n"
"consider memory constraints and make sure the C* file is reading from stdin!\033[0m")
exitcode = 1
# ######################### CLEANUP ############################################
# If debug mode is on, the generated files are kept for debugging purpose, else they are removed
if not args.debug:
print("\033[93mCleanup: removing temp directory (use debug mode to keep the files)\033[0m")
system("rm -r ./temp")
else:
print("\033[94mAll generated files in temp directory!\033[0m")
# exits with 0 if error was verified, else with 1
exit(exitcode)