tools/btor2.py
Rama main · réplica de lectura del repositorio original.
#!/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. For further information and code please refer to:
# selfie.cs.uni-salzburg.at
# BTOR2 parser
# ------------------------------------------------------------
import math
# supported BTOR2 keywords and operators
def init_btor2_keywords_operators():
global BITVEC
global ARRAY
global OP_SORT
global OP_ZERO
global OP_ONE
global OP_CONST
global OP_CONSTD
global OP_CONSTH
global OP_INPUT
global OP_STATE
global OP_INIT
global OP_NEXT
global OP_SEXT
global OP_UEXT
global OP_SLICE
global OP_NOT
global OP_INC
global OP_DEC
global OP_NEG
global OP_IMPLIES
global OP_EQ
global OP_NEQ
global OP_SGT
global OP_UGT
global OP_SGTE
global OP_UGTE
global OP_SLT
global OP_ULT
global OP_SLTE
global OP_ULTE
global OP_AND
global OP_OR
global OP_XOR
global OP_SLL
global OP_SRL
global OP_SRA
global OP_ADD
global OP_SUB
global OP_MUL
global OP_SDIV
global OP_UDIV
global OP_SREM
global OP_UREM
global OP_CONCAT
global OP_READ
global OP_ITE
global OP_WRITE
global OP_BAD
global OP_CONSTRAINT
BITVEC = 'bitvec'
ARRAY = 'array'
OP_SORT = 'sort'
OP_ZERO = 'zero'
OP_ONE = 'one'
OP_CONST = 'const'
OP_CONSTD = 'constd'
OP_CONSTH = 'consth'
OP_INPUT = 'input'
OP_STATE = 'state'
OP_INIT = 'init'
OP_NEXT = 'next'
OP_SEXT = 'sext'
OP_UEXT = 'uext'
OP_SLICE = 'slice'
OP_NOT = 'not'
OP_INC = 'inc'
OP_DEC = 'dec'
OP_NEG = 'neg'
OP_IMPLIES = 'implies'
OP_EQ = 'eq'
OP_NEQ = 'neq'
OP_SGT = 'sgt'
OP_UGT = 'ugt'
OP_SGTE = 'sgte'
OP_UGTE = 'ugte'
OP_SLT = 'slt'
OP_ULT = 'ult'
OP_SLTE = 'slte'
OP_ULTE = 'ulte'
OP_AND = 'and'
OP_OR = 'or'
OP_XOR = 'xor'
OP_SLL = 'sll'
OP_SRL = 'srl'
OP_SRA = 'sra'
OP_ADD = 'add'
OP_SUB = 'sub'
OP_MUL = 'mul'
OP_SDIV = 'sdiv'
OP_UDIV = 'udiv'
OP_SREM = 'srem'
OP_UREM = 'urem'
OP_CONCAT = 'concat'
OP_READ = 'read'
OP_ITE = 'ite'
OP_WRITE = 'write'
OP_BAD = 'bad'
OP_CONSTRAINT = 'constraint'
init_btor2_keywords_operators()
class model_error(Exception):
def __init__(self, expected, line_no):
super().__init__(f"model error in line {line_no}: {expected} expected")
class Line:
lines = {}
count = 0
def __init__(self, nid, comment, line_no):
self.nid = nid
self.comment = "; " + comment if comment and comment[0] != ';' else comment
self.line_no = line_no
self.new_line()
def __repr__(self):
return self.__str__()
def new_line(self):
if self.nid is not None:
assert self.nid not in Line.lines, f"nid {self.nid} already defined @ {self.line_no}"
Line.lines[self.nid] = self
type(self).count += 1
def is_defined(nid):
return nid in Line.lines
def get(nid):
assert Line.is_defined(nid), f"undefined nid {self.nid} @ {self.line_no}"
return Line.lines[nid]
class Sort(Line):
keyword = OP_SORT
def __init__(self, nid, comment, line_no):
super().__init__(nid, comment, line_no)
def match_sorts(self, sort):
return type(self) is type(sort)
class Bitvector(Sort):
keyword = BITVEC
def __init__(self, nid, size, comment, line_no):
assert size > 0
super().__init__(nid, comment, line_no)
self.size = size
def __str__(self):
return f"{self.nid} {Sort.keyword} {Bitvec.keyword} {self.size} {self.comment}"
def match_init_sorts(self, sort):
return self.match_sorts(sort)
def is_mapped_array(self):
return False
def is_unsigned_value(self, value):
return 0 <= value < 2**self.size
def is_signed_value(self, value):
return -2**(self.size - 1) <= value < 2**(self.size - 1)
def is_value(self, value):
return self.is_unsigned_value(value) or self.is_signed_value(value)
def get_unsigned_value(self, value):
assert self.is_value(value)
return 2**self.size + value if value < 0 else value
def get_signed_value(self, value):
assert self.is_value(value)
return value - 2**self.size if value >= 2**(self.size - 1) else value
class Bool(Bitvector):
boolean = None
def __init__(self, nid, comment, line_no):
super().__init__(nid, 1, comment, line_no)
assert Bool.boolean is None
Bool.boolean = self
class Bitvec(Bitvector):
def __init__(self, nid, size, comment, line_no):
super().__init__(nid, size, comment, line_no)
def match_sorts(self, sort):
return super().match_sorts(sort) and self.size == sort.size
class Array(Sort):
keyword = ARRAY
# map arrays up to size bound to bitvectors
ARRAY_SIZE_BOUND = 0 # array size in bits
number_of_variable_arrays = 0
number_of_mapped_arrays = 0
def __init__(self, nid, array_size_line, element_size_line, comment, line_no):
super().__init__(nid, comment, line_no)
self.array_size_line = array_size_line
self.element_size_line = element_size_line
if not isinstance(array_size_line, Bitvec):
raise model_error("array size bitvector", line_no)
if not isinstance(element_size_line, Bitvec):
raise model_error("element size bitvector", line_no)
def __str__(self):
return f"{self.nid} {Sort.keyword} {Array.keyword} {self.array_size_line.nid} {self.element_size_line.nid} {self.comment}"
def match_sorts(self, sort):
return (super().match_sorts(sort)
and self.array_size_line.match_sorts(sort.array_size_line)
and self.element_size_line.match_sorts(sort.element_size_line))
def match_init_sorts(self, sort):
# allow constant arrays: array init with bitvector
return (self.match_sorts(sort)
or (isinstance(sort, Bitvec) and self.element_size_line.match_sorts(sort)))
def is_mapped_array(self):
return self.array_size_line.size <= Array.ARRAY_SIZE_BOUND
def accommodate_array_indexes(nid):
if Array.ARRAY_SIZE_BOUND == 0:
return nid
else:
# shift left by log10(2**n + 1) decimal digits where n is the array index space
return nid * 10**(math.floor(math.log10(2**Array.ARRAY_SIZE_BOUND + 1)) + 1)
class Expression(Line):
total_number_of_generated_expressions = 0
def __init__(self, nid, sid_line, domain, depth, comment, line_no):
super().__init__(nid, comment, line_no)
self.sid_line = sid_line
self.domain = domain
self.depth = depth
if not isinstance(sid_line, Sort):
raise model_error("sort", line_no)
def print_deep(self):
print(self)
def get_domain(self):
# filter out uninitialized states
return [state for state in self.domain if state.init_line is not None]
class Constant(Expression):
def __init__(self, nid, sid_line, value, comment, line_no):
super().__init__(nid, sid_line, {}, 0, comment, line_no)
if not sid_line.is_value(value):
raise model_error(f"{value} in range of {sid_line.size}-bit bitvector", line_no)
self.print_value = value
self.signed_value = sid_line.get_signed_value(value)
self.value = sid_line.get_unsigned_value(value)
def print_deep(self):
print(self)
def get_mapped_array_expression_for(self, index):
return self
class Zero(Constant):
keyword = OP_ZERO
def __init__(self, nid, sid_line, symbol, comment, line_no):
super().__init__(nid, sid_line, 0, comment, line_no)
self.symbol = symbol
def __str__(self):
if self.symbol:
return f"{self.nid} {Zero.keyword} {self.sid_line.nid} {self.symbol} {self.comment}"
else:
return f"{self.nid} {Zero.keyword} {self.sid_line.nid} {self.comment}"
class One(Constant):
keyword = OP_ONE
def __init__(self, nid, sid_line, symbol, comment, line_no):
super().__init__(nid, sid_line, 1, comment, line_no)
self.symbol = symbol
def __str__(self):
if self.symbol:
return f"{self.nid} {One.keyword} {self.sid_line.nid} {self.symbol} {self.comment}"
else:
return f"{self.nid} {One.keyword} {self.sid_line.nid} {self.comment}"
class Constd(Constant):
keyword = OP_CONSTD
def __init__(self, nid, sid_line, value, comment, line_no):
super().__init__(nid, sid_line, value, comment, line_no)
def __str__(self):
return f"{self.nid} {Constd.keyword} {self.sid_line.nid} {self.print_value} {self.comment}"
class Const(Constant):
keyword = OP_CONST
def __init__(self, nid, sid_line, value, comment, line_no):
super().__init__(nid, sid_line, value, comment, line_no)
def __str__(self):
size = self.sid_line.size
return f"{self.nid} {Const.keyword} {self.sid_line.nid} {self.value:0{size}b} {self.comment}"
class Consth(Constant):
keyword = OP_CONSTH
def __init__(self, nid, sid_line, value, comment, line_no):
super().__init__(nid, sid_line, value, comment, line_no)
def __str__(self):
size = math.ceil(self.sid_line.size / 4)
return f"{self.nid} {Consth.keyword} {self.sid_line.nid} {self.value:0{size}X} {self.comment}"
class Constant_Array(Expression):
def __init__(self, sid_line, constant_line):
super().__init__(None, sid_line, {}, 0, constant_line.comment, constant_line.line_no)
self.nid = constant_line.nid # reuse nid of constant_line
self.constant_line = constant_line
if not isinstance(sid_line, Array):
raise model_error("array sort", line_no)
if not isinstance(constant_line, Constant):
raise model_error("bitvector constant", line_no)
if not sid_line.element_size_line.match_sorts(constant_line.sid_line):
raise model_error("compatible sorts", line_no)
def __str__(self):
return f"{self.nid} {"consta"} {self.sid_line.nid} {self.constant_line.nid} {self.comment}"
def get_mapped_array_expression_for(self, index):
if index is not None:
assert self.sid_line.is_mapped_array()
return self.constant_line
else:
assert not self.sid_line.is_mapped_array()
return self
class Variable(Expression):
keywords = {OP_INPUT, OP_STATE}
inputs = {}
input_indexes = {}
def __init__(self, nid, sid_line, domain, symbol, comment, line_no, index):
super().__init__(nid, sid_line, domain, 0, comment, line_no)
self.symbol = symbol
if isinstance(sid_line, Array):
Array.number_of_variable_arrays += 1
self.new_mapped_array(index)
def __lt__(self, variable):
# ordering variables for constructing model input
return self.nid < variable.nid
def new_mapped_array(self, index):
self.index = index
self.input_index = None
if index is not None:
if not isinstance(self.sid_line, Bitvector):
raise model_error("bitvector", self.line_no)
elif self.sid_line.is_mapped_array():
Array.number_of_mapped_arrays += 1
self.array = {}
for index in range(2**self.sid_line.array_size_line.size):
self.array[index] = type(self)(self.nid + index + 1, self.sid_line.element_size_line,
f"{self.symbol}-{index}", f"{self.comment} @ index {index}", self.line_no, index)
def new_input(self, index):
if index is not None or not self.sid_line.is_mapped_array():
assert self.nid not in Variable.inputs, f"variable nid {self.nid} already defined @ {self.line_no}"
Variable.inputs[self.nid] = self
if isinstance(self.sid_line, Bitvector) and self.sid_line.size == 8:
self.input_index = len(Variable.input_indexes)
Variable.input_indexes[self.input_index] = self
def get_mapped_array_expression_for(self, index):
if index is not None:
assert self.sid_line.is_mapped_array()
return self.array[index]
else:
assert not self.sid_line.is_mapped_array()
return self
class Input(Variable):
keyword = OP_INPUT
def __init__(self, nid, sid_line, symbol, comment, line_no, index = None):
super().__init__(nid, sid_line, {}, symbol, comment, line_no, index)
self.name = f"input{self.nid}"
self.new_input(index)
def __str__(self):
return f"{self.nid} {Input.keyword} {self.sid_line.nid} {self.symbol} {self.comment}"
class State(Variable):
keyword = OP_STATE
states = {}
pc = None
def __init__(self, nid, sid_line, symbol, comment, line_no, index = None):
# domain is ordered set by using dictionary with None values
super().__init__(nid, sid_line, {self:None}, symbol, comment, line_no, index)
self.name = f"state{self.nid}"
self.init_line = None
self.next_line = None
self.new_state(index)
# rotor-dependent program counter declaration
if comment == "; program counter":
State.pc = self
def __str__(self):
return f"{self.nid} {State.keyword} {self.sid_line.nid} {self.symbol} {self.comment}"
def new_state(self, index):
if index is not None or not self.sid_line.is_mapped_array():
assert self.nid not in State.states, f"state nid {self.nid} already defined @ {self.line_no}"
State.states[self.nid] = self
def remove_state(self):
for key in State.states.keys():
if State.states[key] is self:
del State.states[key]
return
def get_mapped_array_expression_for(self, index):
if isinstance(self.sid_line, Bitvector) or self.sid_line.is_mapped_array():
if self.init_line is not None and self.next_line is not None and self.next_line.exp_line is self:
# propagate initial value of initialized read-only bitvector states
return self.init_line.exp_line.get_mapped_array_expression_for(index)
return super().get_mapped_array_expression_for(index)
class Indexed(Expression):
def __init__(self, nid, sid_line, arg1_line, comment, line_no):
super().__init__(nid, sid_line, arg1_line.domain, arg1_line.depth + 1, comment, line_no)
self.arg1_line = arg1_line
if not isinstance(arg1_line, Expression):
raise model_error("expression operand", line_no)
if not isinstance(sid_line, Bitvec):
raise model_error("bitvector result", line_no)
if not isinstance(arg1_line.sid_line, Bitvec):
raise model_error("bitvector operand", line_no)
def print_deep(self):
self.arg1_line.print_deep()
print(self)
def get_mapped_array_expression_for(self, index):
assert index is None
arg1_line = self.arg1_line.get_mapped_array_expression_for(None)
return self.copy(arg1_line)
class Ext(Indexed):
keywords = {OP_SEXT, OP_UEXT}
def __init__(self, nid, op, sid_line, arg1_line, w, comment, line_no):
super().__init__(nid, sid_line, arg1_line, comment, line_no)
assert op in Ext.keywords
self.op = op
self.w = w
if sid_line.size != arg1_line.sid_line.size + w:
raise model_error("compatible bitvector sorts", line_no)
def __str__(self):
return f"{self.nid} {self.op} {self.sid_line.nid} {self.arg1_line.nid} {self.w} {self.comment}"
def copy(self, arg1_line):
if self.arg1_line is not arg1_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), self.op, self.sid_line, arg1_line, self.w, self.comment, self.line_no)
else:
return self
class Slice(Indexed):
keyword = OP_SLICE
def __init__(self, nid, sid_line, arg1_line, u, l, comment, line_no):
super().__init__(nid, sid_line, arg1_line, comment, line_no)
self.u = u
self.l = l
if u >= arg1_line.sid_line.size:
raise model_error("upper bit in range", line_no)
if u < l:
raise model_error("upper bit >= lower bit", line_no)
if sid_line.size != u - l + 1:
raise model_error("compatible bitvector sorts", line_no)
def __str__(self):
return f"{self.nid} {Slice.keyword} {self.sid_line.nid} {self.arg1_line.nid} {self.u} {self.l} {self.comment}"
def copy(self, arg1_line):
if self.arg1_line is not arg1_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), self.sid_line, arg1_line, self.u, self.l, self.comment, self.line_no)
else:
return self
class Unary(Expression):
keywords = {OP_NOT, OP_INC, OP_DEC, OP_NEG}
def __init__(self, nid, op, sid_line, arg1_line, comment, line_no):
super().__init__(nid, sid_line, arg1_line.domain, arg1_line.depth + 1, comment, line_no)
assert op in Unary.keywords
self.op = op
self.arg1_line = arg1_line
if not isinstance(arg1_line, Expression):
raise model_error("expression operand", line_no)
if op == 'not' and not isinstance(sid_line, Bitvector):
raise model_error("Boolean or bitvector result", line_no)
if op != 'not' and not isinstance(sid_line, Bitvec):
raise model_error("bitvector result", line_no)
if not sid_line.match_sorts(arg1_line.sid_line):
raise model_error("compatible sorts", line_no)
def __str__(self):
return f"{self.nid} {self.op} {self.sid_line.nid} {self.arg1_line.nid} {self.comment}"
def print_deep(self):
self.arg1_line.print_deep()
print(self)
def copy(self, arg1_line):
if self.arg1_line is not arg1_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), self.op, self.sid_line, arg1_line, self.comment, self.line_no)
else:
return self
def get_mapped_array_expression_for(self, index):
assert index is None
arg1_line = self.arg1_line.get_mapped_array_expression_for(None)
return self.copy(arg1_line)
class Binary(Expression):
keywords = {OP_IMPLIES, OP_EQ, OP_NEQ, OP_SGT, OP_UGT, OP_SGTE, OP_UGTE, OP_SLT, OP_ULT, OP_SLTE, OP_ULTE, OP_AND, OP_OR, OP_XOR, OP_SLL, OP_SRL, OP_SRA, OP_ADD, OP_SUB, OP_MUL, OP_SDIV, OP_UDIV, OP_SREM, OP_UREM, OP_CONCAT, OP_READ}
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
super().__init__(nid, sid_line, arg1_line.domain | arg2_line.domain,
max(arg1_line.depth, arg2_line.depth) + 1, comment, line_no)
assert op in Binary.keywords
self.op = op
self.arg1_line = arg1_line
self.arg2_line = arg2_line
if not isinstance(arg1_line, Expression):
raise model_error("expression left operand", line_no)
if not isinstance(arg2_line, Expression):
raise model_error("expression right operand", line_no)
def __str__(self):
return f"{self.nid} {self.op} {self.sid_line.nid} {self.arg1_line.nid} {self.arg2_line.nid} {self.comment}"
def print_deep(self):
self.arg1_line.print_deep()
self.arg2_line.print_deep()
print(self)
def copy(self, arg1_line, arg2_line):
if self.arg1_line is not arg1_line or self.arg2_line is not arg2_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), self.op, self.sid_line, arg1_line, arg2_line, self.comment, self.line_no)
else:
return self
def get_mapped_array_expression_for(self, index):
assert index is None
arg1_line = self.arg1_line.get_mapped_array_expression_for(None)
arg2_line = self.arg2_line.get_mapped_array_expression_for(None)
return self.copy(arg1_line, arg2_line)
class Implies(Binary):
keyword = OP_IMPLIES
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op == Implies.keyword
super().__init__(nid, Implies.keyword, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(sid_line, Bool):
raise model_error("Boolean result", line_no)
if not sid_line.match_sorts(arg1_line.sid_line):
raise model_error("compatible result and first operand sorts", line_no)
if not arg1_line.sid_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first and second operand sorts", line_no)
class Comparison(Binary):
keywords = {OP_EQ, OP_NEQ, OP_SGT, OP_UGT, OP_SGTE, OP_UGTE, OP_SLT, OP_ULT, OP_SLTE, OP_ULTE}
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op in Comparison.keywords
super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(sid_line, Bool):
raise model_error("Boolean result", line_no)
if (op in {OP_SGT, OP_UGT, OP_SGTE, OP_UGTE, OP_SLT, OP_ULT, OP_SLTE, OP_ULTE} and
not isinstance(arg1_line.sid_line, Bitvec)):
raise model_error("bitvector first operand", line_no)
if not arg1_line.sid_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first and second operand sorts", line_no)
class Logical(Binary):
keywords = {OP_AND, OP_OR, OP_XOR}
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op in Logical.keywords
super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(sid_line, Bitvector):
raise model_error("Boolean or bitvector result", line_no)
if not sid_line.match_sorts(arg1_line.sid_line):
raise model_error("compatible result and first operand sorts", line_no)
if not arg1_line.sid_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first and second operand sorts", line_no)
class Computation(Binary):
keywords = {OP_SLL, OP_SRL, OP_SRA, OP_ADD, OP_SUB, OP_MUL, OP_SDIV, OP_UDIV, OP_SREM, OP_UREM}
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op in Computation.keywords
super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(sid_line, Bitvec):
raise model_error("bitvector result", line_no)
if not sid_line.match_sorts(arg1_line.sid_line):
raise model_error("compatible result and first operand sorts", line_no)
if not arg1_line.sid_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first and second operand sorts", line_no)
class Concat(Binary):
keyword = OP_CONCAT
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op == Concat.keyword
super().__init__(nid, Concat.keyword, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(sid_line, Bitvec):
raise model_error("bitvector result", line_no)
if not isinstance(arg1_line.sid_line, Bitvec):
raise model_error("bitvector first operand", line_no)
if not isinstance(arg2_line.sid_line, Bitvec):
raise model_error("bitvector second operand", line_no)
if sid_line.size != arg1_line.sid_line.size + arg2_line.sid_line.size:
raise model_error("compatible bitvector result", line_no)
class Read(Binary):
keyword = OP_READ
READ_ARRAY_ITERATIVELY = True
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no):
assert op == Read.keyword
super().__init__(nid, Read.keyword, sid_line, arg1_line, arg2_line, comment, line_no)
if not isinstance(arg1_line.sid_line, Array):
raise model_error("array first operand", line_no)
if not arg1_line.sid_line.array_size_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first operand array size and second operand sorts", line_no)
if not sid_line.match_sorts(arg1_line.sid_line.element_size_line):
raise model_error("compatible result and first operand element size sorts", line_no)
self.read_cache = None
def read_array_iterative(self, array_line, index_line):
for index in range(2**array_line.sid_line.array_size_line.size):
if index == 0:
read_line = array_line.get_mapped_array_expression_for(0)
else:
read_line = Parser.parser.get_class(Ite)(Parser.next_nid(), self.sid_line,
Parser.parser.get_class(Comparison)(Parser.next_nid(), OP_EQ, Bool.boolean,
index_line,
Parser.parser.get_class(Constd)(Parser.next_nid(), index_line.sid_line,
index, f"index {index}", self.line_no),
f"is address equal to index {index}?", self.line_no),
array_line.get_mapped_array_expression_for(index),
read_line,
f"read value from {array_line.comment[2:]} @ address if equal to index {index}", self.line_no)
return read_line
def read_array_recursive(self, array_line, index_line, index_array, zero_line):
assert 2 <= len(index_array) == 2**math.log2(len(index_array))
if len(index_array) == 2:
even_line = array_line.get_mapped_array_expression_for(index_array[0])
odd_line = array_line.get_mapped_array_expression_for(index_array[1])
else:
even_line = self.read_array_recursive(array_line, index_line,
index_array[0:len(index_array)//2], zero_line)
odd_line = self.read_array_recursive(array_line, index_line,
index_array[len(index_array)//2:len(index_array)], zero_line)
address_bit = int(math.log2(len(index_array))) - 1
return Parser.parser.get_class(Ite)(Parser.next_nid(), self.sid_line,
Parser.parser.get_class(Comparison)(Parser.next_nid(), OP_EQ, Bool.boolean,
Parser.parser.get_class(Slice)(Parser.next_nid(), zero_line.sid_line, index_line,
address_bit, address_bit,
f"extract {address_bit}-th address bit", self.line_no),
zero_line,
f"is {address_bit}-th address bit set?", self.line_no),
even_line,
odd_line,
f"read value from {array_line.comment[2:]} @ reset or set {address_bit}-th address bit", self.line_no)
def read_array(self, array_line, index_line):
if array_line.sid_line.is_mapped_array():
if isinstance(index_line, Constant):
return array_line.get_mapped_array_expression_for(index_line.value)
else:
if Read.READ_ARRAY_ITERATIVELY:
return self.read_array_iterative(array_line, index_line)
else:
return self.read_array_recursive(array_line, index_line,
list(range(2**array_line.sid_line.array_size_line.size)),
Parser.parser.get_class(Zero)(Parser.next_nid(),
Parser.parser.get_class(Bitvec)(Parser.next_nid(), 1, "1-bit bitvector for testing bits", self.line_no),
"", "zero value for testing bits", self.line_no))
else:
return self.copy(array_line.get_mapped_array_expression_for(None), index_line)
def get_mapped_array_expression_for(self, index):
assert index is None
if self.read_cache is None: # avoids quadratic blowup in mapped array size
arg1_line = self.arg1_line # map later when index is known
arg2_line = self.arg2_line.get_mapped_array_expression_for(None)
self.read_cache = self.read_array(arg1_line, arg2_line)
return self.read_cache
class Ternary(Expression):
keywords = {OP_ITE, OP_WRITE}
def __init__(self, nid, op, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no):
super().__init__(nid, sid_line, arg1_line.domain | arg2_line.domain | arg3_line.domain,
max(arg1_line.depth, arg2_line.depth, arg3_line.depth) + 1, comment, line_no)
assert op in Ternary.keywords
self.op = op
self.arg1_line = arg1_line
self.arg2_line = arg2_line
self.arg3_line = arg3_line
if not isinstance(arg1_line, Expression):
raise model_error("expression first operand", line_no)
if not isinstance(arg2_line, Expression):
raise model_error("expression second operand", line_no)
if not isinstance(arg3_line, Expression):
raise model_error("expression third operand", line_no)
def __str__(self):
return f"{self.nid} {self.op} {self.sid_line.nid} {self.arg1_line.nid} {self.arg2_line.nid} {self.arg3_line.nid} {self.comment}"
def print_deep(self):
self.arg1_line.print_deep()
self.arg2_line.print_deep()
self.arg3_line.print_deep()
print(self)
class Ite(Ternary):
keyword = OP_ITE
branching_conditions = None
non_branching_conditions = None
def __init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no):
super().__init__(nid, Ite.keyword, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no)
if not isinstance(arg1_line.sid_line, Bool):
raise model_error("Boolean first operand", line_no)
if not sid_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible result and second operand sorts", line_no)
if not arg2_line.sid_line.match_sorts(arg3_line.sid_line):
raise model_error("compatible second and third operand sorts", line_no)
self.ite_cache = {}
if Ite.branching_conditions is None and comment == "; branch true condition":
Ite.branching_conditions = self
elif Ite.non_branching_conditions is None and comment == "; branch false condition":
Ite.non_branching_conditions = self
def copy(self, arg1_line, arg2_line, arg3_line):
if self.arg1_line is not arg1_line or self.arg2_line is not arg2_line or self.arg3_line is not arg3_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), arg2_line.sid_line, arg1_line, arg2_line, arg3_line, self.comment, self.line_no)
else:
return self
def get_mapped_array_expression_for(self, index):
if index not in self.ite_cache:
arg1_line = self.arg1_line.get_mapped_array_expression_for(None)
arg2_line = self.arg2_line.get_mapped_array_expression_for(index)
arg3_line = self.arg3_line.get_mapped_array_expression_for(index)
self.ite_cache[index] = self.copy(arg1_line, arg2_line, arg3_line)
return self.ite_cache[index]
class Write(Ternary):
keyword = OP_WRITE
def __init__(self, nid, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no):
super().__init__(nid, Write.keyword, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no)
if not isinstance(sid_line, Array):
raise model_error("array result", line_no)
if not sid_line.match_sorts(arg1_line.sid_line):
raise model_error("compatible result and first operand sorts", line_no)
if not arg1_line.sid_line.array_size_line.match_sorts(arg2_line.sid_line):
raise model_error("compatible first operand array size and second operand sorts", line_no)
if not arg1_line.sid_line.element_size_line.match_sorts(arg3_line.sid_line):
raise model_error("compatible first operand element size and third operand sorts", line_no)
self.write_cache = {}
def copy(self, arg1_line, arg2_line, arg3_line):
if self.arg1_line is not arg1_line or self.arg2_line is not arg2_line or self.arg3_line is not arg3_line:
Expression.total_number_of_generated_expressions += 1
return type(self)(Parser.next_nid(), arg1_line.sid_line, arg1_line, arg2_line, arg3_line, self.comment, self.line_no)
else:
return self
def write_array(self, array_line, index_line, value_line, index):
if self.sid_line.is_mapped_array():
assert index is not None
if isinstance(index_line, Constant):
if index_line.value == index:
return value_line
else:
return array_line
else:
return Parser.parser.get_class(Ite)(Parser.next_nid(), value_line.sid_line,
Parser.parser.get_class(Comparison)(Parser.next_nid(), OP_EQ, Bool.boolean,
index_line,
Parser.parser.get_class(Constd)(Parser.next_nid(), index_line.sid_line,
index, f"index {index}", self.line_no),
f"is address equal to index {index}?", self.line_no),
value_line,
array_line,
f"write value to {array_line.comment[2:]} @ address if equal to index {index}", self.line_no)
else:
assert index is None
return self.copy(array_line, index_line, value_line)
def get_mapped_array_expression_for(self, index):
if index not in self.write_cache:
arg1_line = self.arg1_line.get_mapped_array_expression_for(index)
arg2_line = self.arg2_line.get_mapped_array_expression_for(None)
arg3_line = self.arg3_line.get_mapped_array_expression_for(None)
self.write_cache[index] = self.write_array(arg1_line, arg2_line, arg3_line, index)
return self.write_cache[index]
class Transitional(Line):
def __init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line, index):
super().__init__(nid, comment, line_no)
self.sid_line = sid_line
self.state_line = state_line
self.exp_line = exp_line
self.symbol = symbol
if not isinstance(sid_line, Sort):
raise model_error("sort", line_no)
if not isinstance(state_line, State):
raise model_error("state operand", line_no)
if not isinstance(exp_line, Expression):
raise model_error("expression operand", line_no)
if not self.sid_line.match_sorts(state_line.sid_line):
raise model_error("compatible line and state sorts", line_no)
if not state_line.sid_line.match_init_sorts(exp_line.sid_line):
raise model_error("compatible state and expression sorts", line_no)
self.new_mapped_array(array_line, index)
def new_mapped_array(self, array_line, index):
self.array_line = array_line
self.index = index
if index is not None:
if not isinstance(self.sid_line, Bitvector):
raise model_error("bitvector", self.line_no)
elif self.sid_line.is_mapped_array():
self.array = {}
for index in self.state_line.array.keys():
self.array[index] = type(self)(self.nid + index + 1, self.sid_line.element_size_line,
self.state_line.array[index], self.state_line.array[index], self.symbol,
f"{self.comment} @ index {index}", self.line_no, self, index)
def set_mapped_array_expression(self):
if self.index is None:
self.exp_line = self.exp_line.get_mapped_array_expression_for(None)
else:
self.exp_line = self.array_line.exp_line.get_mapped_array_expression_for(self.index)
def remove_transition(state_line, transitions):
for key in transitions.keys():
if transitions[key].state_line is state_line:
del transitions[key]
return
def new_transition(self, transitions, index):
if index is not None or not self.sid_line.is_mapped_array():
assert self.nid not in transitions, f"transition nid {self.nid} already defined @ {self.line_no}"
transitions[self.nid] = self
class Init(Transitional):
keyword = OP_INIT
inits = {}
def __init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line = None, index = None):
if isinstance(state_line.sid_line, Array) and isinstance(exp_line, Constant):
exp_line = Parser.parser.get_class(Constant_Array)(state_line.sid_line, exp_line)
super().__init__(nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line, index)
if state_line.nid < exp_line.nid:
raise model_error("state after expression", line_no)
if isinstance(state_line, Input):
raise model_error("state, not input", line_no)
if self.state_line.init_line is None:
self.state_line.init_line = self
else:
raise model_error("uninitialized state", line_no)
self.new_transition(Init.inits, index)
def __str__(self):
if self.symbol:
return f"{self.nid} {Init.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.symbol} {self.comment}"
else:
return f"{self.nid} {Init.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.comment}"
class Next(Transitional):
keyword = OP_NEXT
nexts = {}
def __init__(self, nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line = None, index = None):
super().__init__(nid, sid_line, state_line, exp_line, symbol, comment, line_no, array_line, index)
if self.state_line.next_line is None:
self.state_line.next_line = self
else:
raise model_error("untransitioned state", line_no)
self.new_transition(Next.nexts, index)
def __str__(self):
if self.symbol:
return f"{self.nid} {Next.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.symbol} {self.comment}"
else:
return f"{self.nid} {Next.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.comment}"
class Property(Line):
keywords = {OP_CONSTRAINT, OP_BAD}
def __init__(self, nid, property_line, symbol, comment, line_no):
super().__init__(nid, comment, line_no)
self.property_line = property_line
self.symbol = symbol
if not isinstance(property_line, Expression):
raise model_error("expression operand", line_no)
if not isinstance(property_line.sid_line, Bool):
raise model_error("Boolean operand", line_no)
def set_mapped_array_expression(self):
self.property_line = self.property_line.get_mapped_array_expression_for(None)
class Constraint(Property):
keyword = OP_CONSTRAINT
constraints = {}
def __init__(self, nid, property_line, symbol, comment, line_no):
super().__init__(nid, property_line, symbol, comment, line_no)
self.new_constraint()
def __str__(self):
return f"{self.nid} {Constraint.keyword} {self.property_line.nid} {self.symbol} {self.comment}"
def new_constraint(self):
assert self not in Constraint.constraints, f"constraint nid {self.nid} already defined @ {self.line_no}"
Constraint.constraints[self.nid] = self
class Bad(Property):
keyword = OP_BAD
bads = {}
def __init__(self, nid, property_line, symbol, comment, line_no):
super().__init__(nid, property_line, symbol, comment, line_no)
self.new_bad()
def __str__(self):
return f"{self.nid} {Bad.keyword} {self.property_line.nid} {self.symbol} {self.comment}"
def new_bad(self):
assert self.nid not in Bad.bads, f"bad nid {self.nid} already defined @ {self.line_no}"
Bad.bads[self.nid] = self
# BTOR2 parser
class syntax_error(Exception):
def __init__(self, expected, line_no):
super().__init__(f"syntax error in line {line_no}: {expected} expected")
import re
class Parser:
parser = None
current_nid = 0
def next_nid(nid = None):
if nid is None:
Parser.current_nid += 1
return Parser.current_nid
else:
return nid
def tokenize_btor2(line):
# comment, non-comment no-space printable string,
# signed integer, binary number, hexadecimal number
btor2_token_pattern = r"(;.*|[^; \n\r]+|-?\d+|[0-1]|[0-9a-fA-F]+)"
tokens = re.findall(btor2_token_pattern, line)
return tokens
def get_token(tokens, expected, line_no):
try:
return tokens.pop(0)
except:
raise syntax_error(expected, line_no)
def get_decimal(tokens, expected, line_no):
token = Parser.get_token(tokens, expected, line_no)
if token.isdecimal():
return int(token)
else:
raise syntax_error(expected, line_no)
def get_nid(tokens, expected, line_no):
return Array.accommodate_array_indexes(Parser.get_decimal(tokens, expected, line_no))
def get_nid_line(tokens, clss, expected, line_no):
nid = Parser.get_nid(tokens, expected, line_no)
if Line.is_defined(nid):
line = Line.get(nid)
if isinstance(line, clss):
return line
else:
raise syntax_error(expected, line_no)
else:
raise syntax_error(f"defined {expected}", line_no)
def get_bool_or_bitvec_sid_line(tokens, line_no):
return Parser.get_nid_line(tokens, Bitvector, "Boolean or bitvector sort nid", line_no)
def get_bitvec_sid_line(tokens, line_no):
return Parser.get_nid_line(tokens, Bitvec, "bitvector sort nid", line_no)
def get_sid_line(tokens, line_no):
return Parser.get_nid_line(tokens, Sort, "sort nid", line_no)
def get_state_line(tokens, line_no):
return Parser.get_nid_line(tokens, State, "state nid", line_no)
def get_exp_line(tokens, line_no):
return Parser.get_nid_line(tokens, Expression, "expression nid", line_no)
def get_number(tokens, base, expected, line_no):
token = Parser.get_token(tokens, expected, line_no)
try:
if (base == 10):
return int(token)
else:
return int(token, base)
except ValueError:
raise syntax_error(expected, line_no)
def get_symbol(tokens):
try:
return Parser.get_token(tokens, None, None)
except:
return ""
def get_comment(tokens, line_no):
comment = Parser.get_symbol(tokens)
if comment:
if comment[0] != ';':
raise syntax_error("comment", line_no)
return comment
def get_class(self, clss_or_keyword):
if clss_or_keyword is Bool:
return Bool
elif clss_or_keyword is Bitvec:
return Bitvec
elif clss_or_keyword is Array:
return Array
elif clss_or_keyword is Constant_Array:
return Constant_Array
elif clss_or_keyword is Zero or clss_or_keyword == Zero.keyword:
return Zero
elif clss_or_keyword is One or clss_or_keyword == One.keyword:
return One
elif clss_or_keyword is Constd or clss_or_keyword == Constd.keyword:
return Constd
elif clss_or_keyword is Const or clss_or_keyword == Const.keyword:
return Const
elif clss_or_keyword is Consth or clss_or_keyword == Consth.keyword:
return Consth
elif clss_or_keyword is Input or clss_or_keyword == Input.keyword:
return Input
elif clss_or_keyword is State or clss_or_keyword == State.keyword:
return State
elif clss_or_keyword is Ext or clss_or_keyword in Ext.keywords:
return Ext
elif clss_or_keyword is Slice or clss_or_keyword == Slice.keyword:
return Slice
elif clss_or_keyword is Unary or clss_or_keyword in Unary.keywords:
return Unary
elif clss_or_keyword is Implies or clss_or_keyword == Implies.keyword:
return Implies
elif clss_or_keyword is Comparison or clss_or_keyword in Comparison.keywords:
return Comparison
elif clss_or_keyword is Logical or clss_or_keyword in Logical.keywords:
return Logical
elif clss_or_keyword is Computation or clss_or_keyword in Computation.keywords:
return Computation
elif clss_or_keyword is Concat or clss_or_keyword == Concat.keyword:
return Concat
elif clss_or_keyword is Read or clss_or_keyword == Read.keyword:
return Read
elif clss_or_keyword is Ite or clss_or_keyword == Ite.keyword:
return Ite
elif clss_or_keyword is Write or clss_or_keyword == Write.keyword:
return Write
elif clss_or_keyword is Init or clss_or_keyword == Init.keyword:
return Init
elif clss_or_keyword is Next or clss_or_keyword == Next.keyword:
return Next
elif clss_or_keyword is Constraint or clss_or_keyword == Constraint.keyword:
return Constraint
elif clss_or_keyword is Bad or clss_or_keyword == Bad.keyword:
return Bad
def new_boolean(self, nid = None, line_no = None):
return self.get_class(Bool)(Parser.next_nid(nid), "Boolean", line_no)
def new_bitvec(self, size_in_bits, comment, nid = None, line_no = None):
return self.get_class(Bitvec)(Parser.next_nid(nid), size_in_bits, comment, line_no)
def new_array(self, address_sid, element_sid, comment, nid = None, line_no = None):
return self.get_class(Array)(Parser.next_nid(nid), address_sid, element_sid, comment, line_no)
def new_zero_one(self, op, sid, symbol, comment, nid = None, line_no = None):
assert op in {OP_ZERO, OP_ONE}
return self.get_class(op)(Parser.next_nid(nid), sid, symbol, comment, line_no)
def new_constant(self, op, sid, constant, comment, nid = None, line_no = None):
assert op in {OP_CONSTD, OP_CONST, OP_CONSTH}
if op == OP_CONSTD:
if constant == 0:
return self.get_class(Zero)(Parser.next_nid(nid), sid, "", comment, line_no)
elif constant == 1:
return self.get_class(One)(Parser.next_nid(nid), sid, "", comment, line_no)
return self.get_class(op)(Parser.next_nid(nid), sid, constant, comment, line_no)
def new_input(self, op, sid, symbol, comment, nid = None, line_no = None):
assert op in Variable.keywords
return self.get_class(op)(Parser.next_nid(nid), sid, symbol, comment, line_no)
def new_ext(self, op, sid, value_nid, w, comment, nid = None, line_no = None):
assert op in Ext.keywords
return self.get_class(op)(Parser.next_nid(nid), op, sid, value_nid, w, comment, line_no)
def new_slice(self, sid, value_nid, u, l, comment, nid = None, line_no = None):
return self.get_class(Slice.keyword)(Parser.next_nid(nid), sid, value_nid, u, l, comment, line_no)
def new_unary(self, op, sid, value_nid, comment, nid = None, line_no = None):
assert op in Unary.keywords
return self.get_class(op)(Parser.next_nid(nid), op, sid, value_nid, comment, line_no)
def new_unary_boolean(self, op, value_nid, comment, nid = None, line_no = None):
assert op == OP_NOT
return self.get_class(op)(Parser.next_nid(nid), op, SID_BOOLEAN, value_nid, comment, line_no)
def new_binary(self, op, sid, left_nid, right_nid, comment, nid = None, line_no = None):
assert op in Binary.keywords
return self.get_class(op)(Parser.next_nid(nid), op, sid, left_nid, right_nid, comment, line_no)
def new_binary_boolean(self, op, left_nid, right_nid, comment, nid = None, line_no = None):
assert op in Implies.keyword + Comparison.keywords + Logical.keywords
return self.get_class(op)(Parser.next_nid(nid), op, SID_BOOLEAN, left_nid, right_nid, comment, line_no)
def new_ternary(self, op, sid, first_nid, second_nid, third_nid, comment, nid = None, line_no = None):
assert op in Ternary.keywords
return self.get_class(op)(Parser.next_nid(nid), sid, first_nid, second_nid, third_nid, comment, line_no)
def new_init(self, sid, state_nid, value_nid, comment, nid = None, line_no = None):
return self.get_class(Init.keyword)(Parser.next_nid(nid), sid, state_nid, value_nid, comment, line_no)
def new_next(self, sid, state_nid, value_nid, comment, nid = None, line_no = None):
return self.get_class(Next.keyword)(Parser.next_nid(nid), sid, state_nid, value_nid, comment, line_no)
def new_init_next(self, op, sid, state_nid, value_nid, symbol, comment, nid = None, line_no = None):
return self.get_class(op)(Parser.next_nid(nid), sid, state_nid, value_nid, symbol, comment, line_no)
def new_property(self, op, condition_nid, symbol, comment, nid = None, line_no = None):
assert op in Property.keywords
return self.get_class(op)(Parser.next_nid(nid), condition_nid, symbol, comment, line_no)
def parse_sort_line(self, tokens, nid, line_no):
token = Parser.get_token(tokens, "bitvector or array", line_no)
if token == Bitvec.keyword:
size = Parser.get_decimal(tokens, "bitvector size", line_no)
comment = Parser.get_comment(tokens, line_no)
# beator- and rotor-dependent Boolean declaration
if comment == "; Boolean" and size == 1:
return self.new_boolean(nid, line_no)
else:
return self.new_bitvec(size, comment, nid, line_no)
elif token == Array.keyword:
array_size_line = Parser.get_bitvec_sid_line(tokens, line_no)
element_size_line = Parser.get_bitvec_sid_line(tokens, line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_array(array_size_line, element_size_line, comment, nid, line_no)
else:
raise syntax_error("bitvector or array", line_no)
def parse_symbol_comment(self, tokens, line_no):
symbol = Parser.get_symbol(tokens)
comment = Parser.get_comment(tokens, line_no)
if symbol:
if symbol[0] == ';':
return "", symbol
return symbol, comment
def parse_zero_one_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_bool_or_bitvec_sid_line(tokens, line_no)
symbol, comment = self.parse_symbol_comment(tokens, line_no)
return self.new_zero_one(op, sid_line, symbol, comment, nid, line_no)
def parse_constant_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_bool_or_bitvec_sid_line(tokens, line_no)
if op == Constd.keyword:
value = Parser.get_number(tokens, 10, "signed integer", line_no)
elif op == Const.keyword:
value = Parser.get_number(tokens, 2, "binary number", line_no)
elif op == Consth.keyword:
value = Parser.get_number(tokens, 16, "hexadecimal number", line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_constant(op, sid_line, value, comment, nid, line_no)
def parse_variable_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
symbol, comment = self.parse_symbol_comment(tokens, line_no)
return self.new_input(op, sid_line, symbol, comment, nid, line_no)
def parse_ext_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
arg1_line = Parser.get_exp_line(tokens, line_no)
w = Parser.get_decimal(tokens, "bit width", line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_ext(op, sid_line, arg1_line, w, comment, nid, line_no)
def parse_slice_line(self, tokens, nid, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
arg1_line = Parser.get_exp_line(tokens, line_no)
u = Parser.get_decimal(tokens, "upper bit", line_no)
l = Parser.get_decimal(tokens, "lower bit", line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_slice(sid_line, arg1_line, u, l, comment, nid, line_no)
def parse_unary_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
arg1_line = Parser.get_exp_line(tokens, line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_unary(op, sid_line, arg1_line, comment, nid, line_no)
def parse_binary_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
arg1_line = Parser.get_exp_line(tokens, line_no)
arg2_line = Parser.get_exp_line(tokens, line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_binary(op, sid_line, arg1_line, arg2_line, comment, nid, line_no)
def parse_ternary_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
arg1_line = Parser.get_exp_line(tokens, line_no)
arg2_line = Parser.get_exp_line(tokens, line_no)
arg3_line = Parser.get_exp_line(tokens, line_no)
comment = Parser.get_comment(tokens, line_no)
return self.new_ternary(op, sid_line, arg1_line, arg2_line, arg3_line, comment, nid, line_no)
def parse_init_next_line(self, tokens, nid, op, line_no):
sid_line = Parser.get_sid_line(tokens, line_no)
state_line = Parser.get_state_line(tokens, line_no)
exp_line = Parser.get_exp_line(tokens, line_no)
symbol, comment = self.parse_symbol_comment(tokens, line_no)
return self.new_init_next(op, sid_line, state_line, exp_line, symbol, comment, nid, line_no)
def parse_property_line(self, tokens, nid, op, line_no):
property_line = Parser.get_exp_line(tokens, line_no)
symbol, comment = self.parse_symbol_comment(tokens, line_no)
return self.new_property(op, property_line, symbol, comment, nid, line_no)
def parse_btor2_line(self, line, line_no):
if line.strip():
tokens = Parser.tokenize_btor2(line)
token = Parser.get_token(tokens, None, None)
if token[0] != ';':
if token.isdecimal():
nid = Array.accommodate_array_indexes(int(token))
if nid > Parser.current_nid:
Parser.current_nid = nid
token = Parser.get_token(tokens, "keyword", line_no)
if token == Sort.keyword:
return self.parse_sort_line(tokens, nid, line_no)
elif token in {Zero.keyword, One.keyword}:
return self.parse_zero_one_line(tokens, nid, token, line_no)
elif token in {Constd.keyword, Const.keyword, Consth.keyword}:
return self.parse_constant_line(tokens, nid, token, line_no)
elif token in Variable.keywords:
return self.parse_variable_line(tokens, nid, token, line_no)
elif token in Ext.keywords:
return self.parse_ext_line(tokens, nid, token, line_no)
elif token == Slice.keyword:
return self.parse_slice_line(tokens, nid, line_no)
elif token in Unary.keywords:
return self.parse_unary_line(tokens, nid, token, line_no)
elif token in Binary.keywords:
return self.parse_binary_line(tokens, nid, token, line_no)
elif token in Ternary.keywords:
return self.parse_ternary_line(tokens, nid, token, line_no)
elif token in {Init.keyword, Next.keyword}:
return self.parse_init_next_line(tokens, nid, token, line_no)
elif token in Property.keywords:
return self.parse_property_line(tokens, nid, token, line_no)
else:
raise syntax_error(f"unknown operator {token}", line_no)
raise syntax_error("increasing nid", line_no)
raise syntax_error("nid", line_no)
return line.strip()
def parse_btor2(self, modelfile, outputfile):
Parser.parser = self
print(f"model file: {modelfile.name}")
lines = {}
line_no = 1
for line in modelfile:
try:
lines[line_no] = self.parse_btor2_line(line, line_no)
line_no += 1
except (model_error, syntax_error) as message:
print(f"parsing exception: {message}")
exit(1)
# start: mapping arrays to bitvectors
if Array.ARRAY_SIZE_BOUND > 0:
for init in Init.inits.values():
init.set_mapped_array_expression()
for constraint in Constraint.constraints.values():
constraint.set_mapped_array_expression()
for bad in Bad.bads.values():
bad.set_mapped_array_expression()
for next_line in Next.nexts.values():
next_line.set_mapped_array_expression()
for state in list(State.states.values()):
if isinstance(state.sid_line, Bitvector):
if state.init_line is not None and state.next_line is not None:
if state.init_line.exp_line is state.next_line.exp_line or state.next_line.exp_line is state:
# remove initialized read-only bitvector states
state.remove_state()
Transitional.remove_transition(state, Init.inits)
Transitional.remove_transition(state, Next.nexts)
if Ite.branching_conditions and Ite.non_branching_conditions:
Ite.branching_conditions = Ite.branching_conditions.get_mapped_array_expression_for(None)
Ite.non_branching_conditions = Ite.non_branching_conditions.get_mapped_array_expression_for(None)
# end: mapping arrays to bitvectors
for state in State.states.values():
if state.init_line is None:
# state has no init
state.new_input(state.index)
are_there_uninitialized_states = False
are_there_untransitioned_states = False
are_there_state_transitions = False
for state in State.states.values():
if state.init_line is None:
are_there_uninitialized_states = True
if state.next_line is None:
are_there_untransitioned_states = True
else:
are_there_state_transitions = True
if are_there_state_transitions:
print("sequential problem:")
else:
print("combinational problem:")
for input_line in Input.inputs.values():
if isinstance(input_line, Input):
print(input_line)
for state in State.states.values():
print(state)
if are_there_uninitialized_states:
print("uninitialized states:")
for state in State.states.values():
if state.init_line is None:
print(state)
if are_there_untransitioned_states:
print("untransitioned states:")
for state in State.states.values():
if state.next_line is None:
print(state)
if Ite.branching_conditions and Ite.non_branching_conditions:
print("branching conditions:")
print(Ite.branching_conditions)
print(Ite.non_branching_conditions)
print("model profile:")
print(f"{len(Line.lines)} lines in total")
print(f"{self.get_class(Input).count} input, ", end="")
print(f"{self.get_class(State).count} state, ", end="")
print(f"{self.get_class(Init).count} init, ", end="")
print(f"{self.get_class(Next).count} next, ", end="")
print(f"{self.get_class(Constraint).count} constraint, ", end="")
print(f"{self.get_class(Bad).count} bad")
print(f"{self.get_class(Bool).count} bool, ", end="")
print(f"{self.get_class(Bitvec).count} bitvec, ", end="")
print(f"{self.get_class(Array).count} array")
print(f"{self.get_class(Zero).count} zero, ", end="")
print(f"{self.get_class(One).count} one, ", end="")
print(f"{self.get_class(Constd).count} constd, ", end="")
print(f"{self.get_class(Const).count} const, ", end="")
print(f"{self.get_class(Consth).count} consth")
print(f"{self.get_class(Ext).count} ext, ", end="")
print(f"{self.get_class(Slice).count} slice, ", end="")
print(f"{self.get_class(Unary).count} unary")
print(f"{self.get_class(Implies).count} implies, ", end="")
print(f"{self.get_class(Comparison).count} comparison, ", end="")
print(f"{self.get_class(Logical).count} logical, ", end="")
print(f"{self.get_class(Computation).count} computation")
print(f"{self.get_class(Concat).count} concat, ", end="")
print(f"{self.get_class(Ite).count} ite, ", end="")
print(f"{self.get_class(Read).count} read, ", end="")
print(f"{self.get_class(Write).count} write")
if Array.ARRAY_SIZE_BOUND > 0:
print("array mapping profile:")
print(f"out of {Array.number_of_variable_arrays} arrays {Array.number_of_mapped_arrays} mapped")
print(f"{Expression.total_number_of_generated_expressions} generated expressions")
Expression.total_number_of_generated_expressions = 0
if outputfile:
print(f"output file: {outputfile.name}")
for line in lines.values():
print(line, file=outputfile)
return are_there_state_transitions