#!/usr/bin/env python3 # Copyright (c) the Selfie Project authors. All rights reserved. # Please see the AUTHORS file for details. Use of this source code is # governed by a BSD license that can be found in the LICENSE file. # Selfie is a project of the Computational Systems Group at the # Department of Computer Sciences of the University of Salzburg # in Austria and the Faculty of Information Technology of the # Czech Technical University in Prague (CTU) in the Czech Republic. # For further information and code please refer to: # selfie.cs.uni-salzburg.at # Bitme was co-developed at the University of Salzburg and at CTU, # where it was developed under the project # Robotics and Advanced Industrial Production (Roboprox, # reg. no. CZ.02.01.01/00/22_008/0004590). # Bitme is a bounded model checker for BTOR2 models using # the Z3 and bitwuzla SMT solvers as reasoning engines. # Bitme is designed to work with BTOR2 models generated by rotor # for modeling RISC-V machines and RISC-V code. Rotor is a tool # that is part of the selfie system. # ------------------------------------------------------------ # for debugging segfaults: import faulthandler; faulthandler.enable() import btor2 import z3interface import bitwuzlainterface import bvdd as BVDD import cflobvdd as CFLOBVDD import pdd as PDD import ctypes try: rotor = ctypes.cdll.LoadLibrary("rotor") is_rotor_present = True except OSError: print("rotor is not available") is_rotor_present = False import concurrent.futures class Futures: executor = concurrent.futures.ThreadPoolExecutor() def __init__(self): self.cache_futures = {} def wait_step(self, step): assert step >= 0 if step in self.cache_futures: concurrent.futures.wait([self.cache_futures[step]]) return self.get_step(step) def fork_step(self, step): assert step >= 0 if step not in self.cache_futures: self.cache_futures[step] = Futures.executor.submit(self.get_step, step) from math import log2 from math import ceil class Values: BVDD = False BVDD_number_of_inputs = 0 CFLOBVDD = False CFLOBVDD_level = 0 CFLOBVDD_swap_level = 0 CFLOBVDD_fork_level = 0 CLOBVDD_number_of_inputs = 0 total_number_of_constants = 0 total_number_of_values = 0 total_number_of_distinct_inputs = 0 max_number_of_connections = 0 false = None true = None def __init__(self, sid_line, bits, value, var_line = None, bvdd = None, cflobvdd = None): assert isinstance(sid_line, Bitvector) assert sid_line.size == abs(bits) self.sid_line = sid_line self.bits = bits self.bvdd = bvdd self.cflobvdd = cflobvdd if isinstance(value, bool) or isinstance(value, int): assert sid_line.is_unsigned_value(value) if Values.BVDD: self.bvdd = BVDD.BVDD.constant(value) # self.bvdd = PDD.PDD.constant(value, BVDD.BVDD) if Values.CFLOBVDD: self.cflobvdd = CFLOBVDD.CFLOBVDD.constant(value) # self.cflobvdd = PDD.PDD.constant(value, CFLOBVDD.CFLOBVDD) Values.total_number_of_constants += 1 elif isinstance(var_line, Variable): if Values.BVDD: self.bvdd = BVDD.BVDD.projection(var_line.input_index) # self.bvdd = PDD.PDD.projection(var_line.input_index, BVDD.BVDD) if Values.CFLOBVDD: self.cflobvdd = CFLOBVDD.CFLOBVDD.projection(var_line.input_index) # self.cflobvdd = PDD.PDD.projection(var_line.input_index, CFLOBVDD.CFLOBVDD) Values.total_number_of_constants += 2**var_line.sid_line.size if Values.BVDD: Values.total_number_of_values += self.bvdd.number_of_outputs() Values.total_number_of_distinct_inputs += self.bvdd.number_of_distinct_inputs() else: assert Values.CFLOBVDD Values.total_number_of_values += self.cflobvdd.number_of_outputs() Values.total_number_of_distinct_inputs += self.cflobvdd.number_of_distinct_inputs() if Values.BVDD: Values.max_number_of_connections = max(Values.max_number_of_connections, self.bvdd.number_of_connections()) else: assert Values.CFLOBVDD Values.max_number_of_connections = max(Values.max_number_of_connections, self.cflobvdd.number_of_connections()) # for debugging assert self.is_consistent() def __str__(self): return f"{self.sid_line}: {self.bvdd} {self.cflobvdd}" def match_sorts(self, values): return self.sid_line.match_sorts(values.sid_line) def is_consistent(self): return self.bvdd.is_consistent() # BVDD adapter def get_input_expression(var_line, inputs): if inputs == 0: return [] else: assert inputs > 0 inputs_sid_line = Bitvec(btor2.Parser.next_nid(), 2**var_line.sid_line.size, var_line.comment, var_line.line_no) inputs_zero_line = Constd(btor2.Parser.next_nid(), inputs_sid_line, 0, var_line.comment, var_line.line_no) inputs_one_line = Constd(btor2.Parser.next_nid(), inputs_sid_line, 1, var_line.comment, var_line.line_no) if inputs.bit_count() == 1: # true if value of var_line is in singleton-set inputs comparison_line = Comparison(btor2.Parser.next_nid(), btor2.OP_EQ, Bool.boolean, Constd(btor2.Parser.next_nid(), var_line.sid_line, int(log2(inputs)), var_line.comment, var_line.line_no), var_line, var_line.comment, var_line.line_no) else: # true if value of var_line is in inputs comparison_line = Comparison(btor2.Parser.next_nid(), btor2.OP_NEQ, Bool.boolean, # check if value of var_line is in inputs by masking inputs with 2**var_line Logical(btor2.Parser.next_nid(), btor2.OP_AND, inputs_sid_line, Constd(btor2.Parser.next_nid(), inputs_sid_line, inputs, var_line.comment, var_line.line_no), # calculate 2**var_line by shifting 1 left by value of var_line Computation(btor2.Parser.next_nid(), btor2.OP_SLL, inputs_sid_line, inputs_one_line, Ext(btor2.Parser.next_nid(), btor2.OP_UEXT, inputs_sid_line, var_line, 2**var_line.sid_line.size - var_line.sid_line.size, var_line.comment, var_line.line_no), var_line.comment, var_line.line_no), var_line.comment, var_line.line_no), inputs_zero_line, var_line.comment, var_line.line_no) return [comparison_line] def get_bvdd_node_expression(sid_line, bvdd, sbdd, pdd, index = 0): if pdd and bvdd == BVDD.BVDD_Node.no_input: return None elif isinstance(bvdd, bool) or isinstance(bvdd, int): return Constd(btor2.Parser.next_nid(), sid_line, int(bvdd), "domain-propagated value", 0) elif bvdd.is_dont_care(): return Values.get_bvdd_node_expression(sid_line, bvdd.get_dont_care_output(), sbdd, pdd, index + 1) else: var_line = Variable.input_indexes[index] exp_line = None s2o = bvdd.get_s2o() # assert s2o is sorted by inputs for inputs in s2o: output = s2o[inputs] if exp_line is None: # reachable only if input value is in inputs exp_line = Values.get_bvdd_node_expression(sid_line, output, sbdd, pdd, index + 1) else: if sbdd: assert 0 <= inputs < 256 inputs = 2**inputs output_line = Values.get_bvdd_node_expression(sid_line, output, sbdd, pdd, index + 1) if output_line is None: continue exp_line = Ite(btor2.Parser.next_nid(), sid_line, Values.get_input_expression(var_line, inputs)[0], output_line, exp_line, var_line.comment, var_line.line_no) return exp_line def get_bvdd_expression(self): return Values.get_bvdd_node_expression(self.sid_line, self.bvdd, not (isinstance(self.bvdd, BVDD.SBDD_s2o) or isinstance(self.bvdd, BVDD.SBDD_o2s)), False) # CFLOBVDD adapter def get_logical_expression(op, paths): if not paths: return [] else: logical_line = None for path_line in paths: if logical_line is None: logical_line = path_line else: logical_line = Logical(btor2.Parser.next_nid(), op, Bool.boolean, logical_line, path_line, path_line.comment, path_line.line_no) return [logical_line] def get_path_expression(paths): path_expression = [] for path in paths: if isinstance(path[0], int): assert isinstance(path[1], int) index_i = path[0] inputs = path[1] path_expression += Values.get_input_expression(Variable.input_indexes[index_i], inputs) else: a_paths = Values.get_path_expression(path[0]) b_paths = Values.get_path_expression(path[1]) path_expression += Values.get_logical_expression(btor2.OP_AND, a_paths + b_paths) return Values.get_logical_expression(btor2.OP_OR, path_expression) def get_cflobvdd_expression(self): cflobvdd = self.cflobvdd exp_line = None for exit_i in cflobvdd.outputs: output_line = Constd(btor2.Parser.next_nid(), self.sid_line, int(cflobvdd.outputs[exit_i]), "domain-propagated value", 0) if len(cflobvdd.outputs) == 1: # dont-care output return output_line elif exp_line is None: # reachable only if input value is in inputs exp_line = output_line else: input_line = Values.get_path_expression(cflobvdd.grouping.get_paths(exit_i)) assert input_line exp_line = Ite(btor2.Parser.next_nid(), self.sid_line, input_line[0], output_line, exp_line, self.sid_line.comment, self.sid_line.line_no) return exp_line # PDD adapter def get_pdd_expression(self, clss): pdd = self.bvdd if clss is BVDD.BVDD else self.cflobvdd exp_line = None for output_value in pdd.o2s: inputs = pdd.o2s[output_value] output_line = Constd(btor2.Parser.next_nid(), self.sid_line, int(output_value), "domain-propagated value", 0) if len(pdd.o2s) == 1: assert not inputs.is_not_full() # dont-care output return output_line elif exp_line is None: # reachable only if input value is in inputs exp_line = output_line else: if isinstance(inputs, BVDD): input_line = Values.get_bvdd_node_expression(self.sid_line, inputs, not (isinstance(inputs, BVDD.SBDD_s2o) or isinstance(inputs, BVDD.SBDD_o2s)), True) else: assert 0 < len(inputs.outputs) <= 2 exit_i = 1 if inputs.outputs[1] == CFLOBVDD.CFLOBVDD.has_input else 2 input_line = Values.get_path_expression(inputs.grouping.get_paths(exit_i))[0] assert input_line exp_line = Ite(btor2.Parser.next_nid(), self.sid_line, input_line, output_line, exp_line, self.sid_line.comment, self.sid_line.line_no) return exp_line # expressions def get_expression(self): # naive transition from domain propagation to bit blasting assert isinstance(self.sid_line, Bitvector) if Values.BVDD: if isinstance(self.bvdd, BVDD.BVDD): return self.get_bvdd_expression() else: return self.get_pdd_expression(BVDD.BVDD) else: assert Values.CFLOBVDD if isinstance(self.cflobvdd, CFLOBVDD.CFLOBVDD): return self.get_cflobvdd_expression() else: return self.get_pdd_expression(CFLOBVDD.CFLOBVDD) def FALSE(): if Values.false is None: Values.false = Values(Bool.boolean, 1, False) return Values.false def TRUE(): if Values.true is None: Values.true = Values(Bool.boolean, 1, True) return Values.true def is_always_false(self): assert isinstance(self.sid_line, Bool) if Values.BVDD and Values.CFLOBVDD: assert self.bvdd.is_always_false() == self.cflobvdd.is_always_false() if Values.BVDD: return self.bvdd.is_always_false() if Values.CFLOBVDD: return self.cflobvdd.is_always_false() def is_always_true(self): assert isinstance(self.sid_line, Bool) if Values.BVDD and Values.CFLOBVDD: assert self.bvdd.is_always_true() == self.cflobvdd.is_always_true() if Values.BVDD: return self.bvdd.is_always_true() if Values.CFLOBVDD: return self.cflobvdd.is_always_true() # per-value semantics of value sets # unary operators def apply_unary(self, sid_line, op, op_id, bits): bvdd = cflobvdd = None if Values.BVDD: bvdd = self.bvdd.compute_unary(op, op_id, bits) if Values.CFLOBVDD: cflobvdd = self.cflobvdd.compute_unary(op, op_id, bits) return Values(sid_line, bits, None, None, bvdd, cflobvdd) def SignExt(self, sid_line): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(sid_line, lambda x: self.sid_line.get_signed_value(x) % 2**sid_line.size, f"sext {self.sid_line.size} {sid_line.size}", -sid_line.size) def ZeroExt(self, sid_line): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(sid_line, lambda x: x, f"uext", sid_line.size) def Extract(self, sid_line, u, l): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(sid_line, lambda x: (x & 2**(u + 1) - 1) >> l, f"slice {u} {l}", sid_line.size) def Not(self): assert isinstance(self.sid_line, Bool) return self.apply_unary(self.sid_line, lambda x: not x, "not", 1) def __invert__(self): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(self.sid_line, lambda x: ~x % 2**self.sid_line.size, f"inv {self.sid_line.size}", self.bits) def Inc(self): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(self.sid_line, lambda x: (x + 1) % 2**self.sid_line.size, f"inc {self.sid_line.size}", self.bits) def Dec(self): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(self.sid_line, lambda x: (x - 1) % 2**self.sid_line.size, f"dec {self.sid_line.size}", self.bits) def __neg__(self): assert isinstance(self.sid_line, Bitvec) return self.apply_unary(self.sid_line, lambda x: -x % 2**self.sid_line.size, f"neg {self.sid_line.size}", -self.sid_line.size) # binary operators def apply_binary(self, sid_line, values, op, op_id, bits): assert isinstance(values, Values), f"{self} {op} {values}" bvdd = cflobvdd = None if Values.BVDD: bvdd = self.bvdd.compute_binary(op, values.bvdd, op_id, bits) if Values.CFLOBVDD: cflobvdd = self.cflobvdd.compute_binary(op, values.cflobvdd, op_id, bits) return Values(sid_line, bits, None, None, bvdd, cflobvdd) def Implies(self, values): assert isinstance(self.sid_line, Bool) if self.is_always_false(): return Values.TRUE() else: # lazy evaluation of implied values assert isinstance(values, Values) and isinstance(values.sid_line, Bool) return self.apply_binary(Bool.boolean, values, lambda x, y: (not x) or y, "implies", 1) def __eq__(self, values): assert isinstance(self.sid_line, Bitvector) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x == y, "eq", 1) def __ne__(self, values): assert isinstance(self.sid_line, Bitvector) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x != y, "neq", 1) def __gt__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: self.sid_line.get_signed_value(x) > values.sid_line.get_signed_value(y), f"sgt {self.sid_line.size} {values.sid_line.size}", 1) def UGT(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x > y, "ugt", 1) def __ge__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: self.sid_line.get_signed_value(x) >= values.sid_line.get_signed_value(y), f"sge {self.sid_line.size} {values.sid_line.size}", 1) def UGE(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x >= y, "uge", 1) def __lt__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: self.sid_line.get_signed_value(x) < values.sid_line.get_signed_value(y), f"slt {self.sid_line.size} {values.sid_line.size}", 1) def ULT(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x < y, "ult", 1) def __le__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: self.sid_line.get_signed_value(x) <= values.sid_line.get_signed_value(y), f"sle {self.sid_line.size} {values.sid_line.size}", 1) def ULE(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(Bool.boolean, values, lambda x, y: x <= y, "ule", 1) def And(self, values): assert isinstance(self.sid_line, Bool) if self.is_always_false(): return Values.FALSE() else: # lazy evaluation of second operand assert isinstance(values, Values) and isinstance(values.sid_line, Bool) return self.apply_binary(Bool.boolean, values, lambda x, y: x and y, "And", 1) def Or(self, values): assert isinstance(self.sid_line, Bool) if self.is_always_true(): return Values.TRUE() else: # lazy evaluation of second operand assert isinstance(values, Values) and isinstance(values.sid_line, Bool) return self.apply_binary(Bool.boolean, values, lambda x, y: x or y, "Or", 1) def Xor(self, values): assert isinstance(self.sid_line, Bool) and isinstance(values.sid_line, Bool) return self.apply_binary(Bool.boolean, values, lambda x, y: x != y, "Xor", 1) def __and__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: x & y, "and", min(self.bits, values.bits)) def __or__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: x | y, "or", min(self.bits, values.bits)) def __xor__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: x ^ y, "xor", min(self.bits, values.bits)) def __lshift__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (x << y) % 2**self.sid_line.size, f"lshl {self.sid_line.size}", self.bits) def LShR(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (x >> y) % 2**self.sid_line.size, f"lshr {self.sid_line.size}", self.sid_line.size) def __rshift__(self, values): # right shift operator computes arithmetic right shift in Python assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (self.sid_line.get_signed_value(x) >> y) % 2**self.sid_line.size, f"ashr {self.sid_line.size}", -self.sid_line.size) def __add__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (x + y) % 2**self.sid_line.size, f"add {self.sid_line.size}", min(self.bits, values.bits)) def __sub__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (x - y) % 2**self.sid_line.size, f"sub {self.sid_line.size}", min(self.bits, values.bits)) def __mul__(self, values): assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (x * y) % 2**self.sid_line.size, f"mul {self.sid_line.size}", min(self.bits, values.bits)) def __truediv__(self, values): # using the integer portion of division, not floor division with the // operator, # because int(x / y) != x // y in Python if x < 0 or y < 0 since # the integer portion of division truncates towards 0 whereas # floor division truncates towards negative infinity assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (int(self.sid_line.get_signed_value(x) / values.sid_line.get_signed_value(y)) if not (y == 0 or (self.sid_line.get_signed_value(x) == -2**(self.sid_line.size - 1) and values.sid_line.get_signed_value(y) == -1)) else -1 if y == 0 else -2**(self.sid_line.size - 1)) % 2**self.sid_line.size, f"sdiv {self.sid_line.size} {values.sid_line.size}", -self.sid_line.size) def UDiv(self, values): # using floor division is ok since x >= 0 and y >= 0 assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: x // y if y != 0 else 2**self.sid_line.size - 1, f"udiv {self.sid_line.size}", self.sid_line.size) def SRem(self, values): # using the integer portion of division, not the % operator, # because x % y != x - int(x / y) * y in Python if x < 0 since # the % operator in Python computes Euclidean modulus, not remainder, # such that x // y * y + x % y == x holds in Python for all x and y even if x < 0 assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: (self.sid_line.get_signed_value(x) - int(self.sid_line.get_signed_value(x) / values.sid_line.get_signed_value(y)) * values.sid_line.get_signed_value(y)) % 2**self.sid_line.size if not (y == 0 or (self.sid_line.get_signed_value(x) == -2**(self.sid_line.size - 1) and values.sid_line.get_signed_value(y) == -1)) else x if y == 0 else 0, f"srem {self.sid_line.size} {values.sid_line.size}", -self.sid_line.size) def URem(self, values): # using the % operator is ok since x >= 0 and y >= 0 assert isinstance(self.sid_line, Bitvec) and self.sid_line.match_sorts(values.sid_line) return self.apply_binary(self.sid_line, values, lambda x, y: x % y if y != 0 else x, "urem", self.sid_line.size) def Concat(self, values, sid_line): assert isinstance(self.sid_line, Bitvec) and isinstance(values.sid_line, Bitvec) bits = self.sid_line.size + values.sid_line.size if self.bits > 0 else \ -(self.sid_line.size + values.sid_line.size) return self.apply_binary(sid_line, values, lambda x, y: (x << values.sid_line.size) + y, f"concat {values.sid_line.size}", bits) # ternary operator def ite(self, values2, values3): assert isinstance(self.sid_line, Bool) assert isinstance(values2, Values) and isinstance(values3, Values) assert values2.match_sorts(values3) bits = min(values2.bits, values3.bits) bvdd = cflobvdd = None if Values.BVDD: bvdd = self.bvdd.compute_ite(values2.bvdd, values3.bvdd, "ite", bits) if Values.CFLOBVDD: cflobvdd = self.cflobvdd.compute_ite(values2.cflobvdd, values3.cflobvdd, "ite", bits) return Values(values2.sid_line, bits, None, None, bvdd, cflobvdd) LAMBDAS = True UNROLL = False PROPAGATE = None PROPAGATE_UNARY = True PROPAGATE_BINARY = True PROPAGATE_ITE = True class Line(btor2.Line, z3interface.Z3, bitwuzlainterface.Bitwuzla): def __init__(self): z3interface.Z3.__init__(self) bitwuzlainterface.Bitwuzla.__init__(self) class Sort(Line, btor2.Sort): def __init__(self): Line.__init__(self) class Bitvector(Sort, btor2.Bitvector): def __init__(self): Sort.__init__(self) class Bool(Bitvector, btor2.Bool, z3interface.Bool, bitwuzlainterface.Bool): def __init__(self, nid, comment, line_no): Bitvector.__init__(self) btor2.Bool.__init__(self, nid, comment, line_no) class Bitvec(Bitvector, btor2.Bitvec, z3interface.Bitvec, bitwuzlainterface.Bitvec): def __init__(self, nid, size, comment, line_no): Bitvector.__init__(self) btor2.Bitvec.__init__(self, nid, size, comment, line_no) class Array(Sort, btor2.Array, z3interface.Array, bitwuzlainterface.Array): def __init__(self, nid, array_size_line, element_size_line, comment, line_no): Sort.__init__(self) btor2.Array.__init__(self, nid, array_size_line, element_size_line, comment, line_no) class Expression(Line, btor2.Expression, z3interface.Expression, bitwuzlainterface.Expression): def __init__(self): Line.__init__(self) self.cache_values = {} z3interface.Expression.__init__(self) bitwuzlainterface.Expression.__init__(self) def get_expression(self): return self def is_cached(self, step): assert step >= 0 if step in self.cache_values: if self.cache_values[step][1] in Bitme_Solver.versions: if self.cache_values[step][1] == Bitme_Solver.covered_version: return True elif Bitme_Solver.version != Bitme_Solver.covered_version: return True elif step < Bitme_Solver.covered_step: return True else: # re-compute values for first uncovered step return False else: return False else: return False def get_values(self, step): assert step >= 0 if UNROLL or PROPAGATE is not None: # versioning needed for support of branching and increments in bitme solver if not self.is_cached(step): self.cache_values[step] = (self.compute_values(step), Bitme_Solver.version) return self.cache_values[step][0] else: return self class Constant(Expression, btor2.Constant, z3interface.Constant, bitwuzlainterface.Constant): def __init__(self): Expression.__init__(self) def get_values(self, step): assert step >= 0 return super().get_values(0) def compute_values(self, step): assert step == 0 if PROPAGATE is not None: if isinstance(self.sid_line, Bool): return Values.TRUE() if bool(self.value) else Values.FALSE() else: assert isinstance(self.sid_line, Bitvec) bits = self.sid_line.size if self.signed_value >= 0 else -self.sid_line.size return Values(self.sid_line, bits, self.value) else: return self class Zero(Constant, btor2.Zero): def __init__(self, nid, sid_line, symbol, comment, line_no): Constant.__init__(self) btor2.Zero.__init__(self, nid, sid_line, symbol, comment, line_no) class One(Constant, btor2.One): def __init__(self, nid, sid_line, symbol, comment, line_no): Constant.__init__(self) btor2.One.__init__(self, nid, sid_line, symbol, comment, line_no) class Constd(Constant, btor2.Constd): def __init__(self, nid, sid_line, value, comment, line_no): Constant.__init__(self) btor2.Constd.__init__(self, nid, sid_line, value, comment, line_no) class Const(Constant, btor2.Const): def __init__(self, nid, sid_line, value, comment, line_no): Constant.__init__(self) btor2.Const.__init__(self, nid, sid_line, value, comment, line_no) class Consth(Constant, btor2.Consth): def __init__(self, nid, sid_line, value, comment, line_no): Constant.__init__(self) btor2.Consth.__init__(self, nid, sid_line, value, comment, line_no) class Constant_Array(Expression, btor2.Constant_Array, z3interface.Constant_Array, bitwuzlainterface.Constant_Array): def __init__(self, sid_line, constant_line): Expression.__init__(self) btor2.Constant_Array.__init__(self, sid_line, constant_line) def get_values(self, step): assert step >= 0 return self class Variable(Expression, btor2.Variable, z3interface.Variable): incremental_number_of_input_variables = 1 uncovered_steps = {} def __init__(self): Expression.__init__(self) def is_uncovered(self): return self.input_index is not None and \ self.input_index > Variable.incremental_number_of_input_variables - 1 def cover(self): if self.is_uncovered(): return Variable.input_indexes[Variable.incremental_number_of_input_variables - 1] else: return self def get_values(self, step): if self.is_uncovered(): # exploiting thread-safe single dict updates Variable.uncovered_steps[step] = None return self.cover().get_values(step) else: return super().get_values(step) def compute_values(self, step): assert step == 0 if (isinstance(self.sid_line, Bitvector) and PROPAGATE is not None and self.sid_line.size <= PROPAGATE): return Values(self.sid_line, self.sid_line.size, None, self) else: return self class Input(Variable, btor2.Input, z3interface.Input, bitwuzlainterface.Input): def __init__(self, nid, sid_line, symbol, comment, line_no, index = None): Variable.__init__(self) btor2.Input.__init__(self, nid, sid_line, symbol, comment, line_no, index) def get_step_name(self, step): return self.name def compute_values(self, step): return super().compute_values(0) class State(Variable, btor2.State, z3interface.State, bitwuzlainterface.State): pc = None def __init__(self, nid, sid_line, symbol, comment, line_no, index = None): Variable.__init__(self) btor2.State.__init__(self, nid, sid_line, symbol, comment, line_no, index) z3interface.State.__init__(self) bitwuzlainterface.State.__init__(self) if symbol == "core-0-pc": State.pc = self def get_step_name(self, step): return f"{self.name}-{step}" def compute_values(self, step): assert step >= 0 if step == 0: if self.init_line is None: # uninitialized state return super().compute_values(0) elif UNROLL: return self.init_line.wait_step(0) else: return self elif self.next_line is None or self.next_line.exp_line is self: # untransitioned state or transitioned to itself return self.get_values(0) elif UNROLL: return self.next_line.wait_step(step - 1) else: return self class Indexed(Expression, btor2.Indexed): def __init__(self): Expression.__init__(self) class Ext(Indexed, btor2.Ext, z3interface.Ext, bitwuzlainterface.Ext): def __init__(self, nid, op, sid_line, arg1_line, w, comment, line_no): Indexed.__init__(self) btor2.Ext.__init__(self, nid, op, sid_line, arg1_line, w, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) if PROPAGATE_UNARY and isinstance(arg1_value, Values): if self.op == btor2.OP_SEXT: return arg1_value.SignExt(self.sid_line) else: assert self.op == btor2.OP_UEXT return arg1_value.ZeroExt(self.sid_line) else: return self.copy(arg1_value.get_expression()) class Slice(Indexed, btor2.Slice, z3interface.Slice, bitwuzlainterface.Slice): def __init__(self, nid, sid_line, arg1_line, u, l, comment, line_no): Indexed.__init__(self) btor2.Slice.__init__(self, nid, sid_line, arg1_line, u, l, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) if PROPAGATE_UNARY and isinstance(arg1_value, Values): return arg1_value.Extract(self.sid_line, self.u, self.l) else: return self.copy(arg1_value.get_expression()) class Unary(Expression, btor2.Unary, z3interface.Unary, bitwuzlainterface.Unary): def __init__(self, nid, op, sid_line, arg1_line, comment, line_no): Expression.__init__(self) btor2.Unary.__init__(self, nid, op, sid_line, arg1_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) if PROPAGATE_UNARY and isinstance(arg1_value, Values): if self.op == btor2.OP_NOT: if isinstance(self.sid_line, Bool): return arg1_value.Not() else: return ~arg1_value elif self.op == btor2.OP_INC: return arg1_value.Inc() elif self.op == btor2.OP_DEC: return arg1_value.Dec() else: assert self.op == btor2.OP_NEG return -arg1_value else: return self.copy(arg1_value.get_expression()) class Binary(Expression, btor2.Binary): def __init__(self): Expression.__init__(self) class Implies(Binary, btor2.Implies, z3interface.Implies, bitwuzlainterface.Implies): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Implies.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) if PROPAGATE_BINARY and isinstance(arg1_value, Values): if arg1_value.is_always_false(): return arg1_value.Implies(None) else: # lazy evaluation of implied values arg2_value = self.arg2_line.get_values(step) if isinstance(arg2_value, Values): return arg1_value.Implies(arg2_value) else: arg2_value = self.arg2_line.get_values(step) return self.copy(arg1_value.get_expression(), arg2_value.get_expression()) class Comparison(Binary, btor2.Comparison, z3interface.Comparison, bitwuzlainterface.Comparison): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Comparison.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) arg2_value = self.arg2_line.get_values(step) if PROPAGATE_BINARY: if isinstance(arg1_value, Values) and isinstance(arg2_value, Values): if self.op == btor2.OP_EQ: return arg1_value == arg2_value elif self.op == btor2.OP_NEQ: return arg1_value != arg2_value elif self.op == btor2.OP_SGT: return arg1_value > arg2_value elif self.op == btor2.OP_UGT: return arg1_value.UGT(arg2_value) elif self.op == btor2.OP_SGTE: return arg1_value >= arg2_value elif self.op == btor2.OP_UGTE: return arg1_value.UGE(arg2_value) elif self.op == btor2.OP_SLT: return arg1_value < arg2_value elif self.op == btor2.OP_ULT: return arg1_value.ULT(arg2_value) elif self.op == btor2.OP_SLTE: return arg1_value <= arg2_value else: assert self.op == btor2.OP_ULTE return arg1_value.ULE(arg2_value) return self.copy(arg1_value.get_expression(), arg2_value.get_expression()) def is_always_false(self): # only needed for termination check return False def get_step(self, step): # only needed for termination check assert step >= 0 return self.get_values(step) def wait_step(self, step): # no waiting return self.get_step(step) class Logical(Binary, btor2.Logical, z3interface.Logical, bitwuzlainterface.Logical): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Logical.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): if PROPAGATE_BINARY: if isinstance(self.sid_line, Bool): arg1_value = self.arg1_line.get_values(step) if isinstance(arg1_value, Values): if self.op == btor2.OP_AND: if arg1_value.is_always_false(): return arg1_value.And(None) else: # lazy evaluation of second operand arg2_value = self.arg2_line.get_values(step) if isinstance(arg2_value, Values): return arg1_value.And(arg2_value) elif self.op == btor2.OP_OR: if arg1_value.is_always_true(): return arg1_value.Or(None) else: # lazy evaluation of second operand arg2_value = self.arg2_line.get_values(step) if isinstance(arg2_value, Values): return arg1_value.Or(arg2_value) else: assert self.op == btor2.OP_XOR arg2_value = self.arg2_line.get_values(step) if isinstance(arg2_value, Values): return arg1_value.Xor(arg2_value) arg2_value = self.arg2_line.get_values(step) else: arg1_value = self.arg1_line.get_values(step) arg2_value = self.arg2_line.get_values(step) if isinstance(arg1_value, Values) and isinstance(arg2_value, Values): if self.op == btor2.OP_AND: return arg1_value & arg2_value elif self.op == btor2.OP_OR: return arg1_value | arg2_value else: assert self.op == btor2.OP_XOR return arg1_value ^ arg2_value else: arg1_value = self.arg1_line.get_values(step) arg2_value = self.arg2_line.get_values(step) return self.copy(arg1_value.get_expression(), arg2_value.get_expression()) class Computation(Binary, btor2.Computation, z3interface.Computation, bitwuzlainterface.Computation): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Computation.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) arg2_value = self.arg2_line.get_values(step) if PROPAGATE_BINARY: if isinstance(arg1_value, Values) and isinstance(arg2_value, Values): if self.op == btor2.OP_SLL: return arg1_value << arg2_value elif self.op == btor2.OP_SRL: return arg1_value.LShR(arg2_value) elif self.op == btor2.OP_SRA: return arg1_value >> arg2_value elif self.op == btor2.OP_ADD: return arg1_value + arg2_value elif self.op == btor2.OP_SUB: return arg1_value - arg2_value elif self.op == btor2.OP_MUL: return arg1_value * arg2_value elif self.op == btor2.OP_SDIV: return arg1_value / arg2_value elif self.op == btor2.OP_UDIV: return arg1_value.UDiv(arg2_value) elif self.op == btor2.OP_SREM: return arg1_value.SRem(arg2_value) else: assert self.op == btor2.OP_UREM return arg1_value.URem(arg2_value) return self.copy(arg1_value.get_expression(), arg2_value.get_expression()) class Concat(Binary, btor2.Concat, z3interface.Concat, bitwuzlainterface.Concat): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Concat.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) arg2_value = self.arg2_line.get_values(step) if PROPAGATE_BINARY: if isinstance(arg1_value, Values) and isinstance(arg2_value, Values): return arg1_value.Concat(arg2_value, self.sid_line) return self.copy(arg1_value.get_expression(), arg2_value.get_expression()) class Read(Binary, btor2.Read, z3interface.Read, bitwuzlainterface.Read): def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): Binary.__init__(self) btor2.Read.__init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step).get_expression() arg2_value = self.arg2_line.get_values(step).get_expression() return self.copy(arg1_value, arg2_value) class Ternary(Expression, btor2.Ternary): def __init__(self): Expression.__init__(self) class Ite(Ternary, btor2.Ite, z3interface.Ite, bitwuzlainterface.Ite): def __init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no): Ternary.__init__(self) btor2.Ite.__init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step) if PROPAGATE_ITE and isinstance(arg1_value, Values): if arg1_value.is_always_true(): arg2_value = self.arg2_line.get_values(step) if not isinstance(arg2_value, Values): arg2_value = arg2_value.get_expression() return arg2_value elif arg1_value.is_always_false(): arg3_value = self.arg3_line.get_values(step) if not isinstance(arg3_value, Values): arg3_value = arg3_value.get_expression() return arg3_value else: # lazy evaluation of true and false case arg2_value = self.arg2_line.get_values(step) arg3_value = self.arg3_line.get_values(step) if isinstance(arg2_value, Values) and isinstance(arg3_value, Values): return arg1_value.ite(arg2_value, arg3_value) else: arg2_value = self.arg2_line.get_values(step) arg3_value = self.arg3_line.get_values(step) return self.copy(arg1_value.get_expression(), arg2_value.get_expression(), arg3_value.get_expression()) def get_step(self, step): # only needed for branching assert step >= 0 return self.get_values(step) def wait_step(self, step): # no waiting return self.get_step(step) class Write(Ternary, btor2.Write, z3interface.Write, bitwuzlainterface.Write): def __init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no): Ternary.__init__(self) btor2.Write.__init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no) def compute_values(self, step): arg1_value = self.arg1_line.get_values(step).get_expression() arg2_value = self.arg2_line.get_values(step).get_expression() arg3_value = self.arg3_line.get_values(step).get_expression() return self.copy(arg1_value, arg2_value, arg3_value) class Transitional(Line, btor2.Transitional): def __init__(self): Line.__init__(self) class Init(Transitional, btor2.Init, z3interface.Init, bitwuzlainterface.Init): def __init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line = None, index = None): Transitional.__init__(self) btor2.Init.__init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line, index) def get_step(self, step): assert step == 0, f"get init with {step} != 0" return self.exp_line.get_values(0) def wait_step(self, step): # no waiting return self.get_step(step) class Next(Transitional, btor2.Next, z3interface.Next, bitwuzlainterface.Next, Futures): def __init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line = None, index = None): Transitional.__init__(self) btor2.Next.__init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line, index) z3interface.Next.__init__(self) bitwuzlainterface.Next.__init__(self) Futures.__init__(self) self.is_state_changing_line = None self.state_is_not_changing_line = None def get_step(self, step): assert step >= 0 return self.exp_line.get_values(step) def is_state_changing(self): if self.is_state_changing_line is None: self.is_state_changing_line = Comparison(btor2.Parser.next_nid(), btor2.OP_NEQ, Bool.boolean, self.state_line, self.exp_line, f"state change check for {self.symbol}", self.line_no) return self.is_state_changing_line def state_is_not_changing(self): if self.state_is_not_changing_line is None: self.state_is_not_changing_line = Comparison(btor2.Parser.next_nid(), btor2.OP_EQ, Bool.boolean, self.state_line, self.exp_line, f"state is not changing for {self.symbol}", self.line_no) return self.state_is_not_changing_line class Property(Line, btor2.Property, z3interface.Property, bitwuzlainterface.Property, Futures): def __init__(self): Line.__init__(self) Futures.__init__(self) def get_step(self, step): assert step >= 0 return self.property_line.get_values(step) class Constraint(Property, btor2.Constraint): def __init__(self, nid, property_line, symbol, comment, line_no): Property.__init__(self) btor2.Constraint.__init__(self, nid, property_line, symbol, comment, line_no) class Bad(Property, btor2.Bad): def __init__(self, nid, property_line, symbol, comment, line_no): Property.__init__(self) btor2.Bad.__init__(self, nid, property_line, symbol, comment, line_no) # parser interface class ValuesParser(btor2.Parser): def get_class(self, clss_or_keyword): if clss_or_keyword is btor2.Bool: return Bool elif clss_or_keyword is btor2.Bitvec: return Bitvec elif clss_or_keyword is btor2.Array: return Array elif clss_or_keyword is btor2.Constant_Array: return Constant_Array elif clss_or_keyword is btor2.Zero or clss_or_keyword == btor2.Zero.keyword: return Zero elif clss_or_keyword is btor2.One or clss_or_keyword == btor2.One.keyword: return One elif clss_or_keyword is btor2.Constd or clss_or_keyword == btor2.Constd.keyword: return Constd elif clss_or_keyword is btor2.Const or clss_or_keyword == btor2.Const.keyword: return Const elif clss_or_keyword is btor2.Consth or clss_or_keyword == btor2.Consth.keyword: return Consth elif clss_or_keyword is btor2.Input or clss_or_keyword == btor2.Input.keyword: return Input elif clss_or_keyword is btor2.State or clss_or_keyword == btor2.State.keyword: return State elif clss_or_keyword is btor2.Ext or clss_or_keyword in btor2.Ext.keywords: return Ext elif clss_or_keyword is btor2.Slice or clss_or_keyword == btor2.Slice.keyword: return Slice elif clss_or_keyword is btor2.Unary or clss_or_keyword in btor2.Unary.keywords: return Unary elif clss_or_keyword is btor2.Implies or clss_or_keyword == btor2.Implies.keyword: return Implies elif clss_or_keyword is btor2.Comparison or clss_or_keyword in btor2.Comparison.keywords: return Comparison elif clss_or_keyword is btor2.Logical or clss_or_keyword in btor2.Logical.keywords: return Logical elif clss_or_keyword is btor2.Computation or clss_or_keyword in btor2.Computation.keywords: return Computation elif clss_or_keyword is btor2.Concat or clss_or_keyword == btor2.Concat.keyword: return Concat elif clss_or_keyword is btor2.Read or clss_or_keyword == btor2.Read.keyword: return Read elif clss_or_keyword is btor2.Ite or clss_or_keyword == btor2.Ite.keyword: return Ite elif clss_or_keyword is btor2.Write or clss_or_keyword == btor2.Write.keyword: return Write elif clss_or_keyword is btor2.Init or clss_or_keyword == btor2.Init.keyword: return Init elif clss_or_keyword is btor2.Next or clss_or_keyword == btor2.Next.keyword: return Next elif clss_or_keyword is btor2.Constraint or clss_or_keyword == btor2.Constraint.keyword: return Constraint elif clss_or_keyword is btor2.Bad or clss_or_keyword == btor2.Bad.keyword: return Bad # console output def get_step(step, level): if step is None or level is None: return "" elif level == 0: return f"{step}: " else: return f"{step}-{level}: " last_message_length = 0 def print_message(message, step = None, level = None): global last_message_length if last_message_length > 0: print("\r%s" % (" " * last_message_length), end='\r') message = f"{get_step(step, level)}{message}" print(message, end='', flush=True) last_message_length = len(message) if message[-1:] != '\n' else 0 def print_separator(separator, step = None, level = None): print_message(f"{separator * (80 - len(get_step(step, level)))}\n", step, level) def print_message_with_propagation_profile(message, step = None, level = None): if UNROLL or PROPAGATE is not None: string = f"({Values.total_number_of_constants} constants, " string += f"{Values.total_number_of_values} values, " string += f"{Values.total_number_of_distinct_inputs} distinct inputs, " string += f"{Values.max_number_of_connections} connections, " string += f"{Expression.total_number_of_generated_expressions} expressions) {message}" message = string print_message(message, step, level) # bitme solver class Bitme_Solver: versions = {0:None} version = 0 covered_version = 1 covered_step = 0 bump = 2 def __init__(self, z3_solver, bitwuzla_solver): self.z3_solver = z3_solver self.bitwuzla_solver = bitwuzla_solver self.fallback = False self.stack = [] self.constraint = Values.TRUE() self.proven = {} self.unproven = {} def __str__(self): return f"{self.fallback}\n" + \ f"Stack: {self.stack}\n" + \ f"Constraint: {self.constraint}\n" + \ f"Proven: {self.proven}\n" + \ f"Unproven: {self.unproven}\n" def push(self): if self.fallback: if self.z3_solver: self.z3_solver.push() if self.bitwuzla_solver: self.bitwuzla_solver.push() else: # push before proving to enable fallback to other solvers self.stack.append((self.constraint, self.proven | self.unproven)) self.prove() # may trigger fallback to other solvers self.proven = {} assert not self.unproven if not self.fallback: # proving may have strengthened constraint _, proven = self.stack.pop() self.stack.append((self.constraint, proven)) Bitme_Solver.version = Bitme_Solver.bump Bitme_Solver.bump += 1 Bitme_Solver.versions[Bitme_Solver.version] = None def pop(self): if self.fallback: if self.z3_solver: self.z3_solver.pop() if self.bitwuzla_solver: self.bitwuzla_solver.pop() else: assert self.stack self.constraint, self.proven = self.stack.pop() self.unproven = {} del Bitme_Solver.versions[Bitme_Solver.version] Bitme_Solver.version = list(Bitme_Solver.versions)[-1] def assert_this(self, assertions, step): if self.fallback: if self.z3_solver: self.z3_solver.assert_this(assertions, step) if self.bitwuzla_solver: self.bitwuzla_solver.assert_this(assertions, step) else: for assertion in assertions: if step not in self.unproven: self.unproven[step] = {assertion:True} else: assert assertion not in self.unproven[step] self.unproven[step] |= {assertion:True} def assert_not_this(self, assertions, step): if self.fallback: if self.z3_solver: self.z3_solver.assert_not_this(assertions, step) if self.bitwuzla_solver: self.bitwuzla_solver.assert_not_this(assertions, step) else: for assertion in assertions: if step not in self.unproven: self.unproven[step] = {assertion:False} else: assert assertion not in self.unproven[step] self.unproven[step] |= {assertion:False} def simplify(self): if self.fallback: if self.z3_solver: self.z3_solver.simplify() if self.bitwuzla_solver: self.bitwuzla_solver.simplify() def solve(self): self.fallback = True self.constraint = Values.TRUE() self.proven |= self.unproven self.unproven = {} self.stack.append((None, self.proven)) for _, assertions in self.stack: for step in assertions: for assertion in assertions[step]: if assertions[step][assertion]: self.assert_this([assertion], step) else: self.assert_not_this([assertion], step) if assertions is not self.proven: # push with other solvers except for top of stack self.push() self.proven = {} self.stack = [] return self.prove() def cover(self): for step in self.unproven: if Variable.uncovered_steps and step > min(Variable.uncovered_steps): return else: for assertion in self.unproven[step]: assertion.wait_step(step) if Variable.uncovered_steps and step == min(Variable.uncovered_steps): if Bitme_Solver.version == 0: assert Bitme_Solver.versions == {0:None} Bitme_Solver.versions[Bitme_Solver.covered_version] = None Bitme_Solver.version = Bitme_Solver.covered_version Bitme_Solver.covered_step = step return def prove(self): if self.fallback: z3_SAT = False if self.z3_solver: result = self.z3_solver.prove() z3_SAT = self.z3_solver.is_SAT(result) if self.bitwuzla_solver: result = self.bitwuzla_solver.prove() bitwuzla_SAT = self.bitwuzla_solver.is_SAT(result) assert not self.z3_solver or z3_SAT == bitwuzla_SAT return bitwuzla_SAT return z3_SAT else: self.cover() for step in self.unproven: for assertion in self.unproven[step]: values = assertion.wait_step(step) if not isinstance(assertion, Transitional): # property or condition assert isinstance(values.sid_line, Bool) if isinstance(values, Values): if self.unproven[step][assertion] is True: self.constraint = values.And(self.constraint) else: assert self.unproven[step][assertion] is False self.constraint = values.Not().And(self.constraint) else: return self.solve() self.proven |= self.unproven self.unproven = {} return not self.constraint.is_always_false() def is_SAT(self, result): return result def is_UNSAT(self, result): return not result def assert_is_state_changing(self, next_line, step): if self.fallback: if self.z3_solver: self.z3_solver.assert_is_state_changing(next_line, step) if self.bitwuzla_solver: self.bitwuzla_solver.assert_is_state_changing(next_line, step) else: self.assert_this([next_line.is_state_changing()], step) def assert_state_is_not_changing(self, next_line, step): if self.fallback: if self.z3_solver: self.z3_solver.assert_state_is_not_changing(next_line, step) if self.bitwuzla_solver: self.bitwuzla_solver.assert_state_is_not_changing(next_line, step) else: self.assert_this([next_line.state_is_not_changing()], step) def print_pc(self, pc, step, level): if self.fallback: if self.z3_solver: self.z3_solver.print_pc(pc, step, level) if self.bitwuzla_solver: self.bitwuzla_solver.print_pc(pc, step, level) else: self.prove() pc_value = pc.get_values(step) print_message(f"{pc}\n", step, level) print_message("%s = %s\n" % (pc.get_step_name(step), pc_value), step, level) def print_inputs(self, inputs, step, level): if self.fallback: if self.z3_solver: self.z3_solver.print_inputs(inputs, step, level) if self.bitwuzla_solver: self.bitwuzla_solver.print_inputs(inputs, step, level) else: if Values.BVDD: print(self.constraint.bvdd.get_printed_inputs(True)) if Values.CFLOBVDD: print(self.constraint.cflobvdd.get_printed_inputs(True)) def eval_inputs(self, inputs, step): if self.fallback: if self.z3_solver: return self.z3_solver.eval_inputs(inputs, step) if self.bitwuzla_solver: return self.bitwuzla_solver.eval_inputs(inputs, step) elif Values.BVDD: sample = self.constraint.get_true_constraint().bvdd.sample_input_values() input_values = dict() for input_variable in inputs.values(): if input_variable in sample: input_values[input_variable.symbol] = sample[input_variable] del sample[input_variable] else: # The variable doesn't appear in our sample of the BVDD - this means any value will do input_values[input_variable.symbol] = 0x42 # ord("A"), but also a nice magic value assert len(sample) == 0, "sanity check: all branches of the BVDD must be on input values" return input_values else: # TODO pass # bitr concurrent bitme def fork(kmin, kmax, step): while step <= kmax: # assert all constraints for constraint in Constraint.constraints.values(): constraint.fork_step(step) if step >= kmin: # check all bad properties from kmin on for bad in Bad.bads.values(): bad.fork_step(step) for next_line in Next.nexts.values(): # compute next step next_line.fork_step(step) step += 1 # bitme bounded model checker def branching_bmc(solver, kmin, kmax, args, step, level): while step <= kmax or args.analyzor: # check model up to kmax steps # in analyzor mode we keep going until we find a bad input if args.print_pc and State.pc: # print current program counter value of single-core rotor model solver.print_pc(State.pc, step, level) # assert all constraints for constraint in Constraint.constraints.values(): print_message_with_propagation_profile(constraint.symbol, step, level) solver.assert_this([constraint], step) result = solver.prove() if solver.is_UNSAT(result): print_separator('v', step, level) print_message(f"{constraint}\n", step, level) if UNROLL or PROPAGATE is not None: print_message_with_propagation_profile("propagation profile\n", step, level) print_separator('^', step, level) return if step >= kmin: # check bad properties from kmin on for bad in Bad.bads.values(): print_message_with_propagation_profile(bad.symbol, step, level) solver.push() solver.assert_this([bad], step) result = solver.prove() if solver.is_SAT(result): print_separator('v', step, level) print_message(f"{bad}\n", step, level) solver.print_inputs(Variable.inputs, step, level) if UNROLL or PROPAGATE is not None: print_message_with_propagation_profile("propagation profile\n", step, level) print_separator('^', step, level) if args.analyzor: print("Found bad input; exiting from analyzor mode...") print(f"analyzor#step={step}") print(f"analyzor#bad={bad.symbol}") input_vals = solver.eval_inputs(Variable.inputs, step) for (name, val) in input_vals.items(): print(f"analyzor#input:{name}={val}") return solver.pop() if not args.unconstraining_bad: # assert all bad properties as negated constraints solver.assert_not_this(Bad.bads.values(), step) if args.check_termination and step >= kmin: state_change = False for next_line in Next.nexts.values(): # check if state changes solver.push() solver.assert_is_state_changing(next_line, step) result = solver.prove() solver.pop() if solver.is_SAT(result): state_change = True print_message(f"state change: {next_line}\n", step, level) # compute next step solver.assert_this([next_line], step) else: solver.assert_state_is_not_changing(next_line, step) if not state_change and next_line is list(Next.nexts.values())[-1]: print_message_with_propagation_profile("no states changed: terminating\n", step, level) return else: # compute next step solver.assert_this(Next.nexts.values(), step) if args.print_transition: print_message_with_propagation_profile("transitioning\n", step, level) else: print_message("transitioning", step, level) solver.simplify() if args.branching and Ite.branching_conditions and Ite.non_branching_conditions: print_message_with_propagation_profile("checking branching", step, level) solver.push() solver.assert_this([Ite.branching_conditions], step) branching_result = solver.is_SAT(solver.prove()) solver.pop() solver.push() solver.assert_not_this([Ite.non_branching_conditions], step) non_branching_result = solver.is_SAT(solver.prove()) solver.pop() if branching_result != non_branching_result: if branching_result: solver.assert_this([Ite.branching_conditions], step) elif non_branching_result: solver.assert_not_this([Ite.non_branching_conditions], step) if branching_result and non_branching_result: print_separator('v', step, level) print_message("branching:\n", step, level) solver.push() solver.assert_this([Ite.branching_conditions], step) branching_bmc(solver, kmin, kmax, args, step + 1, level + 1) solver.pop() print_separator('-', step, level) print_message("not branching:\n", step, level) solver.push() solver.assert_not_this([Ite.non_branching_conditions], step) branching_bmc(solver, kmin, kmax, args, step + 1, level + 1) solver.pop() print_separator('^', step, level) return step += 1 print_message_with_propagation_profile("reached kmax: terminating\n", step, level) def bmc(solver, kmin, kmax, args): print_separator('-') print_message(f"bitme bounded model checking: -kmin {kmin} -kmax {kmax}\n") print_separator('-') # initialize all states solver.assert_this(Init.inits.values(), 0) print_message("initializing", 0, 0) solver.prove() if args.use_bitr: fork(kmin, kmax, 0) branching_bmc(solver, kmin, kmax, args, 0, 0) print_separator('-') def ibmc(solver, kmin, kmax, imin, imax, args): assert 0 < imin <= imax for state in State.states.values(): if state.init_line is None: if state.next_line is not None: del Next.nexts[state.next_line.nid] print_separator('-') print_message(f"bitme incremental bounded model checking: -kmin {kmin} -kmax {kmax} -imin {imin} -imax {imax}\n") print_separator('-') # initialize all states solver.assert_this(Init.inits.values(), 0) print_message("initializing", 0, 0) solver.prove() Variable.incremental_number_of_input_variables = imin step = 0 while Variable.incremental_number_of_input_variables <= imax: print_message(f"{Variable.incremental_number_of_input_variables} incremental input variables at increment {step}\n") print_separator('-') if args.use_bitr: fork(kmin, kmax, step) branching_bmc(solver, kmin, kmax, args, step, 0) print_separator('-') assert not solver.stack if Variable.uncovered_steps: step = min(Variable.uncovered_steps) Variable.uncovered_steps = {} solver.constraint = Values.TRUE() solver.unproven = {} del Bitme_Solver.versions[Bitme_Solver.covered_version] Bitme_Solver.covered_version = Bitme_Solver.bump Bitme_Solver.bump += 1 Bitme_Solver.covered_step = 0 Bitme_Solver.version = 0 Variable.incremental_number_of_input_variables += 1 else: return import sys def try_rotor(): if is_rotor_present and len(sys.argv) > 1 and sys.argv[1] == '--rotor': # just run rotor argv = [sys.argv[0]] + sys.argv[2:] # remove --rotor but keep all other arguments rotor.main.argtypes = ctypes.c_int, ctypes.POINTER(ctypes.c_char_p) rotor.main(len(argv), (ctypes.c_char_p * len(argv))(*[arg.encode('utf-8') for arg in argv])) exit(0) import argparse def main(): try_rotor() parser = argparse.ArgumentParser(prog='bitme', description="bitme is a bounded model checker for BTOR2 models, see github.com/cksystemsteaching/selfie for more details.", epilog="bitme is designed to work with BTOR2 models generated by rotor for modeling RISC-V machines and RISC-V code.") parser.add_argument('modelfile', type=argparse.FileType('r')) parser.add_argument('outputfile', nargs='?', type=argparse.FileType('w', encoding='UTF-8')) parser.add_argument('-analyzor', action='store_true') parser.add_argument('--use-bitr', action='store_true') parser.add_argument('--use-Z3', action='store_true') parser.add_argument('--use-bitwuzla', action='store_true') parser.add_argument('--use-BVDD', action='store_true') parser.add_argument('--use-CFLOBVDD', nargs='*', type=int) parser.add_argument('--no-reduction', action='store_true') parser.add_argument('--substitute', action='store_true') parser.add_argument('--unroll', action='store_true') parser.add_argument('-propagate', nargs=1, type=int) parser.add_argument('-array', nargs=1, type=int) parser.add_argument('--recursive-array', action='store_true') parser.add_argument('-kmin', nargs=1, type=int) parser.add_argument('-kmax', nargs=1, type=int) parser.add_argument('-imin', nargs=1, type=int) parser.add_argument('-imax', nargs=1, type=int) parser.add_argument('--print-pc', action='store_true') # only for rotor models parser.add_argument('--check-termination', action='store_true') parser.add_argument('--unconstraining-bad', action='store_true') parser.add_argument('--print-transition', action='store_true') parser.add_argument('--branching', action='store_true') # only for rotor models args = parser.parse_args() global LAMBDAS LAMBDAS = not args.substitute global UNROLL UNROLL = args.unroll global PROPAGATE PROPAGATE = args.propagate[0] if args.propagate and args.propagate[0] >= 0 else None btor2.Array.ARRAY_SIZE_BOUND = args.array[0] if args.array else 0 btor2.Read.READ_ARRAY_ITERATIVELY = not args.recursive_array print_separator('#') are_there_state_transitions = ValuesParser().parse_btor2(args.modelfile, args.outputfile) if args.kmin or args.kmax or args.analyzor: kmin = args.kmin[0] if args.kmin else 0 kmax = args.kmax[0] if args.kmax else 0 if are_there_state_transitions: kmax = max(kmin, kmax) else: kmin = kmax = 0 imax = args.imax[0] if args.imax else len(Variable.input_indexes) if Variable.input_indexes else 1 imin = args.imin[0] if args.imin else imax assert 0 < imin <= imax Variable.incremental_number_of_input_variables = imin z3_solver = None bitwuzla_solver = None if z3interface.is_Z3_present: z3_solver = z3interface.Z3_Solver(print_message, LAMBDAS, UNROLL) if bitwuzlainterface.is_bitwuzla_present: bitwuzla_solver = bitwuzlainterface.Bitwuzla_Solver(print_message, LAMBDAS, UNROLL) if args.use_BVDD or args.use_CFLOBVDD is None: Values.BVDD = True Values.BVDD_number_of_inputs = len(Variable.input_indexes) if Variable.input_indexes else 1 print_separator('-') print(f"BVDD configuration: {Values.BVDD_number_of_inputs} input bytes") if args.use_CFLOBVDD is not None: Values.CFLOBVDD = True Values.CFLOBVDD_number_of_inputs = 2**ceil(log2(len(Variable.input_indexes))) if Variable.input_indexes else 1 level = ceil(log2(Values.CFLOBVDD_number_of_inputs)) Values.CFLOBVDD_fork_level = args.use_CFLOBVDD[0] if len(args.use_CFLOBVDD) > 0 else 0 Values.CFLOBVDD_swap_level = args.use_CFLOBVDD[1] if len(args.use_CFLOBVDD) > 1 else level Values.CFLOBVDD_level = args.use_CFLOBVDD[2] if len(args.use_CFLOBVDD) > 2 else Values.CFLOBVDD_swap_level assert 0 <= Values.CFLOBVDD_fork_level <= Values.CFLOBVDD_level, \ f"invalid fork level {Values.CFLOBVDD_fork_level} for level {Values.CFLOBVDD_level}" assert 0 <= Values.CFLOBVDD_swap_level <= Values.CFLOBVDD_level, \ f"invalid swap level {Values.CFLOBVDD_swap_level} for level {Values.CFLOBVDD_level}" CFLOBVDD.CFLOBVDD.level = Values.CFLOBVDD_level CFLOBVDD.CFLOBVDD.swap_level = Values.CFLOBVDD_swap_level CFLOBVDD.CFLOBVDD.fork_level = Values.CFLOBVDD_fork_level CFLOBVDD.CFLOBVDD.number_of_inputs = Values.CFLOBVDD_number_of_inputs print_separator('-') print(f"CFLOBVDD configuration: {Values.CFLOBVDD_number_of_inputs} input bytes " + f"@ level {Values.CFLOBVDD_level}, swap level {Values.CFLOBVDD_swap_level}, and fork level {Values.CFLOBVDD_fork_level}") CFLOBVDD.CFLOBVDD.REDUCE = not args.no_reduction bitme_solver = Bitme_Solver(z3_solver, bitwuzla_solver) if not args.use_Z3 and not args.use_bitwuzla: if Variable.input_indexes: ibmc(bitme_solver, kmin, kmax, imin, imax, args) else: print_separator('-') print("model input is unmapped, consider increasing -array") print_separator('#') return else: if args.use_Z3 and z3interface.is_Z3_present: bmc(z3_solver, kmin, kmax, args) if args.use_bitwuzla and bitwuzlainterface.is_bitwuzla_present: bmc(bitwuzla_solver, kmin, kmax, args) if Values.BVDD: BVDD.BVDD.print_profile() PDD.PDD.print_profile() if Values.CFLOBVDD: BVDD.BVDD.print_profile() CFLOBVDD.CFLOBVDD.print_profile() PDD.PDD.print_profile() print_separator('#') if __name__ == '__main__': main()