diff --git a/tools/bitme.py b/tools/bitme.py index 5e1e90e0..8e2c2139 100755 --- a/tools/bitme.py +++ b/tools/bitme.py @@ -1,7 +1,35 @@ #!/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 + +# 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 ctypes + +try: + rotor = ctypes.cdll.LoadLibrary("rotor") + is_rotor_present = True +except OSError: + print("rotor is not available") + is_rotor_present = False + # requires Z3 and the Z3 Python API: # pip install z3-solver @@ -23,8 +51,81 @@ print("bitwuzla is not available") is_bitwuzla_present = False +# BTOR2, Z3, and bitwuzla models + import math +# supported BTOR2 keywords and operators + +UNUSED = None + +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' + +# map arrays up to size bound to bitvectors + +ARRAY_SIZE_BOUND = 5 # array size in bits + class model_error(Exception): def __init__(self, expected, line_no): super().__init__(f"model error in line {line_no}: {expected} expected") @@ -36,32 +137,35 @@ def __init__(self): class Bitwuzla(): def __init__(self): self.bitwuzla = None - self.step = 0 class Line(Z3, Bitwuzla): lines = dict() - def __init__(self, nid, comment, line_no): + def __init__(self, nid, comment, line_no, index = None): Z3.__init__(self) Bitwuzla.__init__(self) self.nid = nid - self.comment = comment + self.comment = "; " + comment if comment != "" and comment[0] != ';' else comment self.line_no = line_no - self.new_line() + self.new_line(index) + + def __repr__(self): + return self.__str__() - def new_line(self): - assert self not in Line.lines - Line.lines[self.nid] = self + def new_line(self, index = None): + if index is None: + assert self.nid not in Line.lines, f"nid {self.nid} already defined @ {self.line_no}" + Line.lines[self.nid] = self def is_defined(nid): return nid in Line.lines def get(nid): - assert nid in Line.lines + assert Line.is_defined(nid), f"undefined nid {self.nid} @ {self.line_no}" return Line.lines[nid] class Sort(Line): - keyword = 'sort' + keyword = OP_SORT def __init__(self, nid, comment, line_no): super().__init__(nid, comment, line_no) @@ -70,7 +174,7 @@ def match_sorts(self, sort): return type(self) == type(sort) class Bitvector(Sort): - keyword = 'bitvec' + keyword = BITVEC def __init__(self, nid, size, comment, line_no): super().__init__(nid, comment, line_no) @@ -94,9 +198,8 @@ def get_z3(self): self.z3 = z3.BoolSort() return self.z3 - def get_bitwuzla(self, step, tm): + def get_bitwuzla(self, tm): if self.bitwuzla is None: - assert step == 0 self.bitwuzla = tm.mk_bool_sort() return self.bitwuzla @@ -112,14 +215,13 @@ def get_z3(self): self.z3 = z3.BitVecSort(self.size) return self.z3 - def get_bitwuzla(self, step, tm): + def get_bitwuzla(self, tm): if self.bitwuzla is None: - assert step == 0 self.bitwuzla = tm.mk_bv_sort(self.size) return self.bitwuzla class Array(Sort): - keyword = 'array' + keyword = ARRAY def __init__(self, nid, array_size_line, element_size_line, comment, line_no): super().__init__(nid, comment, line_no) @@ -145,28 +247,29 @@ def match_init_sorts(self, sort): def get_z3(self): if self.z3 is None: - self.z3 = z3.ArraySort(self.array_size_line.get_z3(), self.element_size_line.get_z3()) + self.z3 = z3.ArraySort(self.array_size_line.get_z3(), + self.element_size_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): + def get_bitwuzla(self, tm): if self.bitwuzla is None: - assert step == 0 - self.bitwuzla = tm.mk_array_sort(self.array_size_line.get_bitwuzla(step, tm), - self.element_size_line.get_bitwuzla(step, tm)) + self.bitwuzla = tm.mk_array_sort(self.array_size_line.get_bitwuzla(tm), + self.element_size_line.get_bitwuzla(tm)) return self.bitwuzla class Expression(Line): - def __init__(self, nid, sid_line, comment, line_no): - super().__init__(nid, comment, line_no) + def __init__(self, nid, sid_line, domain, comment, line_no, index = None): + super().__init__(nid, comment, line_no, index) self.sid_line = sid_line + self.domain = domain if not isinstance(sid_line, Sort): raise model_error("sort", line_no) class Constant(Expression): def __init__(self, nid, sid_line, value, comment, line_no): - super().__init__(nid, sid_line, comment, line_no) + super().__init__(nid, sid_line, dict(), comment, line_no) self.value = value - if value >= 2**sid_line.size: + if not(0 <= value < 2**sid_line.size or -2**(sid_line.size - 1) <= value < 2**(sid_line.size - 1)): raise model_error(f"{value} in range of {sid_line.size}-bit bitvector", line_no) def get_z3(self): @@ -177,17 +280,16 @@ def get_z3(self): self.z3 = z3.BitVecVal(self.value, self.sid_line.size) return self.z3 - def get_bitwuzla(self, step, tm): + def get_bitwuzla(self, tm): if self.bitwuzla is None: - assert step == 0 if isinstance(self.sid_line, Bool): self.bitwuzla = tm.mk_true() if bool(self.value) else tm.mk_false() else: - self.bitwuzla = tm.mk_bv_value(self.sid_line.get_bitwuzla(step, tm), self.value) + self.bitwuzla = tm.mk_bv_value(self.sid_line.get_bitwuzla(tm), self.value) return self.bitwuzla class Zero(Constant): - keyword = 'zero' + keyword = OP_ZERO def __init__(self, nid, sid_line, comment, line_no): super().__init__(nid, sid_line, 0, comment, line_no) @@ -196,7 +298,7 @@ def __str__(self): return f"{self.nid} {Zero.keyword} {self.sid_line.nid} {self.comment}" class One(Constant): - keyword = 'one' + keyword = OP_ONE def __init__(self, nid, sid_line, comment, line_no): super().__init__(nid, sid_line, 1, comment, line_no) @@ -205,7 +307,7 @@ def __str__(self): return f"{self.nid} {One.keyword} {self.sid_line.nid} {self.comment}" class Constd(Constant): - keyword = 'constd' + keyword = OP_CONSTD def __init__(self, nid, sid_line, value, comment, line_no): super().__init__(nid, sid_line, value, comment, line_no) @@ -214,7 +316,7 @@ def __str__(self): return f"{self.nid} {Constd.keyword} {self.sid_line.nid} {self.value} {self.comment}" class Const(Constant): - keyword = 'const' + keyword = OP_CONST def __init__(self, nid, sid_line, value, comment, line_no): super().__init__(nid, sid_line, value, comment, line_no) @@ -224,7 +326,7 @@ def __str__(self): return f"{self.nid} {Const.keyword} {self.sid_line.nid} {self.value:0{size}b} {self.comment}" class Consth(Constant): - keyword = 'consth' + keyword = OP_CONSTH def __init__(self, nid, sid_line, value, comment, line_no): super().__init__(nid, sid_line, value, comment, line_no) @@ -234,93 +336,142 @@ def __str__(self): return f"{self.nid} {Consth.keyword} {self.sid_line.nid} {self.value:0{size}X} {self.comment}" class Variable(Expression): - keywords = {'input', 'state'} + keywords = {OP_INPUT, OP_STATE} inputs = dict() - def __init__(self, nid, sid_line, symbol, comment, line_no): - super().__init__(nid, sid_line, comment, line_no) + def __init__(self, nid, sid_line, domain, symbol, comment, line_no, index = None): + super().__init__(nid, sid_line, domain, comment, line_no, index) + self.qid = f"{nid}{f"-{index}" if index is not None else ''}" self.symbol = symbol + if index is not None and not isinstance(sid_line, Bitvector): + raise model_error("bitvector", line_no) + if index is None: + self.array = self.new_array() + else: + self.index = index + + def new_array(self): + if isinstance(self.sid_line, Array) and self.sid_line.array_size_line.size <= ARRAY_SIZE_BOUND: + array = dict() + for index in range(2**self.sid_line.array_size_line.size): + array[index] = self.__class__(self.nid, + self.sid_line.element_size_line, self.symbol, self.comment, self.line_no, index) + return array + else: + return None - def new_input(self): - assert self not in Variable.inputs - Variable.inputs[self.nid] = self + def new_input(self, index = None): + if index is None: + assert self.nid not in Variable.inputs, f"variable nid {self.nid} already defined @ {self.line_no}" + Variable.inputs[self.nid] = self + + def get_z3(self): + if self.z3 is None: + self.z3 = z3.Const(self.name, self.sid_line.get_z3()) + return self.z3 class Input(Variable): - keyword = 'input' + keyword = OP_INPUT - def __init__(self, nid, sid_line, symbol, comment, line_no): - super().__init__(nid, sid_line, symbol, comment, line_no) - self.new_input() + def __init__(self, nid, sid_line, symbol, comment, line_no, index = None): + super().__init__(nid, sid_line, dict(), symbol, comment, line_no, index) + self.name = f"input{self.qid}" + self.new_input(index) def __str__(self): - return f"{self.nid} {Input.keyword} {self.sid_line.nid} {self.symbol} {self.comment}" + return f"{self.qid} {Input.keyword} {self.sid_line.nid} {self.symbol} {self.comment}" - def get_name(self): - return f"input{self.nid}" - - def get_z3(self): - if self.z3 is None: - self.z3 = z3.Const(self.get_name(), self.sid_line.get_z3()) - return self.z3 + def get_z3_step(self, step): + return self.get_z3() - def get_bitwuzla(self, step, tm): + def get_bitwuzla(self, tm): if self.bitwuzla is None: - assert step == 0 - self.bitwuzla = tm.mk_const(self.sid_line.get_bitwuzla(step, tm), self.get_name()) + self.bitwuzla = tm.mk_const(self.sid_line.get_bitwuzla(tm), self.name) return self.bitwuzla -class State(Variable): - keyword = 'state' + def get_bitwuzla_step(self, step, tm): + return self.get_bitwuzla(tm) + +class Cache(): + def __init__(self): + self.cache_z3 = dict() + self.cache_bitwuzla = dict() + +class State(Variable, Cache): + keyword = OP_STATE states = dict() pc = None - def __init__(self, nid, sid_line, symbol, comment, line_no): - super().__init__(nid, sid_line, symbol, comment, line_no) - self.init_line = self - self.next_line = self - self.new_state() + def __init__(self, nid, sid_line, symbol, comment, line_no, index = None): + Variable.__init__(self, nid, sid_line, {nid:self}, symbol, comment, line_no, index) + Cache.__init__(self) + self.name = f"state{self.qid}" + 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}" + return f"{self.qid} {State.keyword} {self.sid_line.nid} {self.symbol} {self.comment}" - def new_state(self): - assert self not in State.states - State.states[self.nid] = self + def new_state(self, index = None): + if index is None: + assert self.nid not in State.states, f"state nid {self.nid} already defined @ {self.line_no}" + State.states[self.nid] = self - def get_name(self, step): - return f"state{self.nid}-{step}" + def get_step_name(self, step): + return f"{self.name}-{step}" def get_z3_step(self, step): - return z3.Const(self.get_name(step), self.sid_line.get_z3()) + if step not in self.cache_z3: + self.cache_z3[step] = z3.Const(self.get_step_name(step), self.sid_line.get_z3()) + return self.cache_z3[step] - def get_z3(self): - if self.z3 is None: - self.z3 = self.get_z3_step(0) - return self.z3 + def get_z3_lambda(term, domain): + if domain: + return z3.Lambda([state.get_z3() for state in domain.values()], term) + else: + return term - def get_bitwuzla_step(self, step, tm): - return tm.mk_const(self.sid_line.get_bitwuzla(step, tm), self.get_name(step)) + def get_z3_select(term, domain, step): + if domain: + return z3.Select(term, *[state.get_z3_step(step) for state in domain.values()]) + else: + return term - def get_bitwuzla(self, step, tm): - assert step == self.step + def get_bitwuzla(self, tm): if self.bitwuzla is None: - self.bitwuzla = self.get_bitwuzla_step(step, tm) + self.bitwuzla = tm.mk_var(self.sid_line.get_bitwuzla(tm), self.name) return self.bitwuzla - def set_bitwuzla(self, step, tm): - assert step == self.step + 1 and self.next_line is not None and step == self.next_line.step + 1 - self.bitwuzla = self.next_line.next_step - self.step = step + def get_bitwuzla_step(self, step, tm): + if step not in self.cache_bitwuzla: + self.cache_bitwuzla[step] = tm.mk_const(self.sid_line.get_bitwuzla(tm), + self.get_step_name(step)) + return self.cache_bitwuzla[step] + + def get_bitwuzla_lambda(term, domain, tm): + if domain: + return tm.mk_term(bitwuzla.Kind.LAMBDA, + [*[state.get_bitwuzla(tm) for state in domain.values()], term]) + else: + return term + + def get_bitwuzla_select(term, domain, step, tm): + if domain: + return tm.mk_term(bitwuzla.Kind.APPLY, + [term, *[state.get_bitwuzla_step(step, tm) for state in domain.values()]]) + else: + return term class Indexed(Expression): def __init__(self, nid, sid_line, arg1_line, comment, line_no): - super().__init__(nid, sid_line, comment, line_no) + super().__init__(nid, sid_line, arg1_line.domain, comment, line_no) self.arg1_line = arg1_line if not isinstance(arg1_line, Expression): raise model_error("expression operand", line_no) @@ -330,7 +481,7 @@ def __init__(self, nid, sid_line, arg1_line, comment, line_no): raise model_error("bitvector operand", line_no) class Ext(Indexed): - keywords = {'sext', 'uext'} + 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) @@ -350,20 +501,18 @@ def get_z3(self): self.z3 = z3.ZeroExt(self.w, self.arg1_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: if self.op == 'sext': bitwuzla_op = bitwuzla.Kind.BV_SIGN_EXTEND elif self.op == 'uext': bitwuzla_op = bitwuzla.Kind.BV_ZERO_EXTEND self.bitwuzla = tm.mk_term(bitwuzla_op, - [self.arg1_line.get_bitwuzla(step, tm)], [self.w]) - self.step = step + [self.arg1_line.get_bitwuzla(tm)], [self.w]) return self.bitwuzla class Slice(Indexed): - keyword = 'slice' + 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) @@ -384,19 +533,17 @@ def get_z3(self): self.z3 = z3.Extract(self.u, self.l, self.arg1_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.BV_EXTRACT, - [self.arg1_line.get_bitwuzla(step, tm)], [self.u, self.l]) - self.step = step + [self.arg1_line.get_bitwuzla(tm)], [self.u, self.l]) return self.bitwuzla class Unary(Expression): - keywords = {'not', 'inc', 'dec', 'neg'} + 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, comment, line_no) + super().__init__(nid, sid_line, arg1_line.domain, comment, line_no) self.op = op self.arg1_line = arg1_line if not isinstance(arg1_line, Expression): @@ -426,9 +573,8 @@ def get_z3(self): self.z3 = -self.arg1_line.get_z3() return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: if self.op == 'not': if isinstance(self.sid_line, Bool): bitwuzla_op = bitwuzla.Kind.NOT @@ -440,15 +586,14 @@ def get_bitwuzla(self, step, tm): bitwuzla_op = bitwuzla.Kind.BV_DEC elif self.op == 'neg': bitwuzla_op = bitwuzla.Kind.BV_NEG - self.bitwuzla = tm.mk_term(bitwuzla_op, [self.arg1_line.get_bitwuzla(step, tm)]) - self.step = step + self.bitwuzla = tm.mk_term(bitwuzla_op, [self.arg1_line.get_bitwuzla(tm)]) return self.bitwuzla class Binary(Expression): - keywords = {'implies', 'eq', 'neq', 'sgt', 'ugt', 'sgte', 'ugte', 'slt', 'ult', 'slte', 'ulte', 'and', 'or', 'xor', 'sll', 'srl', 'sra', 'add', 'sub', 'mul', 'sdiv', 'udiv', 'srem', 'urem', 'concat', 'read'} + 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, comment, line_no) + super().__init__(nid, sid_line, arg1_line.domain | arg2_line.domain, comment, line_no) self.op = op self.arg1_line = arg1_line self.arg2_line = arg2_line @@ -461,10 +606,10 @@ def __str__(self): return f"{self.nid} {self.op} {self.sid_line.nid} {self.arg1_line.nid} {self.arg2_line.nid} {self.comment}" class Implies(Binary): - keyword = 'implies' + keyword = OP_IMPLIES def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): - super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) + 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): @@ -477,16 +622,14 @@ def get_z3(self): self.z3 = z3.Implies(self.arg1_line.get_z3(), self.arg2_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.IMPLIES, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Comparison(Binary): - keywords = {'eq', 'neq', 'sgt', 'ugt', 'sgte', 'ugte', 'slt', 'ult', 'slte', 'ulte'} + 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): super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) @@ -521,9 +664,8 @@ def get_z3(self): self.z3 = z3.ULE(self.arg1_line.get_z3(), self.arg2_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: if self.op == 'eq': bitwuzla_op = bitwuzla.Kind.EQUAL elif self.op == 'neq': @@ -545,12 +687,11 @@ def get_bitwuzla(self, step, tm): elif self.op == 'ulte': bitwuzla_op = bitwuzla.Kind.BV_ULE self.bitwuzla = tm.mk_term(bitwuzla_op, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Logical(Binary): - keywords = {'and', 'or', 'xor'} + keywords = {OP_AND, OP_OR, OP_XOR} def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) @@ -579,9 +720,8 @@ def get_z3(self): self.z3 = self.arg1_line.get_z3() ^ self.arg2_line.get_z3() return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: if isinstance(self.sid_line, Bool): if self.op == 'and': bitwuzla_op = bitwuzla.Kind.AND @@ -597,12 +737,11 @@ def get_bitwuzla(self, step, tm): elif self.op == 'xor': bitwuzla_op = bitwuzla.Kind.BV_XOR self.bitwuzla = tm.mk_term(bitwuzla_op, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Computation(Binary): - keywords = {'sll', 'srl', 'sra', 'add', 'sub', 'mul', 'sdiv', 'udiv', 'srem', 'urem'} + 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): super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) @@ -637,9 +776,8 @@ def get_z3(self): self.z3 = z3.URem(self.arg1_line.get_z3(), self.arg2_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: if self.op == 'sll': bitwuzla_op = bitwuzla.Kind.BV_SHL elif self.op == 'srl': @@ -661,15 +799,14 @@ def get_bitwuzla(self, step, tm): elif self.op == 'urem': bitwuzla_op = bitwuzla.Kind.BV_UREM self.bitwuzla = tm.mk_term(bitwuzla_op, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Concat(Binary): - keyword = 'concat' + keyword = OP_CONCAT def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): - super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) + 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): @@ -684,19 +821,17 @@ def get_z3(self): self.z3 = z3.Concat(self.arg1_line.get_z3(), self.arg2_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.BV_CONCAT, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Read(Binary): - keyword = 'read' + keyword = OP_READ def __init__(self, nid, op, sid_line, arg1_line, arg2_line, comment, line_no): - super().__init__(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) + 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): @@ -709,19 +844,17 @@ def get_z3(self): self.z3 = z3.Select(self.arg1_line.get_z3(), self.arg2_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.ARRAY_SELECT, - [self.arg1_line.get_bitwuzla(step, tm), self.arg2_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), self.arg2_line.get_bitwuzla(tm)]) return self.bitwuzla class Ternary(Expression): - keywords = {'ite', 'write'} + 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, comment, line_no) + super().__init__(nid, sid_line, arg1_line.domain | arg2_line.domain | arg3_line.domain, comment, line_no) self.op = op self.arg1_line = arg1_line self.arg2_line = arg2_line @@ -737,16 +870,27 @@ 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}" class Ite(Ternary): - keyword = 'ite' + keyword = OP_ITE + + branching_conditions = None + non_branching_conditions = None def __init__(self, nid, op, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no): - super().__init__(nid, op, 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) + if comment == "; branch true condition": + Ite.branching_conditions = self + self.z3_lambda_line = None + self.bitwuzla_lambda_line = None + elif comment == "; branch false condition": + Ite.non_branching_conditions = self + self.z3_lambda_line = None + self.bitwuzla_lambda_line = None def get_z3(self): if self.z3 is None: @@ -754,21 +898,29 @@ def get_z3(self): self.arg2_line.get_z3(), self.arg3_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_z3_step(self, step): + if self.z3_lambda_line is None: + self.z3_lambda_line = State.get_z3_lambda(self.get_z3(), self.domain) + return State.get_z3_select(self.z3_lambda_line, self.domain, step) + + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.ITE, - [self.arg1_line.get_bitwuzla(step, tm), - self.arg2_line.get_bitwuzla(step, tm), - self.arg3_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), + self.arg2_line.get_bitwuzla(tm), + self.arg3_line.get_bitwuzla(tm)]) return self.bitwuzla + def get_bitwuzla_step(self, step, tm): + if self.bitwuzla_lambda_line is None: + self.bitwuzla_lambda_line = State.get_bitwuzla_lambda(self.get_bitwuzla(tm), self.domain, tm) + return State.get_bitwuzla_select(self.bitwuzla_lambda_line, self.domain, step, tm) + class Write(Ternary): - keyword = 'write' + keyword = OP_WRITE def __init__(self, nid, op, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no): - super().__init__(nid, op, 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): @@ -784,128 +936,162 @@ def get_z3(self): self.arg2_line.get_z3(), self.arg3_line.get_z3()) return self.z3 - def get_bitwuzla(self, step, tm): - assert step == 0 or self.step <= step <= self.step + 1 - if self.bitwuzla is None or step > self.step: + def get_bitwuzla(self, tm): + if self.bitwuzla is None: self.bitwuzla = tm.mk_term(bitwuzla.Kind.ARRAY_STORE, - [self.arg1_line.get_bitwuzla(step, tm), - self.arg2_line.get_bitwuzla(step, tm), - self.arg3_line.get_bitwuzla(step, tm)]) - self.step = step + [self.arg1_line.get_bitwuzla(tm), + self.arg2_line.get_bitwuzla(tm), + self.arg3_line.get_bitwuzla(tm)]) return self.bitwuzla -class Init(Line): - keyword = 'init' +class Sequential(Line, Cache): + def __init__(self, nid, comment, line_no, index = None): + Line.__init__(self, nid, comment, line_no, index) + Cache.__init__(self) + self.z3_lambda_line = None + self.bitwuzla_lambda_line = None - inits = dict() - - def __init__(self, nid, sid_line, state_line, exp_line, comment, line_no): - super().__init__(nid, comment, line_no) +class Transaction(Sequential): + def __init__(self, nid, sid_line, state_line, exp_line, comment, line_no, index = None): + super().__init__(nid, comment, line_no, index) self.sid_line = sid_line self.state_line = state_line self.exp_line = exp_line if not isinstance(sid_line, Sort): raise model_error("sort", line_no) if not isinstance(state_line, State): - raise model_error("state left operand", line_no) + raise model_error("state operand", line_no) if not isinstance(exp_line, Expression): - raise model_error("expression right operand", line_no) + 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) - if self.state_line.init_line == self.state_line: + +class Init(Transaction): + keyword = OP_INIT + + inits = dict() + + def __init__(self, nid, sid_line, state_line, exp_line, comment, line_no, index = None): + super().__init__(nid, sid_line, state_line, exp_line, comment, line_no, index) + if state_line.nid < exp_line.nid: + raise model_error("state after expression", 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_init() + if index is not None and not isinstance(sid_line, Bitvector): + raise model_error("bitvector", line_no) + if index is None: + self.array = self.new_array() + else: + self.index = index + self.new_init(index) def __str__(self): return f"{self.nid} {Init.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.comment}" - def new_init(self): - assert self not in Init.inits - Init.inits[self.nid] = self + def new_array(self): + if isinstance(self.exp_line.sid_line, Array): + return None + if isinstance(self.sid_line, Array) and self.sid_line.array_size_line.size <= ARRAY_SIZE_BOUND: + array = dict() + for index in range(2**self.sid_line.array_size_line.size): + array[index] = Init(self.nid, self.sid_line.element_size_line, + self.state_line.array[index], self.exp_line, self.comment, self.line_no, index) + return array + else: + return None + + def new_init(self, index = None): + if index is None: + assert self.nid not in Init.inits, f"init nid {self.nid} already defined @ {self.line_no}" + Init.inits[self.nid] = self - def set_z3(self, step): - if self.z3 is None: - if isinstance(self.sid_line, Array) and isinstance(self.exp_line.sid_line, Bitvec): - # initialize with constant array - self.z3 = self.state_line.get_z3() == z3.K(self.sid_line.array_size_line.get_z3(), - self.exp_line.get_z3()) - else: - self.z3 = self.state_line.get_z3() == self.exp_line.get_z3() + def get_z3_step(self, step): + assert step == 0, f"z3 init with {step} != 0" + if isinstance(self.sid_line, Array) and isinstance(self.exp_line.sid_line, Bitvec): + # initialize with constant array + return self.state_line.get_z3_step(0) == z3.K( + self.sid_line.array_size_line.get_z3(), + self.exp_line.get_z3()) + else: + return self.state_line.get_z3_step(0) == State.get_z3_select( + State.get_z3_lambda(self.exp_line.get_z3(), self.exp_line.domain), + self.exp_line.domain, 0) - def set_bitwuzla(self, step, tm): - assert step == 0 and step == self.step - if self.bitwuzla is None: - if isinstance(self.sid_line, Array) and isinstance(self.exp_line.sid_line, Bitvec): - # initialize with constant array - self.bitwuzla = tm.mk_term(bitwuzla.Kind.EQUAL, - [self.state_line.get_bitwuzla(0, tm), - tm.mk_const_array(self.sid_line.get_bitwuzla(0, tm), - self.exp_line.get_bitwuzla(0, tm))]) - else: - self.bitwuzla = tm.mk_term(bitwuzla.Kind.EQUAL, - [self.state_line.get_bitwuzla(0, tm), self.exp_line.get_bitwuzla(0, tm)]) + def get_bitwuzla_step(self, step, tm): + assert step == 0, f"bitwuzla init with {step} != 0" + if isinstance(self.sid_line, Array) and isinstance(self.exp_line.sid_line, Bitvec): + # initialize with constant array + return tm.mk_term(bitwuzla.Kind.EQUAL, + [self.state_line.get_bitwuzla_step(0, tm), + tm.mk_const_array(self.sid_line.get_bitwuzla(tm), + self.exp_line.get_bitwuzla(tm))]) + else: + return tm.mk_term(bitwuzla.Kind.EQUAL, + [self.state_line.get_bitwuzla_step(0, tm), + State.get_bitwuzla_select( + State.get_bitwuzla_lambda( + self.exp_line.get_bitwuzla(tm), self.exp_line.domain, tm), + self.exp_line.domain, 0, tm)]) -class Next(Line): - keyword = 'next' +class Next(Transaction): + keyword = OP_NEXT nexts = dict() def __init__(self, nid, sid_line, state_line, exp_line, comment, line_no): - super().__init__(nid, comment, line_no) - self.sid_line = sid_line - self.state_line = state_line - self.exp_line = exp_line - if not isinstance(sid_line, Sort): - raise model_error("sort", line_no) - if not isinstance(state_line, State): - raise model_error("state left operand", line_no) - if not isinstance(exp_line, Expression): - raise model_error("expression right 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_sorts(exp_line.sid_line): - raise model_error("compatible state and expression sorts", line_no) - if self.state_line.next_line == self.state_line: + super().__init__(nid, sid_line, state_line, exp_line, comment, line_no) + self.cache_z3_change = dict() + self.cache_bitwuzla_change = dict() + if self.state_line.next_line is None: self.state_line.next_line = self else: raise model_error("untransitioned state", line_no) - self.current_step = None - self.next_step = None self.new_next() def __str__(self): return f"{self.nid} {Next.keyword} {self.sid_line.nid} {self.state_line.nid} {self.exp_line.nid} {self.comment}" def new_next(self): - assert self not in Next.nexts + assert self.nid not in Next.nexts, f"next nid {self.nid} already defined @ {self.line_no}" Next.nexts[self.nid] = self - def set_z3(self, step): - if self.z3 is None: - self.current_step = self.state_line.get_z3() - else: - self.current_step = self.next_step - self.next_step = self.state_line.get_z3_step(step + 1) - self.z3 = self.next_step == self.exp_line.get_z3() - - def set_bitwuzla(self, step, tm): - assert step == 0 or step == self.step + 1 - if self.bitwuzla is None or step > self.step: - if step == 0: - self.current_step = self.state_line.get_bitwuzla(step, tm) - else: - self.current_step = self.next_step - self.next_step = self.state_line.get_bitwuzla_step(step + 1, tm) - self.bitwuzla = tm.mk_term(bitwuzla.Kind.EQUAL, - [self.next_step, self.exp_line.get_bitwuzla(step, tm)]) - self.step = step + def get_z3_step(self, step): + if self.z3_lambda_line is None: + self.z3_lambda_line = State.get_z3_lambda( + self.exp_line.get_z3(), self.exp_line.domain) + if step not in self.cache_z3: + self.cache_z3[step] = self.state_line.get_z3_step(step + 1) == State.get_z3_select( + self.z3_lambda_line, self.exp_line.domain, step) + return self.cache_z3[step] + + def get_z3_change(self, step): + if step not in self.cache_z3_change: + self.cache_z3_change[step] = self.state_line.get_z3_step(step + 1) != self.state_line.get_z3_step(step) + return self.cache_z3_change[step] -class Property(Line): - keywords = {'constraint', 'bad'} + def get_bitwuzla_step(self, step, tm): + if self.bitwuzla_lambda_line is None: + self.bitwuzla_lambda_line = State.get_bitwuzla_lambda( + self.exp_line.get_bitwuzla(tm), self.exp_line.domain, tm) + if step not in self.cache_bitwuzla: + self.cache_bitwuzla[step] = tm.mk_term(bitwuzla.Kind.EQUAL, + [self.state_line.get_bitwuzla_step(step + 1, tm), State.get_bitwuzla_select( + self.bitwuzla_lambda_line, self.exp_line.domain, step, tm)]) + return self.cache_bitwuzla[step] + + def get_bitwuzla_change(self, step, tm): + if step not in self.cache_bitwuzla_change: + self.cache_bitwuzla_change[step] = tm.mk_term(bitwuzla.Kind.DISTINCT, + [self.state_line.get_bitwuzla_step(step + 1, tm), + self.state_line.get_bitwuzla_step(step, tm)]) + return self.cache_bitwuzla_change[step] + +class Property(Sequential): + keywords = {OP_CONSTRAINT, OP_BAD} def __init__(self, nid, property_line, symbol, comment, line_no): super().__init__(nid, comment, line_no) @@ -916,18 +1102,26 @@ def __init__(self, nid, property_line, symbol, comment, line_no): if not isinstance(property_line.sid_line, Bool): raise model_error("Boolean operand", line_no) - def set_z3(self, step): - if self.z3 is None: - self.z3 = self.property_line.get_z3() + def get_z3_step(self, step): + if self.z3_lambda_line is None: + self.z3_lambda_line = State.get_z3_lambda( + self.property_line.get_z3(), self.property_line.domain) + if step not in self.cache_z3: + self.cache_z3[step] = State.get_z3_select( + self.z3_lambda_line, self.property_line.domain, step) + return self.cache_z3[step] - def set_bitwuzla(self, step, tm): - assert step == 0 or step == self.step + 1 - if self.bitwuzla is None or step > self.step: - self.bitwuzla = self.property_line.get_bitwuzla(step, tm) - self.step = step + def get_bitwuzla_step(self, step, tm): + if self.bitwuzla_lambda_line is None: + self.bitwuzla_lambda_line = State.get_bitwuzla_lambda( + self.property_line.get_bitwuzla(tm), self.property_line.domain, tm) + if step not in self.cache_bitwuzla: + self.cache_bitwuzla[step] = State.get_bitwuzla_select( + self.bitwuzla_lambda_line, self.property_line.domain, step, tm) + return self.cache_bitwuzla[step] class Constraint(Property): - keyword = 'constraint' + keyword = OP_CONSTRAINT constraints = dict() @@ -939,11 +1133,11 @@ 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 + 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 = 'bad' + keyword = OP_BAD bads = dict() @@ -955,7 +1149,7 @@ def __str__(self): return f"{self.nid} {Bad.keyword} {self.property_line.nid} {self.symbol} {self.comment}" def new_bad(self): - assert self not in Bad.bads + assert self.nid not in Bad.bads, f"bad nid {self.nid} already defined @ {self.line_no}" Bad.bads[self.nid] = self def get_class(keyword): @@ -1004,183 +1198,3057 @@ def get_class(keyword): elif keyword == Bad.keyword: return Bad -import re +current_nid = 0 -class syntax_error(Exception): - def __init__(self, expected, line_no): - super().__init__(f"syntax error in line {line_no}: {expected} expected") +def next_nid(): + global current_nid + current_nid += 1 + return current_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 new_boolean(nid = next_nid(), line_no = None): + return Bool(nid, "Boolean", line_no) -def get_token(tokens, expected, line_no): - try: - return tokens.pop(0) - except: - raise syntax_error(expected, line_no) +def new_bitvec(size_in_bits, comment, nid = next_nid(), line_no = None): + return Bitvec(nid, size_in_bits, comment, line_no) -def get_decimal(tokens, expected, line_no): - token = get_token(tokens, expected, line_no) - if token.isdecimal(): - return int(token) - else: - raise syntax_error(expected, line_no) +def new_array(address_sid, element_sid, comment, nid = next_nid(), line_no = None): + return Array(nid, address_sid, element_sid, comment, line_no) -def get_nid_line(tokens, clss, expected, line_no): - nid = get_decimal(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 new_zero_one(op, sid, comment, nid = next_nid(), line_no = None): + assert op in {OP_ZERO, OP_ONE} + return get_class(op)(nid, sid, comment, line_no) -def get_bool_or_bitvec_sid_line(tokens, line_no): - return get_nid_line(tokens, Bitvector, "Boolean or bitvector sort nid", line_no) +def new_constant(op, sid, constant, comment, nid = next_nid(), line_no = None): + assert op in {OP_CONSTD, OP_CONST, OP_CONSTH} + if op == OP_CONSTD: + if constant == 0: + return Zero(nid, sid, comment, line_no) + elif constant == 1: + return One(nid, sid, comment, line_no) + return get_class(op)(nid, sid, constant, comment, line_no) -def get_bitvec_sid_line(tokens, line_no): - return get_nid_line(tokens, Bitvec, "bitvector sort nid", line_no) +def new_input(op, sid, symbol, comment, nid = next_nid(), line_no = None): + assert op in Variable.keywords + return get_class(op)(nid, sid, symbol, comment, line_no) -def get_sid_line(tokens, line_no): - return get_nid_line(tokens, Sort, "sort nid", line_no) +def new_ext(op, sid, value_nid, w, comment, nid = next_nid(), line_no = None): + assert op in Ext.keywords + return get_class(op)(nid, op, sid, value_nid, w, comment, line_no) -def get_state_line(tokens, line_no): - return get_nid_line(tokens, State, "state nid", line_no) +def new_slice(sid, value_nid, u, l, comment, nid = next_nid(), line_no = None): + return Slice(nid, sid, value_nid, u, l, comment, line_no) -def get_exp_line(tokens, line_no): - return get_nid_line(tokens, Expression, "expression nid", line_no) +def new_unary(op, sid, value_nid, comment, nid = next_nid(), line_no = None): + assert op in Unary.keywords + return get_class(op)(nid, op, sid, value_nid, comment, line_no) -def get_number(tokens, base, expected, line_no): - token = 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 new_unary_boolean(op, value_nid, comment, nid = next_nid(), line_no = None): + assert op == OP_NOT + return get_class(op)(nid, op, SID_BOOLEAN, value_nid, comment, line_no) -def get_symbol(tokens): - try: - return get_token(tokens, None, None) - except: - return "" +def new_binary(op, sid, left_nid, right_nid, comment, nid = next_nid(), line_no = None): + assert op in Binary.keywords + return get_class(op)(nid, op, sid, left_nid, right_nid, comment, line_no) -def get_comment(tokens, line_no): - comment = get_symbol(tokens) - if comment != "": - if comment[0] != ';': - raise syntax_error("comment", line_no) - return comment +def new_binary_boolean(op, left_nid, right_nid, comment, nid = next_nid(), line_no = None): + assert op in Implies.keyword + Comparison.keywords + Logical.keywords + return get_class(op)(nid, op, SID_BOOLEAN, left_nid, right_nid, comment, line_no) -def parse_sort_line(tokens, nid, line_no): - token = get_token(tokens, "bitvector or array", line_no) - if token == Bitvec.keyword: - size = get_decimal(tokens, "bitvector size", line_no) - comment = get_comment(tokens, line_no) - # rotor-dependent Boolean declaration - if comment == "; Boolean" and size == 1: - return Bool(nid, comment, line_no) - else: - return Bitvec(nid, size, comment, line_no) - elif token == Array.keyword: - array_size_line = get_bitvec_sid_line(tokens, line_no) - element_size_line = get_bitvec_sid_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return Array(nid, array_size_line, element_size_line, comment, line_no) - else: - raise syntax_error("bitvector or array", line_no) +def new_ternary(op, sid, first_nid, second_nid, third_nid, comment, nid = next_nid(), line_no = None): + assert op in Ternary.keywords + return get_class(op)(nid, op, sid, first_nid, second_nid, third_nid, comment, line_no) -def parse_zero_one_line(tokens, nid, op, line_no): - sid_line = get_bool_or_bitvec_sid_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return get_class(op)(nid, sid_line, comment, line_no) +def new_init(sid, state_nid, value_nid, comment, nid = next_nid(), line_no = None): + return Init(nid, sid, state_nid, value_nid, comment, line_no) -def parse_constant_line(tokens, nid, op, line_no): - sid_line = get_bool_or_bitvec_sid_line(tokens, line_no) - if op == Constd.keyword: - value = get_number(tokens, 10, "signed integer", line_no) - elif op == Const.keyword: - value = get_number(tokens, 2, "binary number", line_no) - elif op == Consth.keyword: - value = get_number(tokens, 16, "hexadecimal number", line_no) - comment = get_comment(tokens, line_no) - return get_class(op)(nid, sid_line, value, comment, line_no) +def new_next(sid, state_nid, value_nid, comment, nid = next_nid(), line_no = None): + return Next(nid, sid, state_nid, value_nid, comment, line_no) -def parse_symbol_comment(tokens, line_no): - symbol = get_symbol(tokens) - comment = get_comment(tokens, line_no) - if symbol != "": - if symbol[0] == ';': - return "", symbol - return symbol, comment +def new_init_next(op, sid, state_nid, value_nid, comment, nid = next_nid(), line_no = None): + return get_class(op)(nid, sid, state_nid, value_nid, comment, line_no) -def parse_variable_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - symbol, comment = parse_symbol_comment(tokens, line_no) - return get_class(op)(nid, sid_line, symbol, comment, line_no) +def new_property(op, condition_nid, symbol, comment, nid = next_nid(), line_no = None): + assert op in Property.keywords + return get_class(op)(nid, condition_nid, symbol, comment, line_no) -def parse_ext_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - arg1_line = get_exp_line(tokens, line_no) - w = get_decimal(tokens, "bit width", line_no) - comment = get_comment(tokens, line_no) - return Ext(nid, op, sid_line, arg1_line, w, comment, line_no) +# RISC-V model generator -def parse_slice_line(tokens, nid, line_no): - sid_line = get_sid_line(tokens, line_no) - arg1_line = get_exp_line(tokens, line_no) - u = get_decimal(tokens, "upper bit", line_no) - l = get_decimal(tokens, "lower bit", line_no) - comment = get_comment(tokens, line_no) - return Slice(nid, sid_line, arg1_line, u, l, comment, line_no) +class system_error(Exception): + def __init__(self, message): + super().__init__(message) -def parse_unary_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - arg1_line = get_exp_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return Unary(nid, op, sid_line, arg1_line, comment, line_no) +# TODO: configure: -def parse_binary_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - arg1_line = get_exp_line(tokens, line_no) - arg2_line = get_exp_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return get_class(op)(nid, op, sid_line, arg1_line, arg2_line, comment, line_no) +IS64BITTARGET = True -def parse_ternary_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - arg1_line = get_exp_line(tokens, line_no) - arg2_line = get_exp_line(tokens, line_no) - arg3_line = get_exp_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return get_class(op)(nid, op, sid_line, arg1_line, arg2_line, arg3_line, comment, line_no) +SIZEOFUINT64INBITS = 64 -def parse_init_next_line(tokens, nid, op, line_no): - sid_line = get_sid_line(tokens, line_no) - state_line = get_state_line(tokens, line_no) - exp_line = get_exp_line(tokens, line_no) - comment = get_comment(tokens, line_no) - return get_class(op)(nid, sid_line, state_line, exp_line, comment, line_no) +# avoiding 64-bit integer overflow +UINT64_MAX = ((2**(SIZEOFUINT64INBITS - 1) - 1) << 1) + 1 -def parse_property_line(tokens, nid, op, line_no): - property_line = get_exp_line(tokens, line_no) - symbol, comment = parse_symbol_comment(tokens, line_no) - return get_class(op)(nid, property_line, symbol, comment, line_no) +WORDSIZE = 8 +WORDSIZEINBITS = 64 -current_nid = 0 +INSTRUCTIONSIZE = 4 -def parse_btor2_line(line, line_no): - global current_nid - if line.strip(): - tokens = tokenize_btor2(line) - token = get_token(tokens, None, None) +VIRTUALMEMORYSIZE = 4 # 4GB avoiding 32-bit integer overflow +GIGABYTE = 2**30 + +# unsigned integer arithmetic support + +def is_unsigned_integer(n, b): + assert 0 < b <= SIZEOFUINT64INBITS + if b == SIZEOFUINT64INBITS: + # avoiding 64-bit integer overflow + return 0 <= n <= UINT64_MAX + else: + return 0 <= n < 2**b + +def is_uint64(n): + return is_unsigned_integer(n, SIZEOFUINT64INBITS) + +def is_int64(n): + return is_signed_integer(n, SIZEOFUINT64INBITS) + +# ported from selfie library + +def get_bits(n, i, b): + assert is_uint64(n) + assert 0 <= i + b <= SIZEOFUINT64INBITS + assert 0 < b + if b < SIZEOFUINT64INBITS: + return (n >> i) % 2**b + else: + # avoiding 64-bit integer overflow + return n >> i + +def is_signed_integer(n, b): + assert is_uint64(n) + assert 0 < b <= SIZEOFUINT64INBITS + # avoiding 64-bit integer overflow + return 0 <= n < 2**(b - 1) or UINT64_MAX - 2**(b - 1) <= n - 1 < UINT64_MAX + +def sign_shrink(n, b): + assert is_uint64(n) + assert 0 < b <= SIZEOFUINT64INBITS + return get_bits(n, 0, b) + +# ported from rotor model + +def get_sid(line): + return line.sid_line + +# ported from rotor emulator + +def eval_bitvec_size(line): + assert isinstance(line, Bitvec) + # TODO: tolerating but not yet supporting double machine word bitvectors + assert (line.size > 0 and line.size <= SIZEOFUINT64INBITS) or line.size == 2 * WORDSIZEINBITS + return line.size; + +def fit_bitvec_sort(sid, value): + size = eval_bitvec_size(sid) + if size >= SIZEOFUINT64INBITS: + # TODO: support of bitvectors larger than machine words + return + elif is_unsigned_integer(value, size): + return + raise system_error(f"{value} does not fit {size}-bit bitvector") + +def signed_fit_bitvec_sort(sid, value): + size = eval_bitvec_size(sid) + if size >= SIZEOFUINT64INBITS: + # TODO: support of bitvectors larger than machine words + return + elif is_signed_integer(value, size): + return + fit_bitvec_sort(sid, value) + +def eval_constant_value(line): + # TODO: check if really needed + assert isinstance(line, Constant) + sid = get_sid(line) + value = line.value + if isinstance(line, Constd): + signed_fit_bitvec_sort(sid, value) + value = sign_shrink(value, eval_bitvec_size(sid)) + else: + fit_bitvec_sort(sid, value) + return value + +# machine interface + +SID_BOOLEAN = None + +NID_FALSE = None +NID_TRUE = None + +SID_BYTE = None + +NID_BYTE_0 = None +NID_BYTE_3 = None + +HALFWORDSIZEINBITS = 16 + +SID_HALF_WORD = None + +NID_HALF_WORD_0 = None +NID_HALF_WORD_1 = None + +SINGLEWORDSIZEINBITS = 32 + +SID_SINGLE_WORD = None + +NID_SINGLE_WORD_0 = None +NID_SINGLE_WORD_1 = None +NID_SINGLE_WORD_2 = None +NID_SINGLE_WORD_3 = None +NID_SINGLE_WORD_4 = None +NID_SINGLE_WORD_5 = None +NID_SINGLE_WORD_6 = None +NID_SINGLE_WORD_7 = None +NID_SINGLE_WORD_8 = None + +NID_SINGLE_WORD_MINUS_1 = None +NID_SINGLE_WORD_INT_MIN = None + +DOUBLEWORDSIZE = 8 +DOUBLEWORDSIZEINBITS = 64 + +SID_DOUBLE_WORD = None + +NID_DOUBLE_WORD_0 = None +NID_DOUBLE_WORD_1 = None +NID_DOUBLE_WORD_2 = None +NID_DOUBLE_WORD_3 = None +NID_DOUBLE_WORD_4 = None +NID_DOUBLE_WORD_5 = None +NID_DOUBLE_WORD_6 = None +NID_DOUBLE_WORD_7 = None +NID_DOUBLE_WORD_8 = None + +NID_DOUBLE_WORD_MINUS_1 = None +NID_DOUBLE_WORD_INT_MIN = None + +SID_MACHINE_WORD = None + +NID_MACHINE_WORD_0 = None +NID_MACHINE_WORD_1 = None +NID_MACHINE_WORD_2 = None +NID_MACHINE_WORD_3 = None +NID_MACHINE_WORD_4 = None +NID_MACHINE_WORD_5 = None +NID_MACHINE_WORD_6 = None +NID_MACHINE_WORD_7 = None +NID_MACHINE_WORD_8 = None + +NID_MACHINE_WORD_MINUS_1 = None +NID_MACHINE_WORD_INT_MIN = None + +NID_LSB_MASK = None + +SID_DOUBLE_MACHINE_WORD = None + +def init_machine_interface(): + global SID_BOOLEAN + + global NID_FALSE + global NID_TRUE + + global SID_BYTE + + global NID_BYTE_0 + global NID_BYTE_3 + + global SID_HALF_WORD + + global NID_HALF_WORD_0 + global NID_HALF_WORD_1 + + global SID_SINGLE_WORD + + global NID_SINGLE_WORD_0 + global NID_SINGLE_WORD_1 + global NID_SINGLE_WORD_2 + global NID_SINGLE_WORD_3 + global NID_SINGLE_WORD_4 + global NID_SINGLE_WORD_5 + global NID_SINGLE_WORD_6 + global NID_SINGLE_WORD_7 + global NID_SINGLE_WORD_8 + + global NID_SINGLE_WORD_MINUS_1 + global NID_SINGLE_WORD_INT_MIN + + global SID_DOUBLE_WORD + + global NID_DOUBLE_WORD_0 + global NID_DOUBLE_WORD_1 + global NID_DOUBLE_WORD_2 + global NID_DOUBLE_WORD_3 + global NID_DOUBLE_WORD_4 + global NID_DOUBLE_WORD_5 + global NID_DOUBLE_WORD_6 + global NID_DOUBLE_WORD_7 + global NID_DOUBLE_WORD_8 + + global NID_DOUBLE_WORD_MINUS_1 + global NID_DOUBLE_WORD_INT_MIN + + global SID_MACHINE_WORD + + global NID_MACHINE_WORD_0 + global NID_MACHINE_WORD_1 + global NID_MACHINE_WORD_2 + global NID_MACHINE_WORD_3 + global NID_MACHINE_WORD_4 + global NID_MACHINE_WORD_5 + global NID_MACHINE_WORD_6 + global NID_MACHINE_WORD_7 + global NID_MACHINE_WORD_8 + + global NID_MACHINE_WORD_MINUS_1 + global NID_MACHINE_WORD_INT_MIN + + global NID_LSB_MASK + + global SID_DOUBLE_MACHINE_WORD + + SID_BOOLEAN = new_boolean() + + NID_FALSE = new_constant(OP_CONSTD, SID_BOOLEAN, 0, "false") + NID_TRUE = new_constant(OP_CONSTD, SID_BOOLEAN, 1, "true") + + SID_BYTE = new_bitvec(8, "8-bit byte") + + NID_BYTE_0 = new_constant(OP_CONSTD, SID_BYTE, 0, "byte 0") + NID_BYTE_3 = new_constant(OP_CONSTD, SID_BYTE, 3, "byte 3") + + SID_HALF_WORD = new_bitvec(HALFWORDSIZEINBITS, "16-bit half word") + + NID_HALF_WORD_0 = new_constant(OP_CONSTD, SID_HALF_WORD, 0, "half word 0") + NID_HALF_WORD_1 = new_constant(OP_CONSTD, SID_HALF_WORD, 1, "half word 1") + + SID_SINGLE_WORD = new_bitvec(SINGLEWORDSIZEINBITS, "32-bit single word") + + NID_SINGLE_WORD_0 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 0, "single-word 0") + NID_SINGLE_WORD_1 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 1, "single-word 1") + NID_SINGLE_WORD_2 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 2, "single-word 2") + NID_SINGLE_WORD_3 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 3, "single-word 3") + NID_SINGLE_WORD_4 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 4, "single-word 4") + NID_SINGLE_WORD_5 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 5, "single-word 5") + NID_SINGLE_WORD_6 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 6, "single-word 6") + NID_SINGLE_WORD_7 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 7, "single-word 7") + NID_SINGLE_WORD_8 = new_constant(OP_CONSTD, SID_SINGLE_WORD, 8, "single-word 8") + + NID_SINGLE_WORD_MINUS_1 = new_constant(OP_CONSTD, SID_SINGLE_WORD, -1, "single-word -1") + NID_SINGLE_WORD_INT_MIN = new_constant(OP_CONSTH, SID_SINGLE_WORD, 2**(SINGLEWORDSIZEINBITS - 1), "single-word INT_MIN") + + SID_DOUBLE_WORD = new_bitvec(DOUBLEWORDSIZEINBITS, "64-bit double word") + + NID_DOUBLE_WORD_0 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 0, "double-word 0") + NID_DOUBLE_WORD_1 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 1, "double-word 1") + NID_DOUBLE_WORD_2 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 2, "double-word 2") + NID_DOUBLE_WORD_3 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 3, "double-word 3") + NID_DOUBLE_WORD_4 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 4, "double-word 4") + NID_DOUBLE_WORD_5 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 5, "double-word 5") + NID_DOUBLE_WORD_6 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 6, "double-word 6") + NID_DOUBLE_WORD_7 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 7, "double-word 7") + NID_DOUBLE_WORD_8 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, 8, "double-word 8") + + NID_DOUBLE_WORD_MINUS_1 = new_constant(OP_CONSTD, SID_DOUBLE_WORD, -1, "double-word -1") + + if IS64BITTARGET: + NID_DOUBLE_WORD_INT_MIN = new_constant(OP_CONSTH, SID_DOUBLE_WORD, 2**(DOUBLEWORDSIZEINBITS - 1), "double-word INT_MIN") + + SID_MACHINE_WORD = SID_DOUBLE_WORD + + NID_MACHINE_WORD_0 = NID_DOUBLE_WORD_0 + NID_MACHINE_WORD_1 = NID_DOUBLE_WORD_1 + NID_MACHINE_WORD_2 = NID_DOUBLE_WORD_2 + NID_MACHINE_WORD_3 = NID_DOUBLE_WORD_3 + NID_MACHINE_WORD_4 = NID_DOUBLE_WORD_4 + NID_MACHINE_WORD_5 = NID_DOUBLE_WORD_5 + NID_MACHINE_WORD_6 = NID_DOUBLE_WORD_6 + NID_MACHINE_WORD_7 = NID_DOUBLE_WORD_7 + NID_MACHINE_WORD_8 = NID_DOUBLE_WORD_8 + + NID_MACHINE_WORD_MINUS_1 = NID_DOUBLE_WORD_MINUS_1 + NID_MACHINE_WORD_INT_MIN = NID_DOUBLE_WORD_INT_MIN + else: + # 32-bit system + SID_MACHINE_WORD = SID_SINGLE_WORD + + NID_MACHINE_WORD_0 = NID_SINGLE_WORD_0 + NID_MACHINE_WORD_1 = NID_SINGLE_WORD_1 + NID_MACHINE_WORD_2 = NID_SINGLE_WORD_2 + NID_MACHINE_WORD_3 = NID_SINGLE_WORD_3 + NID_MACHINE_WORD_4 = NID_SINGLE_WORD_4 + NID_MACHINE_WORD_5 = NID_SINGLE_WORD_5 + NID_MACHINE_WORD_6 = NID_SINGLE_WORD_6 + NID_MACHINE_WORD_7 = NID_SINGLE_WORD_7 + NID_MACHINE_WORD_8 = NID_SINGLE_WORD_8 + + NID_MACHINE_WORD_MINUS_1 = NID_SINGLE_WORD_MINUS_1 + NID_MACHINE_WORD_INT_MIN = NID_SINGLE_WORD_INT_MIN + + NID_LSB_MASK = new_constant(OP_CONSTD, SID_MACHINE_WORD, -2, "all bits but LSB set") + + SID_DOUBLE_MACHINE_WORD = new_bitvec(2 * WORDSIZEINBITS, "double machine word") + +# kernel interface + +MAX_STRING_LENGTH = 128 + +NID_MAX_STRING_LENGTH = None + +SYSCALL_EXIT = 93; +SYSCALL_BRK = 214; +SYSCALL_OPENAT = 56; +SYSCALL_OPEN = 1024 # legacy syscall +SYSCALL_READ = 63; +SYSCALL_WRITE = 64; + +NID_EXIT_SYSCALL_ID = None +NID_BRK_SYSCALL_ID = None +NID_OPENAT_SYSCALL_ID = None +NID_OPEN_SYSCALL_ID = None +NID_READ_SYSCALL_ID = None +NID_WRITE_SYSCALL_ID = None + +BYTES_TO_READ = 1 + +NID_BYTES_TO_READ = None + +INPUT_ADDRESS_SPACE = 1 + +SID_INPUT_ADDRESS = None +SID_INPUT_BUFFER = None + +def init_kernel_interface(): + global NID_MAX_STRING_LENGTH + + global NID_EXIT_SYSCALL_ID + global NID_BRK_SYSCALL_ID + global NID_OPENAT_SYSCALL_ID + global NID_OPEN_SYSCALL_ID + global NID_READ_SYSCALL_ID + global NID_WRITE_SYSCALL_ID + + global NID_BYTES_TO_READ + + global INPUT_ADDRESS_SPACE + + global SID_INPUT_ADDRESS + global SID_INPUT_BUFFER + + NID_MAX_STRING_LENGTH = new_constant(OP_CONSTD, SID_MACHINE_WORD, + MAX_STRING_LENGTH, "maximum string length") + + NID_EXIT_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_EXIT, f"exit syscall ID {SYSCALL_EXIT:b}") + NID_BRK_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_BRK, f"brk syscall ID {SYSCALL_BRK:b}") + NID_OPENAT_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_OPENAT, f"openat syscall ID {SYSCALL_OPENAT:b}") + NID_OPEN_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_OPEN, f"open syscall ID {SYSCALL_OPEN:b}") + NID_READ_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_READ, f"read syscall ID {SYSCALL_READ:b}") + NID_WRITE_SYSCALL_ID = new_constant(OP_CONSTD, SID_MACHINE_WORD, + SYSCALL_WRITE, f"write syscall ID {SYSCALL_WRITE:b}") + + NID_BYTES_TO_READ = new_constant(OP_CONSTD, SID_MACHINE_WORD, BYTES_TO_READ, "bytes to read") + + INPUT_ADDRESS_SPACE = calculate_address_space(BYTES_TO_READ, 8) + + SID_INPUT_ADDRESS = new_bitvec(INPUT_ADDRESS_SPACE, f"{INPUT_ADDRESS_SPACE}-bit input address") + SID_INPUT_BUFFER = new_array(SID_INPUT_ADDRESS, SID_BYTE, "input buffer") + +def get_power_of_two_size_in_bytes(size_in_bits): + assert size_in_bits % 8 == 0 + size_in_bits = size_in_bits // 8 + assert size_in_bits == 2**int(math.log2(size_in_bits)) + return size_in_bits + +def calculate_address_space(number_of_bytes, word_size_in_bits): + if number_of_bytes < 2 * get_power_of_two_size_in_bytes(word_size_in_bits): + number_of_bytes = 2 * get_power_of_two_size_in_bytes(word_size_in_bits) + + size_in_words = math.ceil(number_of_bytes / get_power_of_two_size_in_bytes(word_size_in_bits)) + address_space = int(math.log2(size_in_words)) + + if size_in_words > 2**address_space: + address_space += 1 + + return address_space + +# register sorts and specification + +SID_REGISTER_ADDRESS = None + +REG_ZR = 0 +REG_RA = 1 +REG_SP = 2 +REG_GP = 3 +REG_TP = 4 +REG_T0 = 5 +REG_T1 = 6 +REG_T2 = 7 +REG_S0 = 8 +REG_S1 = 9 +REG_A0 = 10 +REG_A1 = 11 +REG_A2 = 12 +REG_A3 = 13 +REG_A4 = 14 +REG_A5 = 15 +REG_A6 = 16 +REG_A7 = 17 +REG_S2 = 18 +REG_S3 = 19 +REG_S4 = 20 +REG_S5 = 21 +REG_S6 = 22 +REG_S7 = 23 +REG_S8 = 24 +REG_S9 = 25 +REG_S10 = 26 +REG_S11 = 27 +REG_T3 = 28 +REG_T4 = 29 +REG_T5 = 30 +REG_T6 = 31 + +NID_ZR = None +NID_RA = None +NID_SP = None +NID_GP = None +NID_TP = None +NID_T0 = None +NID_T1 = None +NID_T2 = None +NID_S0 = None +NID_S1 = None +NID_A0 = None +NID_A1 = None +NID_A2 = None +NID_A3 = None +NID_A4 = None +NID_A5 = None +NID_A6 = None +NID_A7 = None +NID_S2 = None +NID_S3 = None +NID_S4 = None +NID_S5 = None +NID_S6 = None +NID_S7 = None +NID_S8 = None +NID_S9 = None +NID_S10 = None +NID_S11 = None +NID_T3 = None +NID_T4 = None +NID_T5 = None +NID_T6 = None + +SID_REGISTER_STATE = None + +def init_register_file_sorts(): + global SID_REGISTER_ADDRESS + + global NID_ZR + global NID_RA + global NID_SP + global NID_GP + global NID_TP + global NID_T0 + global NID_T1 + global NID_T2 + global NID_S0 + global NID_S1 + global NID_A0 + global NID_A1 + global NID_A2 + global NID_A3 + global NID_A4 + global NID_A5 + global NID_A6 + global NID_A7 + global NID_S2 + global NID_S3 + global NID_S4 + global NID_S5 + global NID_S6 + global NID_S7 + global NID_S8 + global NID_S9 + global NID_S10 + global NID_S11 + global NID_T3 + global NID_T4 + global NID_T5 + global NID_T6 + + global SID_REGISTER_STATE + + SID_REGISTER_ADDRESS = new_bitvec(5, "5-bit register address") + + NID_ZR = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_ZR, "zero") + NID_RA = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_RA, "ra") + NID_SP = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_SP, "sp") + NID_GP = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_GP, "gp") + NID_TP = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_TP, "tp") + NID_T0 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T0, "t0") + NID_T1 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T1, "t1") + NID_T2 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T2, "t2") + NID_S0 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S0, "s0") # used to be fp + NID_S1 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S1, "s1") + NID_A0 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A0, "a0") + NID_A1 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A1, "a1") + NID_A2 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A2, "a2") + NID_A3 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A3, "a3") + NID_A4 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A4, "a4") + NID_A5 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A5, "a5") + NID_A6 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A6, "a6") + NID_A7 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_A7, "a7") + NID_S2 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S2, "s2") + NID_S3 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S3, "s3") + NID_S4 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S4, "s4") + NID_S5 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S5, "s5") + NID_S6 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S6, "s6") + NID_S7 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S7, "s7") + NID_S8 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S8, "s8") + NID_S9 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S9, "s9") + NID_S10 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S10, "s10") + NID_S11 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_S11, "s11") + NID_T3 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T3, "t3") + NID_T4 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T4, "t4") + NID_T5 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T5, "t5") + NID_T6 = new_constant(OP_CONST, SID_REGISTER_ADDRESS, REG_T6, "t6") + + SID_REGISTER_STATE = new_array(SID_REGISTER_ADDRESS, SID_MACHINE_WORD, "register state") + +def load_register_value(reg_nid, comment, register_file_nid): + return new_binary(OP_READ, SID_MACHINE_WORD, register_file_nid, reg_nid, comment) + +def store_register_value(reg_nid, value_nid, comment, register_file_nid): + return new_ternary(OP_WRITE, SID_REGISTER_STATE, register_file_nid, reg_nid, value_nid, comment) + +def get_5_bit_shamt(value_nid): + return new_ext(OP_UEXT, SID_SINGLE_WORD, + new_slice(SID_5_BIT_IMM, value_nid, 4, 0, "get 5-bit shamt"), + SINGLEWORDSIZEINBITS - 5, + "unsigned-extend 5-bit shamt") + +def get_shamt(value_nid): + if IS64BITTARGET: + return new_ext(OP_UEXT, SID_MACHINE_WORD, + new_slice(SID_6_BIT_IMM, value_nid, 5, 0, "get 6-bit shamt"), + WORDSIZEINBITS - 6, + "unsigned-extend 6-bit shamt") + else: + return get_5_bit_shamt(value_nid) + +# memory sorts and specification + +# virtual address space + +VIRTUAL_ADDRESS_SPACE = 32 # number of bits in virtual addresses + +SID_VIRTUAL_ADDRESS = None + +NID_VIRTUAL_ADDRESS_0 = None +NID_VIRTUAL_ADDRESS_1 = None +NID_VIRTUAL_ADDRESS_2 = None +NID_VIRTUAL_ADDRESS_3 = None +NID_VIRTUAL_ADDRESS_4 = None +NID_VIRTUAL_ADDRESS_5 = None +NID_VIRTUAL_ADDRESS_6 = None +NID_VIRTUAL_ADDRESS_7 = None +NID_VIRTUAL_ADDRESS_8 = None + +NID_VIRTUAL_HALF_WORD_SIZE = None +NID_VIRTUAL_SINGLE_WORD_SIZE = None +NID_VIRTUAL_DOUBLE_WORD_SIZE = None + +NID_VIRTUAL_HALF_WORD_SIZE_MINUS_1 = None +NID_VIRTUAL_SINGLE_WORD_SIZE_MINUS_1 = None +NID_VIRTUAL_DOUBLE_WORD_SIZE_MINUS_1 = None + +NID_HIGHEST_VIRTUAL_ADDRESS = None + +# code segment + +CODEWORDSIZEINBITS = 32 + +SID_CODE_WORD = None + +NID_CODE_WORD_0 = None + +CODE_ADDRESS_SPACE = 0 # number of bits in code segment addresses + +SID_CODE_ADDRESS = None +SID_CODE_STATE = None + +max_code_size = 0 + +code_start = 0 +code_size = 0 + +NID_CODE_START = None +NID_CODE_END = None + +# main memory + +MEMORYWORDSIZEINBITS = 64 + +SID_MEMORY_WORD = None + +NID_MEMORY_WORD_0 = None + +# data segment + +DATA_ADDRESS_SPACE = 1 # number of bits in data segment addresses + +SID_DATA_ADDRESS = None +SID_DATA_STATE = None + +max_data_size = 0 + +data_start = 0 +data_size = 0 + +NID_DATA_START = None +NID_DATA_END = None + +# heap segment + +HEAP_ADDRESS_SPACE = 1 # number of bits in heap segment addresses + +SID_HEAP_ADDRESS = None +SID_HEAP_STATE = None + +heap_initial_size = 0 +heap_allowance = 4096 # must be multiple of WORDSIZE + +heap_start = 0 +heap_size = 0 + +NID_HEAP_START = None +NID_HEAP_END = None + +# stack segment + +STACK_ADDRESS_SPACE = 1 # number of bits in stack segment addresses + +SID_STACK_ADDRESS = None +SID_STACK_STATE = None + +stack_initial_size = 0 +stack_allowance = 2048 # must be multiple of WORDSIZE > 0 + +stack_start = 0 +stack_size = 0 + +NID_STACK_START = None +NID_STACK_END = None + +# bit masks and factors + +NID_HALF_WORD_SIZE_MASK = None +NID_SINGLE_WORD_SIZE_MASK = None +NID_DOUBLE_WORD_SIZE_MASK = None + +NID_BYTE_MASK = None +NID_HALF_WORD_MASK = None +NID_SINGLE_WORD_MASK = None + +NID_SINGLE_WORD_SIZE_MINUS_HALF_WORD_SIZE = None +NID_DOUBLE_WORD_SIZE_MINUS_HALF_WORD_SIZE = None +NID_DOUBLE_WORD_SIZE_MINUS_SINGLE_WORD_SIZE = None + +NID_BYTE_SIZE_IN_BASE_BITS = None + +def init_memory_sorts(): + global VIRTUAL_ADDRESS_SPACE + + global SID_VIRTUAL_ADDRESS + + global NID_VIRTUAL_ADDRESS_0 + global NID_VIRTUAL_ADDRESS_1 + global NID_VIRTUAL_ADDRESS_2 + global NID_VIRTUAL_ADDRESS_3 + global NID_VIRTUAL_ADDRESS_4 + global NID_VIRTUAL_ADDRESS_5 + global NID_VIRTUAL_ADDRESS_6 + global NID_VIRTUAL_ADDRESS_7 + global NID_VIRTUAL_ADDRESS_8 + + global NID_VIRTUAL_HALF_WORD_SIZE + global NID_VIRTUAL_SINGLE_WORD_SIZE + global NID_VIRTUAL_DOUBLE_WORD_SIZE + + global NID_VIRTUAL_HALF_WORD_SIZE_MINUS_1 + global NID_VIRTUAL_SINGLE_WORD_SIZE_MINUS_1 + global NID_VIRTUAL_DOUBLE_WORD_SIZE_MINUS_1 + + global NID_HIGHEST_VIRTUAL_ADDRESS + + global CODEWORDSIZEINBITS + + global SID_CODE_WORD + + global NID_CODE_WORD_0 + + global CODE_ADDRESS_SPACE + + global SID_CODE_ADDRESS + global SID_CODE_STATE + + global NID_CODE_START + global NID_CODE_END + + global MEMORYWORDSIZEINBITS + + global SID_MEMORY_WORD + + global NID_MEMORY_WORD_0 + + global DATA_ADDRESS_SPACE + + global SID_DATA_ADDRESS + global SID_DATA_STATE + + global NID_DATA_START + global NID_DATA_END + + global HEAP_ADDRESS_SPACE + + global SID_HEAP_ADDRESS + global SID_HEAP_STATE + + global NID_HEAP_START + global NID_HEAP_END + + global STACK_ADDRESS_SPACE + + global SID_STACK_ADDRESS + global SID_STACK_STATE + + global NID_STACK_START + global NID_STACK_END + + global NID_HALF_WORD_SIZE_MASK + global NID_SINGLE_WORD_SIZE_MASK + global NID_DOUBLE_WORD_SIZE_MASK + + global NID_BYTE_MASK + global NID_HALF_WORD_MASK + global NID_SINGLE_WORD_MASK + + global NID_SINGLE_WORD_SIZE_MINUS_HALF_WORD_SIZE + global NID_DOUBLE_WORD_SIZE_MINUS_HALF_WORD_SIZE + global NID_DOUBLE_WORD_SIZE_MINUS_SINGLE_WORD_SIZE + + global NID_BYTE_SIZE_IN_BASE_BITS + + if VIRTUAL_ADDRESS_SPACE < WORDSIZEINBITS: + NID_HIGHEST_VIRTUAL_ADDRESS = new_constant(OP_CONSTD, SID_MACHINE_WORD, + 2**VIRTUAL_ADDRESS_SPACE - 1, "highest virtual address") + elif VIRTUAL_ADDRESS_SPACE > WORDSIZEINBITS: + VIRTUAL_ADDRESS_SPACE = WORDSIZEINBITS + + SID_VIRTUAL_ADDRESS = new_bitvec(VIRTUAL_ADDRESS_SPACE, f"{VIRTUAL_ADDRESS_SPACE}-bit virtual address") + + NID_VIRTUAL_ADDRESS_0 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 0, "virtual address 0") + NID_VIRTUAL_ADDRESS_1 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 1, "virtual address 1") + NID_VIRTUAL_ADDRESS_2 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 2, "virtual address 2") + NID_VIRTUAL_ADDRESS_3 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 3, "virtual address 3") + NID_VIRTUAL_ADDRESS_4 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 4, "virtual address 4") + NID_VIRTUAL_ADDRESS_5 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 5, "virtual address 5") + NID_VIRTUAL_ADDRESS_6 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 6, "virtual address 6") + NID_VIRTUAL_ADDRESS_7 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 7, "virtual address 7") + NID_VIRTUAL_ADDRESS_8 = new_constant(OP_CONSTD, SID_VIRTUAL_ADDRESS, 8, "virtual address 8") + + NID_VIRTUAL_HALF_WORD_SIZE = NID_VIRTUAL_ADDRESS_2 + NID_VIRTUAL_SINGLE_WORD_SIZE = NID_VIRTUAL_ADDRESS_4 + NID_VIRTUAL_DOUBLE_WORD_SIZE = NID_VIRTUAL_ADDRESS_8 + + NID_VIRTUAL_HALF_WORD_SIZE_MINUS_1 = NID_VIRTUAL_ADDRESS_1 + NID_VIRTUAL_SINGLE_WORD_SIZE_MINUS_1 = NID_VIRTUAL_ADDRESS_3 + NID_VIRTUAL_DOUBLE_WORD_SIZE_MINUS_1 = NID_VIRTUAL_ADDRESS_7 + + # code segment + + if CODEWORDSIZEINBITS > WORDSIZEINBITS: + CODEWORDSIZEINBITS = WORDSIZEINBITS + + SID_CODE_WORD = new_bitvec(CODEWORDSIZEINBITS, f"{CODEWORDSIZEINBITS}-bit code word") + + NID_CODE_WORD_0 = new_constant(OP_CONSTD, SID_CODE_WORD, 0, "code word 0") + + assert max_code_size >= WORDSIZE + + CODE_ADDRESS_SPACE = calculate_address_space(max_code_size, eval_bitvec_size(SID_CODE_WORD)) + + SID_CODE_ADDRESS = new_bitvec(CODE_ADDRESS_SPACE, f"{CODE_ADDRESS_SPACE}-bit code segment address") + + SID_CODE_STATE = new_array(SID_CODE_ADDRESS, SID_CODE_WORD, "code segment state") + + # main memory + + if MEMORYWORDSIZEINBITS > WORDSIZEINBITS: + MEMORYWORDSIZEINBITS = WORDSIZEINBITS + + SID_MEMORY_WORD = new_bitvec(MEMORYWORDSIZEINBITS, f"{MEMORYWORDSIZEINBITS}-bit memory word") + + NID_MEMORY_WORD_0 = new_constant(OP_CONSTD, SID_MEMORY_WORD, 0, "memory word 0") + + DATA_ADDRESS_SPACE = calculate_address_space(max_data_size, eval_bitvec_size(SID_MEMORY_WORD)) + + SID_DATA_ADDRESS = new_bitvec(DATA_ADDRESS_SPACE, + f"{DATA_ADDRESS_SPACE}-bit physical data segment address") + + SID_DATA_STATE = new_array(SID_DATA_ADDRESS, SID_MEMORY_WORD, "data segment state") + + # heap segment + + HEAP_ADDRESS_SPACE = calculate_address_space(heap_allowance, eval_bitvec_size(SID_MEMORY_WORD)) + + SID_HEAP_ADDRESS = new_bitvec(HEAP_ADDRESS_SPACE, + f"{HEAP_ADDRESS_SPACE}-bit physical heap segment address") + + SID_HEAP_STATE = new_array(SID_HEAP_ADDRESS, SID_MEMORY_WORD, "heap segment state") + + # stack segment + + STACK_ADDRESS_SPACE = calculate_address_space(stack_allowance, eval_bitvec_size(SID_MEMORY_WORD)) + + SID_STACK_ADDRESS = new_bitvec(STACK_ADDRESS_SPACE, + f"{STACK_ADDRESS_SPACE}-bit physical stack segment address") + + SID_STACK_STATE = new_array(SID_STACK_ADDRESS, SID_MEMORY_WORD, "stack segment state"); + + # bit masks and factors + + NID_HALF_WORD_SIZE_MASK = NID_VIRTUAL_ADDRESS_1 + NID_SINGLE_WORD_SIZE_MASK = NID_VIRTUAL_ADDRESS_3 + NID_DOUBLE_WORD_SIZE_MASK = NID_VIRTUAL_ADDRESS_7 + + NID_BYTE_MASK = new_constant(OP_CONSTH, SID_BYTE, 255, "maximum byte value") + NID_HALF_WORD_MASK = new_constant(OP_CONSTH, SID_HALF_WORD, 65535, "maximum half-word value") + NID_SINGLE_WORD_MASK = new_constant(OP_CONSTH, SID_SINGLE_WORD, 4294967295, "maximum single-word value") + + NID_SINGLE_WORD_SIZE_MINUS_HALF_WORD_SIZE = NID_VIRTUAL_ADDRESS_2 + NID_DOUBLE_WORD_SIZE_MINUS_HALF_WORD_SIZE = NID_VIRTUAL_ADDRESS_6 + NID_DOUBLE_WORD_SIZE_MINUS_SINGLE_WORD_SIZE = NID_VIRTUAL_ADDRESS_4 + + NID_BYTE_SIZE_IN_BASE_BITS = NID_VIRTUAL_ADDRESS_3 + +def new_segmentation(): + global NID_CODE_START + global NID_CODE_END + + global NID_DATA_START + global NID_DATA_END + + global NID_HEAP_START + global NID_HEAP_END + + global NID_STACK_START + global NID_STACK_END + + NID_CODE_START = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, code_start, + f"start of code segment @ 0x{code_start:X}") + + NID_CODE_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, code_start + code_size, + f"end of code segment accommodating at least {code_size // INSTRUCTIONSIZE} instructions") + + assert data_start >= code_start + code_size > 0 + + NID_DATA_START = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, data_start, + f"start of data segment @ 0x{data_start:X}") + + NID_DATA_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, data_start + data_size, + f"end of data segment accommodating {data_size} bytes") + + assert heap_start >= data_start + data_size > 0 + + NID_HEAP_START = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, heap_start, + f"start of heap segment @ 0x{heap_start:X}") + + NID_HEAP_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, heap_start + heap_size, + f"static end of heap segment accommodating {heap_size} bytes") + + assert stack_start >= heap_start + heap_size > 0 + + NID_STACK_START = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, stack_start, + f"static start of stack segment @ 0x{stack_start:X}") + + stack_end = stack_start + stack_size + + if stack_start < stack_end: + low_stack_address_space = int(math.log2(stack_end)) + up_stack_address_space = low_stack_address_space + + if stack_end > 2**low_stack_address_space: + up_stack_address_space += 1 + + if up_stack_address_space < VIRTUAL_ADDRESS_SPACE: + NID_STACK_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, stack_end, + f"end of stack segment accommodating {stack_size} bytes") + elif up_stack_address_space == VIRTUAL_ADDRESS_SPACE: + if low_stack_address_space < up_stack_address_space: + NID_STACK_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, stack_end, + f"end of stack segment accommodating {stack_size} bytes") + else: + NID_STACK_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, 0, + f"end of stack segment accommodating {stack_size} bytes") + else: + raise system_error(f"end of stack segment at 0x{stack_end:X} does not fit {VIRTUAL_ADDRESS_SPACE}-bit virtual address space") + + elif stack_end == 0: + if VIRTUAL_ADDRESS_SPACE == WORDSIZEINBITS: + NID_STACK_END = new_constant(OP_CONSTH, SID_VIRTUAL_ADDRESS, 0, + f"end of stack segment accommodating {stack_size} bytes") + else: + raise system_error(f"end of stack segment wrapped around to 0x0") + else: + raise system_error(f"end of stack segment wrapped around to 0x{stack_end:X}") + +def select_segment_feature(segment_nid, code_nid, data_nid, heap_nid, stack_nid): + sid = get_sid(segment_nid) + + if sid == SID_CODE_STATE: + return code_nid + elif sid == SID_DATA_STATE: + return data_nid + elif sid == SID_HEAP_STATE: + return heap_nid + elif sid == SID_STACK_STATE: + return stack_nid + else: + return UNUSED + +def get_segment_start(segment_nid): + return select_segment_feature(segment_nid, + NID_CODE_START, NID_DATA_START, NID_HEAP_START, NID_STACK_START) + +def get_segment_end(segment_nid): + return select_segment_feature(segment_nid, + NID_CODE_END, NID_DATA_END, NID_HEAP_END, NID_STACK_END) + +def is_block_in_segment(start_nid, end_nid, segment_nid): + start_comparison_nid = new_binary_boolean(OP_UGTE, + start_nid, + get_segment_start(segment_nid), + "virtual address of start of block >= start of segment?") + + if eval_constant_value(get_segment_end(segment_nid)) == 0: + # comparing with end of segment is unnecessary since end wrapped around to zero + return start_comparison_nid + else: + # assert: block and segment start <= end + return new_binary_boolean(OP_AND, + start_comparison_nid, + new_binary_boolean(OP_ULT, + end_nid, + get_segment_end(segment_nid), + "virtual address of end of block < end of segment?"), + "block in segment?") + +def is_virtual_address_in_segment(vaddr_nid, segment_nid): + return is_block_in_segment(vaddr_nid, vaddr_nid, segment_nid) + +def vaddr_to_laddr(vaddr_nid, segment_nid): + # TODO: distinguish linear addresses from virtual addresses + return new_binary(OP_SUB, SID_VIRTUAL_ADDRESS, + vaddr_nid, get_segment_start(segment_nid), + "map virtual address to linear address in segment") + +def store_if_in_segment(vaddr_nid, store_nid, segment_nid): + return new_ternary(OP_ITE, get_sid(segment_nid), + is_virtual_address_in_segment(vaddr_nid, segment_nid), + store_nid, + segment_nid, + "store at virtual address if in segment") + +# instructions + +SID_INSTRUCTION_WORD = None + +NID_INSTRUCTION_WORD_SIZE_MASK = None + +# RISC-U codes + +OP_LOAD = 3 # 0000011, I format (LD,LW) +OP_IMM = 19 # 0010011, I format (ADDI, NOP) +OP_STORE = 35 # 0100011, S format (SD,SW) +OP_OP = 51 # 0110011, R format (ADD, SUB, MUL, DIVU, REMU, SLTU) +OP_LUI = 55 # 0110111, U format (LUI) +OP_BRANCH = 99 # 1100011, B format (BEQ) +OP_JALR = 103 # 1100111, I format (JALR) +OP_JAL = 111 # 1101111, J format (JAL) +OP_SYSTEM = 115 # 1110011, I format (ECALL) + +F3_NOP = 0 # 000 +F3_ADDI = 0 # 000 +F3_ADD = 0 # 000 +F3_SUB = 0 # 000 +F3_MUL = 0 # 000 +F3_DIVU = 5 # 101 +F3_REMU = 7 # 111 +F3_SLTU = 3 # 011 +F3_LD = 3 # 011 +F3_SD = 3 # 011 +F3_LW = 2 # 010 +F3_SW = 2 # 010 +F3_BEQ = 0 # 000 +F3_JALR = 0 # 000 +F3_ECALL = 0 # 000 + +F7_ADD = 0 # 0000000 +F7_MUL = 1 # 0000001 +F7_SUB = 32 # 0100000 +F7_DIVU = 1 # 0000001 +F7_REMU = 1 # 0000001 +F7_SLTU = 0 # 0000000 + +F12_ECALL = 0 # 000000000000 + +SID_OPCODE = None + +NID_OP_LOAD = None +NID_OP_IMM = None +NID_OP_STORE = None +NID_OP_OP = None +NID_OP_LUI = None +NID_OP_BRANCH = None +NID_OP_JALR = None +NID_OP_JAL = None +NID_OP_SYSTEM = None + +SID_FUNCT3 = None + +NID_F3_NOP = None +NID_F3_ADDI = None +NID_F3_ADD_SUB_MUL = None +NID_F3_DIVU = None +NID_F3_REMU = None +NID_F3_SLTU = None +NID_F3_LD = None +NID_F3_SD = None +NID_F3_LW = None +NID_F3_SW = None +NID_F3_BEQ = None +NID_F3_JALR = None +NID_F3_ECALL = None + +SID_FUNCT7 = None + +NID_F7_ADD = None +NID_F7_MUL = None +NID_F7_SUB = None +NID_F7_DIVU = None +NID_F7_REMU = None +NID_F7_SLTU = None + +NID_F7_MUL_DIV_REM = None + +SID_FUNCT12 = None + +NID_F12_ECALL = None + +NID_ECALL_I = None + +# immediate sorts + +SID_1_BIT_IMM = None +SID_4_BIT_IMM = None +SID_5_BIT_IMM = None +SID_6_BIT_IMM = None +SID_8_BIT_IMM = None +SID_10_BIT_IMM = None +SID_11_BIT_IMM = None +SID_12_BIT_IMM = None +SID_13_BIT_IMM = None +SID_20_BIT_IMM = None +SID_21_BIT_IMM = None +SID_32_BIT_IMM = None + +NID_1_BIT_IMM_0 = None +NID_12_BIT_IMM_0 = None + +# RISC-U instruction switches + +RISCUONLY = False # restrict modeling to RISC-U only + +SID_INSTRUCTION_ID = None + +NID_DISABLED = None + +NID_LUI = None +NID_ADDI = None + +NID_ADD = None +NID_SUB = None +NID_MUL = None +NID_DIVU = None +NID_REMU = None +NID_SLTU = None + +NID_LD = None +NID_SD = None +NID_LW = None +NID_SW = None + +NID_BEQ = None +NID_JAL = None +NID_JALR = None + +NID_ECALL = None + +# RV32I codes missing in RISC-U + +OP_AUIPC = 23 # 0010111, U format (AUIPC) + +F3_BNE = 1 # 001 +F3_BLT = 4 # 100 +F3_BGE = 5 # 101 +F3_BLTU = 6 # 110 +F3_BGEU = 7 # 111 + +F3_LB = 0 # 000 +F3_LH = 1 # 001 +F3_LBU = 4 # 100 +F3_LHU = 5 # 101 + +F3_SB = 0 # 000 +F3_SH = 1 # 001 + +F3_SLL = 1 # 001 +F3_SLT = 2 # 010 +F3_XOR = 4 # 100 +F3_SRL = 5 # 101 +F3_SRA = 5 # 101 +F3_OR = 6 # 110 +F3_AND = 7 # 111 + +NID_OP_AUIPC = None + +NID_F3_BNE = None +NID_F3_BLT = None +NID_F3_BGE = None +NID_F3_BLTU = None +NID_F3_BGEU = None + +NID_F3_LB = None +NID_F3_LH = None +NID_F3_LBU = None +NID_F3_LHU = None + +NID_F3_SB = None +NID_F3_SH = None + +NID_F3_SLL = None +NID_F3_SLT = None +NID_F3_XOR = None +NID_F3_SRL = None +NID_F3_SRA = None +NID_F3_OR = None +NID_F3_AND = None + +NID_F7_ADD_SLT_XOR_OR_AND_SLL_SRL = None +NID_F7_SUB_SRA = None + +NID_F7_SLL_SRL_ILLEGAL = None +NID_F7_SRA_ILLEGAL = None + +# RV32I instruction switches + +NID_AUIPC = None + +NID_BNE = None +NID_BLT = None +NID_BGE = None +NID_BLTU = None +NID_BGEU = None + +NID_LB = None +NID_LH = None +NID_LBU = None +NID_LHU = None + +NID_SB = None +NID_SH = None + +NID_SLTI = None +NID_SLTIU = None +NID_XORI = None +NID_ORI = None +NID_ANDI = None + +NID_SLLI = None +NID_SRLI = None +NID_SRAI = None + +NID_SLL = None +NID_SLT = None +NID_XOR = None +NID_SRL = None +NID_SRA = None + +NID_OR = None +NID_AND = None + +# RV64I codes missing in RISC-U + +SID_FUNCT6 = None + +F6_SLL_SRL = 0 # 000000 +F6_SRA = 16 # 010000 + +NID_F6_SLL_SRL = None +NID_F6_SRA = None + +OP_IMM_32 = 27 # 0011011, I format +OP_OP_32 = 59 # 0111011, I format + +F3_LWU = 6 # 110 + +NID_OP_IMM_32 = None +NID_OP_OP_32 = None + +NID_F3_LWU = None + +# RV64I instruction switches + +NID_LWU = None + +NID_ADDIW = None +NID_SLLIW = None +NID_SRLIW = None +NID_SRAIW = None + +NID_ADDW = None +NID_SUBW = None +NID_SLLW = None +NID_SRLW = None +NID_SRAW = None + +# RV32M codes missing in RISC-U + +F3_MULH = 1 # 001 +F3_MULHSU = 2 # 010 +F3_MULHU = 3 # 011 +F3_DIV = 4 # 100 +F3_REM = 6 # 110 + +NID_F3_MULH = None +NID_F3_MULHSU = None +NID_F3_MULHU = None +NID_F3_DIV = None +NID_F3_REM = None + +# RV32M instruction switches + +RV32M = True # RV32M support + +NID_MULH = None +NID_MULHSU = None +NID_MULHU = None +NID_DIV = None +NID_REM = None + +# RV64M instruction switches + +RV64M = True # RV64M support + +NID_MULW = None +NID_DIVW = None +NID_DIVUW = None +NID_REMW = None +NID_REMUW = None + +# RVC codes + +SID_OPCODE_C = None + +NID_OP_C0 = None +NID_OP_C1 = None +NID_OP_C2 = None +NID_OP_C3 = None + +F3_C_LI = 2 # 010 +F3_C_LUI_ADDI16SP = 3 # 011 + +NID_F3_C_LI = None +NID_F3_C_LUI_ADDI16SP = None + +F3_C_ADDI = 0 # 000 +F3_C_ADDIW_JAL = 1 # 001 + +NID_F3_C_ADDI = None +NID_F3_C_ADDIW_JAL = None + +F3_C_ADDI4SPN = 0 # 000 + +NID_F3_C_ADDI4SPN = None + +F3_C_SLLI = 0 # 000 +F3_C_SRLI_SRAI_ANDI = 4 # 100 + +NID_F3_C_SLLI = None +NID_F3_C_SRLI_SRAI_ANDI = None + +SID_FUNCT2 = None + +F2_C_SRLI = 0 # 00 +F2_C_SRAI = 1 # 01 +F2_C_ANDI = 2 # 10 + +NID_F2_C_SRLI = None +NID_F2_C_SRAI = None +NID_F2_C_ANDI = None + +F6_C_SUB_XOR_OR_AND = 35 # 100011 +F6_C_ADDW_SUBW = 39 # 100111 + +NID_F6_C_SUB_XOR_OR_AND = None +NID_F6_C_ADDW_SUBW = None + +F2_C_SUB_SUBW = 0 # 00 +F2_C_XOR_ADDW = 1 # 01 +F2_C_OR = 2 # 10 +F2_C_AND = 3 # 11 + +NID_F2_C_SUB_SUBW = None +NID_F2_C_XOR_ADDW = None +NID_F2_C_OR = None +NID_F2_C_AND = None + +F3_C_LWSP_LW = 2 # 010 +F3_C_LDSP_LD = 3 # 011 + +NID_F3_C_LWSP_LW = None +NID_F3_C_LDSP_LD = None + +F3_C_SWSP_SW = 6 # 110 +F3_C_SDSP_SD = 7 # 111 + +NID_F3_C_SWSP_SW = None +NID_F3_C_SDSP_SD = None + +F3_C_BEQZ = 6 # 110 +F3_C_BNEZ = 7 # 111 + +NID_F3_C_BEQZ = None +NID_F3_C_BNEZ = None + +F3_C_J = 5 # 101 + +NID_F3_C_J = None + +SID_FUNCT4 = None + +F4_C_MV_JR = 8 # 1000 +F4_C_ADD_JALR = 9 # 1001 + +NID_F4_C_MV_JR = None +NID_F4_C_ADD_JALR = None + +# offset sorts + +SID_1_BIT_OFFSET = None +SID_2_BIT_OFFSET = None +SID_3_BIT_OFFSET = None +SID_4_BIT_OFFSET = None +SID_5_BIT_OFFSET = None +SID_6_BIT_OFFSET = None +SID_7_BIT_OFFSET = None +SID_8_BIT_OFFSET = None +SID_9_BIT_OFFSET = None +SID_10_BIT_OFFSET = None +SID_11_BIT_OFFSET = None +SID_12_BIT_OFFSET = None +SID_17_BIT_OFFSET = None +SID_18_BIT_OFFSET = None + +NID_1_BIT_OFFSET_0 = None +NID_1_BIT_OFFSET_1 = None +NID_2_BIT_OFFSET_0 = None +NID_2_BIT_OFFSET_1 = None +NID_3_BIT_OFFSET_0 = None +NID_4_BIT_OFFSET_0 = None +NID_12_BIT_OFFSET_0 = None + +SID_COMPRESSED_REGISTER_ADDRESS = None + +# RVC instruction switches + +RVC = True # RVC support + +NID_C_LI = None +NID_C_LUI = None + +NID_C_ADDI = None +NID_C_ADDIW = None +NID_C_ADDI16SP = None + +NID_C_ADDI4SPN = None + +NID_C_ANDI = None + +NID_C_SLLI = None +NID_C_SRLI = None +NID_C_SRAI = None + +NID_C_MV = None +NID_C_ADD = None + +NID_C_SUB = None +NID_C_XOR = None +NID_C_OR = None +NID_C_AND = None + +NID_C_ADDW = None +NID_C_SUBW = None + +NID_C_LWSP = None +NID_C_LW = None + +NID_C_LDSP = None +NID_C_LD = None + +NID_C_SWSP = None +NID_C_SW = None + +NID_C_SDSP = None +NID_C_SD = None + +NID_C_BEQZ = None +NID_C_BNEZ = None + +NID_C_J = None +NID_C_JAL = None + +NID_C_JR = None +NID_C_JALR = None + +# instruction IDs + +ID_UNKNOWN = 0 + +ID_ECALL = 1 + +# R-type + +ID_ADD = 2 +ID_SUB = 3 +ID_SLL = 4 +ID_SLT = 5 +ID_SLTU = 6 +ID_XOR = 7 +ID_SRL = 8 +ID_SRA = 9 +ID_OR = 10 +ID_AND = 11 + +ID_ADDW = 12 +ID_SUBW = 13 +ID_SLLW = 14 +ID_SRLW = 15 +ID_SRAW = 16 + +ID_MUL = 17 +ID_MULH = 18 +ID_MULHSU = 19 +ID_MULHU = 20 +ID_DIV = 21 +ID_DIVU = 22 +ID_REM = 23 +ID_REMU = 24 + +ID_MULW = 25 +ID_DIVW = 26 +ID_DIVUW = 27 +ID_REMW = 28 +ID_REMUW = 29 + +# I-type + +ID_JALR = 30 + +ID_LB = 31 +ID_LH = 32 +ID_LW = 33 +ID_LBU = 34 +ID_LHU = 35 +ID_LWU = 36 +ID_LD = 37 + +ID_ADDI = 38 +ID_SLTI = 39 +ID_SLTIU = 40 +ID_XORI = 41 +ID_ORI = 42 +ID_ANDI = 43 + +ID_ADDIW = 44 + +ID_SLLI = 45 +ID_SRLI = 46 +ID_SRAI = 47 + +ID_SLLIW = 48 +ID_SRLIW = 49 +ID_SRAIW = 50 + +# S-type + +ID_SB = 51 +ID_SH = 52 +ID_SW = 53 +ID_SD = 54 + +# SB-type + +ID_BEQ = 55 +ID_BNE = 56 +ID_BLT = 57 +ID_BGE = 58 +ID_BLTU = 59 +ID_BGEU = 60 + +# U-type + +ID_LUI = 61 +ID_AUIPC = 62 + +# UJ-type + +ID_JAL = 63 + +# compressed instruction IDs + +# CR-type + +ID_C_MV = 64 +ID_C_ADD = 65 + +ID_C_JR = 66 +ID_C_JALR = 67 + +# CI-type + +ID_C_LI = 68 +ID_C_LUI = 69 + +ID_C_ADDI = 70 +ID_C_ADDIW = 71 +ID_C_ADDI16SP = 72 + +# CIW-type + +ID_C_ADDI4SPN = 73 + +# CI-type + +ID_C_SLLI = 74 + +ID_C_LWSP = 75 +ID_C_LDSP = 76 + +# CL-type + +ID_C_LW = 77 +ID_C_LD = 78 + +# CS-type + +ID_C_SW = 79 +ID_C_SD = 80 + +ID_C_SUB = 81 +ID_C_XOR = 82 +ID_C_OR = 83 +ID_C_AND = 84 + +ID_C_ADDW = 85 +ID_C_SUBW = 86 + +# CSS-type + +ID_C_SWSP = 87 +ID_C_SDSP = 88 + +# CB-type + +ID_C_BEQZ = 89 +ID_C_BNEZ = 90 + +ID_C_ANDI = 91 + +ID_C_SRLI = 92 +ID_C_SRAI = 93 + +# CJ-type + +ID_C_J = 94 +ID_C_JAL = 95 + +# pseudoinstruction IDs + +# No operands + +ID_P_NOP = 96 +ID_P_RET = 97 + +# rd,I_imm + +ID_P_LI = 98 + +# rd,rsx + +ID_P_MV = 99 # rs1 or rs2 +ID_P_NOT = 100 # rs1 +ID_P_SEXT_W = 101 # rs1 +ID_P_SEQZ = 102 # rs1 +ID_P_SLTZ = 103 # rs1 +ID_P_ZEXT_B = 104 # rs1 +ID_P_NEG = 105 # rs2 +ID_P_NEGW = 106 # rs2 +ID_P_SNEZ = 107 # rs2 +ID_P_SGTZ = 108 # rs2 + +# branch type (rsx,pc+SB_imm ) + +ID_P_BEQZ = 109 # rs1 +ID_P_BNEZ = 110 # rs1 +ID_P_BGEZ = 111 # rs1 +ID_P_BLTZ = 112 # rs1 +ID_P_BLEZ = 113 # rs2 +ID_P_BGTZ = 114 # rs2 + +# jump type (pc + UJ_imm ) + +ID_P_J = 115 +ID_P_JAL = 116 + +# jump register type (immx(rs1)) + +ID_P_JR = 117 # I_imm or 0 +ID_P_JALR = 118 # I_imm or 0 + +RISC_V_MNEMONICS = { + ID_UNKNOWN: "unknown RISC-V instruction", + + ID_ECALL: 'ecall', + + # R-type + + ID_ADD: 'add', + ID_SUB: 'sub', + ID_SLL: 'sll', + ID_SLT: 'slt', + ID_SLTU: 'sltu', + ID_XOR: 'xor', + ID_SRL: 'srl', + ID_SRA: 'sra', + ID_OR: 'or', + ID_AND: 'and', + + ID_ADDW: 'addw', + ID_SUBW: 'subw', + ID_SLLW: 'sllw', + ID_SRLW: 'srlw', + ID_SRAW: 'sraw', + + ID_MUL: 'mul', + ID_MULH: 'mulh', + ID_MULHSU: 'mulhsu', + ID_MULHU: 'mulhu', + ID_DIV: 'div', + ID_DIVU: 'divu', + ID_REM: 'rem', + ID_REMU: 'remu', + + ID_MULW: 'mulw', + ID_DIVW: 'divw', + ID_DIVUW: 'divuw', + ID_REMW: 'remw', + ID_REMUW: 'remuw', + + # I-type + + ID_JALR: 'jalr', + + ID_LB: 'lb', + ID_LH: 'lh', + ID_LW: 'lw', + ID_LBU: 'lbu', + ID_LHU: 'lhu', + ID_LWU: 'lwu', + ID_LD: 'ld', + + ID_ADDI: 'addi', + ID_SLTI: 'slti', + ID_SLTIU: 'sltiu', + ID_XORI: 'xori', + ID_ORI: 'ori', + ID_ANDI: 'andi', + + ID_ADDIW: 'addiw', + + ID_SLLI: 'slli', + ID_SRLI: 'srli', + ID_SRAI: 'srai', + + ID_SLLIW: 'slliw', + ID_SRLIW: 'srliw', + ID_SRAIW: 'sraiw', + + # S-type + + ID_SB: 'sb', + ID_SH: 'sh', + ID_SW: 'sw', + ID_SD: 'sd', + + # SB-type + + ID_BEQ: 'beq', + ID_BNE: 'bne', + ID_BLT: 'blt', + ID_BGE: 'bge', + ID_BLTU: 'bltu', + ID_BGEU: 'bgeu', + + # U-type + + ID_LUI: 'lui', + ID_AUIPC: 'auipc', + + # UJ-type + + ID_JAL: 'jal', + + # compressed instruction IDs + + # CR-type + + ID_C_MV: 'c.mv', + ID_C_ADD: 'c.add', + + ID_C_JR: 'c.jr', + ID_C_JALR: 'c.jalr', + + # CI-type + + ID_C_LI: 'c.li', + ID_C_LUI: 'c.lui', + + ID_C_ADDI: 'c.addi', + ID_C_ADDIW: 'c.addiw', + ID_C_ADDI16SP: 'c.addi16sp', + + # CIW-type + + ID_C_ADDI4SPN: 'c.addi4spn', + + # CI-type + + ID_C_SLLI: 'c.slli', + + ID_C_LWSP: 'c.lwsp', + ID_C_LDSP: 'c.ldsp', + + # CL-type + + ID_C_LW: 'c.lw', + ID_C_LD: 'c.ld', + + # CS-type + + ID_C_SW: 'c.sw', + ID_C_SD: 'c.sd', + + ID_C_SUB: 'c.sub', + ID_C_XOR: 'c.xor', + ID_C_OR: 'c.or', + ID_C_AND: 'c.and', + + ID_C_ADDW: 'c.addw', + ID_C_SUBW: 'c.subw', + + # CSS-type + + ID_C_SWSP: 'c.swsp', + ID_C_SDSP: 'c.sdsp', + + # CB-type + + ID_C_BEQZ: 'c.beqz', + ID_C_BNEZ: 'c.bnez', + + ID_C_ANDI: 'c.andi', + + ID_C_SRLI: 'c.srli', + ID_C_SRAI: 'c.srai', + + # CJ-type + + ID_C_J: 'c.j', + ID_C_JAL: 'c.jal', + + # pseudoinstruction IDs + + # No operands + + ID_P_NOP: 'nop', + ID_P_RET: 'ret', + + # rd,I_imm + + ID_P_LI: 'li', + + # rd,rsx + + ID_P_MV: 'mv', + ID_P_NOT: 'not', + ID_P_SEXT_W: 'sext.w', + ID_P_SEQZ: 'seqz', + ID_P_SLTZ: 'sltz', + ID_P_ZEXT_B: 'zext.b', + ID_P_NEG: 'neg', + ID_P_NEGW: 'negw', + ID_P_SNEZ: 'snez', + ID_P_SGTZ: 'sgtz', + + # branch type (rsx,pc+SB_imm ) + + ID_P_BEQZ: 'beqz', + ID_P_BNEZ: 'bnez', + ID_P_BGEZ: 'bgez', + ID_P_BLTZ: 'bltz', + ID_P_BLEZ: 'blez', + ID_P_BGTZ: 'bgtz', + + # jump type (pc + UJ_imm ) + + ID_P_J: 'j', + ID_P_JAL: 'jal', + + # jump register type (immx(rs1)) + + ID_P_JR: 'jr', + ID_P_JALR: 'jalr' +} + +def init_instruction_sorts(): + global SID_INSTRUCTION_WORD + + global NID_INSTRUCTION_WORD_SIZE_MASK + + global SID_OPCODE + + global NID_OP_LOAD + global NID_OP_IMM + global NID_OP_STORE + global NID_OP_OP + global NID_OP_LUI + global NID_OP_BRANCH + global NID_OP_JALR + global NID_OP_JAL + global NID_OP_SYSTEM + + global SID_FUNCT3 + + global NID_F3_NOP + global NID_F3_ADDI + global NID_F3_ADD_SUB_MUL + global NID_F3_DIVU + global NID_F3_REMU + global NID_F3_SLTU + global NID_F3_LD + global NID_F3_SD + global NID_F3_LW + global NID_F3_SW + global NID_F3_BEQ + global NID_F3_JALR + global NID_F3_ECALL + + global SID_FUNCT7 + + global NID_F7_ADD + global NID_F7_MUL + global NID_F7_SUB + global NID_F7_DIVU + global NID_F7_REMU + global NID_F7_SLTU + + global NID_F7_MUL_DIV_REM + + global SID_FUNCT12 + + global NID_F12_ECALL + + global NID_ECALL_I + + global SID_1_BIT_IMM + global SID_4_BIT_IMM + global SID_5_BIT_IMM + global SID_6_BIT_IMM + global SID_8_BIT_IMM + global SID_10_BIT_IMM + global SID_11_BIT_IMM + global SID_12_BIT_IMM + global SID_13_BIT_IMM + global SID_20_BIT_IMM + global SID_21_BIT_IMM + global SID_32_BIT_IMM + + global NID_1_BIT_IMM_0 + global NID_12_BIT_IMM_0 + + global SID_INSTRUCTION_ID + + global NID_DISABLED + + global NID_LUI + global NID_ADDI + + global NID_ADD + global NID_SUB + global NID_MUL + global NID_DIVU + global NID_REMU + global NID_SLTU + + global NID_LD + global NID_SD + global NID_LW + global NID_SW + + global NID_BEQ + global NID_JAL + global NID_JALR + + global NID_ECALL + + global NID_OP_AUIPC + + global NID_F3_BNE + global NID_F3_BLT + global NID_F3_BGE + global NID_F3_BLTU + global NID_F3_BGEU + + global NID_F3_LB + global NID_F3_LH + global NID_F3_LBU + global NID_F3_LHU + + global NID_F3_SB + global NID_F3_SH + + global NID_F3_SLL + global NID_F3_SLT + global NID_F3_XOR + global NID_F3_SRL + global NID_F3_SRA + global NID_F3_OR + global NID_F3_AND + + global NID_F7_ADD_SLT_XOR_OR_AND_SLL_SRL + global NID_F7_SUB_SRA + + global NID_F7_SLL_SRL_ILLEGAL + global NID_F7_SRA_ILLEGAL + + global NID_AUIPC + + global NID_BNE + global NID_BLT + global NID_BGE + global NID_BLTU + global NID_BGEU + + global NID_LB + global NID_LH + global NID_LBU + global NID_LHU + + global NID_SB + global NID_SH + + global NID_SLTI + global NID_SLTIU + global NID_XORI + global NID_ORI + global NID_ANDI + + global NID_SLLI + global NID_SRLI + global NID_SRAI + + global NID_SLL + global NID_SLT + global NID_XOR + global NID_SRL + global NID_SRA + + global NID_OR + global NID_AND + + global SID_FUNCT6 + + global NID_F6_SLL_SRL + global NID_F6_SRA + + global NID_OP_IMM_32 + global NID_OP_OP_32 + + global NID_F3_LWU + + global NID_LWU + + global NID_ADDIW + global NID_SLLIW + global NID_SRLIW + global NID_SRAIW + + global NID_ADDW + global NID_SUBW + global NID_SLLW + global NID_SRLW + global NID_SRAW + + global NID_F3_MULH + global NID_F3_MULHSU + global NID_F3_MULHU + global NID_F3_DIV + global NID_F3_REM + + global RV32M + + global NID_MULH + global NID_MULHSU + global NID_MULHU + global NID_DIV + global NID_REM + + global RV64M + + global NID_MULW + global NID_DIVW + global NID_DIVUW + global NID_REMW + global NID_REMUW + + SID_INSTRUCTION_WORD = SID_SINGLE_WORD; + + if (RVC): + NID_INSTRUCTION_WORD_SIZE_MASK = NID_MACHINE_WORD_1 + else: + NID_INSTRUCTION_WORD_SIZE_MASK = NID_MACHINE_WORD_3 + + SID_OPCODE = new_bitvec(7, "opcode sort"); + + NID_OP_LOAD = new_constant(OP_CONST, SID_OPCODE, OP_LOAD, "OP_LOAD") + NID_OP_IMM = new_constant(OP_CONST, SID_OPCODE, OP_IMM, "OP_IMM") + NID_OP_STORE = new_constant(OP_CONST, SID_OPCODE, OP_STORE, "OP_STORE") + NID_OP_OP = new_constant(OP_CONST, SID_OPCODE, OP_OP, "OP_OP") + NID_OP_LUI = new_constant(OP_CONST, SID_OPCODE, OP_LUI, "OP_LUI") + NID_OP_BRANCH = new_constant(OP_CONST, SID_OPCODE, OP_BRANCH, "OP_BRANCH") + NID_OP_JALR = new_constant(OP_CONST, SID_OPCODE, OP_JALR, "OP_JALR") + NID_OP_JAL = new_constant(OP_CONST, SID_OPCODE, OP_JAL, "OP_JAL") + NID_OP_SYSTEM = new_constant(OP_CONST, SID_OPCODE, OP_SYSTEM, "OP_SYSTEM") + + SID_FUNCT3 = new_bitvec(3, "funct3 sort") + + NID_F3_NOP = new_constant(OP_CONST, SID_FUNCT3, F3_NOP, "F3_NOP") + NID_F3_ADDI = new_constant(OP_CONST, SID_FUNCT3, F3_ADDI, "F3_ADDI") + NID_F3_ADD_SUB_MUL = new_constant(OP_CONST, SID_FUNCT3, F3_ADD, "F3_ADD_SUB_MUL") + NID_F3_DIVU = new_constant(OP_CONST, SID_FUNCT3, F3_DIVU, "F3_DIVU") + NID_F3_REMU = new_constant(OP_CONST, SID_FUNCT3, F3_REMU, "F3_REMU") + NID_F3_SLTU = new_constant(OP_CONST, SID_FUNCT3, F3_SLTU, "F3_SLTU") + NID_F3_LD = new_constant(OP_CONST, SID_FUNCT3, F3_LD, "F3_LD") + NID_F3_SD = new_constant(OP_CONST, SID_FUNCT3, F3_SD, "F3_SD") + NID_F3_LW = new_constant(OP_CONST, SID_FUNCT3, F3_LW, "F3_LW") + NID_F3_SW = new_constant(OP_CONST, SID_FUNCT3, F3_SW, "F3_SW") + NID_F3_BEQ = new_constant(OP_CONST, SID_FUNCT3, F3_BEQ, "F3_BEQ") + NID_F3_JALR = new_constant(OP_CONST, SID_FUNCT3, F3_JALR, "F3_JALR") + NID_F3_ECALL = new_constant(OP_CONST, SID_FUNCT3, F3_ECALL, "F3_ECALL") + + SID_FUNCT7 = new_bitvec(7, "funct7 sort") + + NID_F7_ADD = new_constant(OP_CONST, SID_FUNCT7, F7_ADD, "F7_ADD") + NID_F7_MUL = new_constant(OP_CONST, SID_FUNCT7, F7_MUL, "F7_MUL") + NID_F7_SUB = new_constant(OP_CONST, SID_FUNCT7, F7_SUB, "F7_SUB") + NID_F7_DIVU = new_constant(OP_CONST, SID_FUNCT7, F7_DIVU, "F7_DIVU") + NID_F7_REMU = new_constant(OP_CONST, SID_FUNCT7, F7_REMU, "F7_REMU") + NID_F7_SLTU = new_constant(OP_CONST, SID_FUNCT7, F7_SLTU, "F7_SLTU") + + NID_F7_MUL_DIV_REM = NID_F7_MUL + + SID_FUNCT12 = new_bitvec(12, "funct12 sort") + + NID_F12_ECALL = new_constant(OP_CONST, SID_FUNCT12, F12_ECALL, "F12_ECALL") + + NID_ECALL_I = new_constant(OP_CONST, SID_INSTRUCTION_WORD, + (((((((F12_ECALL << 5) + REG_ZR) << 3) + F3_ECALL) << 5) + REG_ZR) << 7) + OP_SYSTEM, + "ECALL instruction"); + + # immediate sorts + + SID_1_BIT_IMM = new_bitvec(1, "1-bit immediate sort") + SID_4_BIT_IMM = new_bitvec(4, "4-bit immediate sort") + SID_5_BIT_IMM = new_bitvec(5, "5-bit immediate sort") + SID_6_BIT_IMM = new_bitvec(6, "6-bit immediate sort") + SID_8_BIT_IMM = new_bitvec(8, "8-bit immediate sort") + SID_10_BIT_IMM = new_bitvec(10, "10-bit immediate sort") + SID_11_BIT_IMM = new_bitvec(11, "11-bit immediate sort") + SID_12_BIT_IMM = new_bitvec(12, "12-bit immediate sort") + SID_13_BIT_IMM = new_bitvec(13, "13-bit immediate sort") + SID_20_BIT_IMM = new_bitvec(20, "20-bit immediate sort") + SID_21_BIT_IMM = new_bitvec(21, "21-bit immediate sort") + SID_32_BIT_IMM = new_bitvec(32, "32-bit immediate sort") + + NID_1_BIT_IMM_0 = new_constant(OP_CONST, SID_1_BIT_IMM, 0, "zeroed bit") + NID_12_BIT_IMM_0 = new_constant(OP_CONST, SID_12_BIT_IMM, 0, "12 LSBs zeroed") + + # RISC-U instructions + + SID_INSTRUCTION_ID = new_bitvec(7, "7-bit instruction ID") + + NID_DISABLED = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_UNKNOWN, RISC_V_MNEMONICS[ID_UNKNOWN]) + + NID_LUI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LUI, RISC_V_MNEMONICS[ID_LUI]) + NID_ADDI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ADDI, RISC_V_MNEMONICS[ID_ADDI]) + + NID_ADD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ADD, RISC_V_MNEMONICS[ID_ADD]) + NID_SUB = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SUB, RISC_V_MNEMONICS[ID_SUB]) + NID_MUL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_MUL, RISC_V_MNEMONICS[ID_MUL]) + NID_DIVU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_DIVU, RISC_V_MNEMONICS[ID_DIVU]) + NID_REMU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_REMU, RISC_V_MNEMONICS[ID_REMU]) + NID_SLTU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLTU, RISC_V_MNEMONICS[ID_SLTU]) + + NID_LW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LW, RISC_V_MNEMONICS[ID_LW]) + NID_SW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SW, RISC_V_MNEMONICS[ID_SW]) + NID_LD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LD, RISC_V_MNEMONICS[ID_LD]) + NID_SD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SD, RISC_V_MNEMONICS[ID_SD]) + + NID_BEQ = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BEQ, RISC_V_MNEMONICS[ID_BEQ]) + NID_JAL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_JAL, RISC_V_MNEMONICS[ID_JAL]) + NID_JALR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_JALR, RISC_V_MNEMONICS[ID_JALR]) + + NID_ECALL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ECALL, RISC_V_MNEMONICS[ID_ECALL]) + + if IS64BITTARGET: + if RISCUONLY: + NID_LW = NID_DISABLED + NID_SW = NID_DISABLED + else: + NID_LD = NID_DISABLED + NID_SD = NID_DISABLED + + # RV32I codes missing in RISC-U + + NID_OP_AUIPC = new_constant(OP_CONST, SID_OPCODE, OP_AUIPC, "OP_AUIPC") + + NID_F3_BNE = new_constant(OP_CONST, SID_FUNCT3, F3_BNE, "F3_BNE") + NID_F3_BLT = new_constant(OP_CONST, SID_FUNCT3, F3_BLT, "F3_BLT") + NID_F3_BGE = new_constant(OP_CONST, SID_FUNCT3, F3_BGE, "F3_BGE") + NID_F3_BLTU = new_constant(OP_CONST, SID_FUNCT3, F3_BLTU, "F3_BLTU") + NID_F3_BGEU = new_constant(OP_CONST, SID_FUNCT3, F3_BGEU, "F3_BGEU") + + NID_F3_LB = new_constant(OP_CONST, SID_FUNCT3, F3_LB, "F3_LB") + NID_F3_LH = new_constant(OP_CONST, SID_FUNCT3, F3_LH, "F3_LH") + NID_F3_LBU = new_constant(OP_CONST, SID_FUNCT3, F3_LBU, "F3_LBU") + NID_F3_LHU = new_constant(OP_CONST, SID_FUNCT3, F3_LHU, "F3_LHU") + + NID_F3_SB = new_constant(OP_CONST, SID_FUNCT3, F3_SB, "F3_SB") + NID_F3_SH = new_constant(OP_CONST, SID_FUNCT3, F3_SH, "F3_SH") + + NID_F3_SLL = new_constant(OP_CONST, SID_FUNCT3, F3_SLL, "F3_SLL") + NID_F3_SLT = new_constant(OP_CONST, SID_FUNCT3, F3_SLT, "F3_SLT") + NID_F3_XOR = new_constant(OP_CONST, SID_FUNCT3, F3_XOR, "F3_XOR") + NID_F3_SRL = new_constant(OP_CONST, SID_FUNCT3, F3_SRL, "F3_SRL") + NID_F3_SRA = new_constant(OP_CONST, SID_FUNCT3, F3_SRA, "F3_SRA") + NID_F3_OR = new_constant(OP_CONST, SID_FUNCT3, F3_OR, "F3_OR") + NID_F3_AND = new_constant(OP_CONST, SID_FUNCT3, F3_AND, "F3_AND") + + NID_F7_ADD_SLT_XOR_OR_AND_SLL_SRL = NID_F7_ADD + NID_F7_SUB_SRA = NID_F7_SUB + + NID_F7_SLL_SRL_ILLEGAL = new_constant(OP_CONST, SID_FUNCT7, F7_ADD + 1, "F7_SLL_SRL_ILLEGAL") + NID_F7_SRA_ILLEGAL = new_constant(OP_CONST, SID_FUNCT7, F7_SUB + 1, "F7_SRA_ILLEGAL") + + # RV32I instruction switches + + if RISCUONLY: + NID_AUIPC = NID_DISABLED + + NID_BNE = NID_DISABLED + NID_BLT = NID_DISABLED + NID_BGE = NID_DISABLED + NID_BLTU = NID_DISABLED + NID_BGEU = NID_DISABLED + + NID_LB = NID_DISABLED + NID_LH = NID_DISABLED + NID_LBU = NID_DISABLED + NID_LHU = NID_DISABLED + + NID_SB = NID_DISABLED + NID_SH = NID_DISABLED + + NID_SLTI = NID_DISABLED + NID_SLTIU = NID_DISABLED + NID_XORI = NID_DISABLED + NID_ORI = NID_DISABLED + NID_ANDI = NID_DISABLED + + NID_SLLI = NID_DISABLED + NID_SRLI = NID_DISABLED + NID_SRAI = NID_DISABLED + + NID_SLL = NID_DISABLED + NID_SLT = NID_DISABLED + NID_XOR = NID_DISABLED + NID_SRL = NID_DISABLED + NID_SRA = NID_DISABLED + + NID_OR = NID_DISABLED + NID_AND = NID_DISABLED; + else: + NID_AUIPC = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_AUIPC, RISC_V_MNEMONICS[ID_AUIPC]) + + NID_BNE = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BNE, RISC_V_MNEMONICS[ID_BNE]) + NID_BLT = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BLT, RISC_V_MNEMONICS[ID_BLT]) + NID_BGE = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BGE, RISC_V_MNEMONICS[ID_BGE]) + NID_BLTU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BLTU, RISC_V_MNEMONICS[ID_BLTU]) + NID_BGEU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_BGEU, RISC_V_MNEMONICS[ID_BGEU]) + + NID_LB = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LB, RISC_V_MNEMONICS[ID_LB]) + NID_LH = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LH, RISC_V_MNEMONICS[ID_LH]) + NID_LBU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LBU, RISC_V_MNEMONICS[ID_LBU]) + NID_LHU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LHU, RISC_V_MNEMONICS[ID_LHU]) + + NID_SB = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SB, RISC_V_MNEMONICS[ID_SB]) + NID_SH = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SH, RISC_V_MNEMONICS[ID_SH]) + + NID_SLTI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLTI, RISC_V_MNEMONICS[ID_SLTI]) + NID_SLTIU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLTIU, RISC_V_MNEMONICS[ID_SLTIU]) + NID_XORI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_XORI, RISC_V_MNEMONICS[ID_XORI]) + NID_ORI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ORI, RISC_V_MNEMONICS[ID_ORI]) + NID_ANDI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ANDI, RISC_V_MNEMONICS[ID_ANDI]) + + NID_SLLI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLLI, RISC_V_MNEMONICS[ID_SLLI]) + NID_SRLI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRLI, RISC_V_MNEMONICS[ID_SRLI]) + NID_SRAI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRAI, RISC_V_MNEMONICS[ID_SRAI]) + + NID_SLL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLL, RISC_V_MNEMONICS[ID_SLL]) + NID_SLT = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLT, RISC_V_MNEMONICS[ID_SLT]) + NID_XOR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_XOR, RISC_V_MNEMONICS[ID_XOR]) + NID_SRL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRL, RISC_V_MNEMONICS[ID_SRL]) + NID_SRA = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRA, RISC_V_MNEMONICS[ID_SRA]) + + NID_OR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_OR, RISC_V_MNEMONICS[ID_OR]) + NID_AND = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_AND, RISC_V_MNEMONICS[ID_AND]) + + # RV64I codes missing in RISC-U + + SID_FUNCT6 = new_bitvec(6, "funct6 sort") + + NID_F6_SLL_SRL = new_constant(OP_CONST, SID_FUNCT6, F6_SLL_SRL, "F6_SLL_SRL") + NID_F6_SRA = new_constant(OP_CONST, SID_FUNCT6, F6_SRA, "F6_SRA") + + NID_OP_IMM_32 = new_constant(OP_CONST, SID_OPCODE, OP_IMM_32, "OP_IMM_32") + NID_OP_OP_32 = new_constant(OP_CONST, SID_OPCODE, OP_OP_32, "OP_OP_32") + + NID_F3_LWU = new_constant(OP_CONST, SID_FUNCT3, F3_LWU, "F3_LWU") + + # RV64I instruction switches + + NID_LWU = NID_DISABLED + + NID_ADDIW = NID_DISABLED + NID_SLLIW = NID_DISABLED + NID_SRLIW = NID_DISABLED + NID_SRAIW = NID_DISABLED + + NID_ADDW = NID_DISABLED + NID_SUBW = NID_DISABLED + NID_SLLW = NID_DISABLED + NID_SRLW = NID_DISABLED + NID_SRAW = NID_DISABLED + + if not RISCUONLY: + if IS64BITTARGET: + NID_LWU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LWU, RISC_V_MNEMONICS[ID_LWU]) + + NID_ADDIW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ADDIW, RISC_V_MNEMONICS[ID_ADDIW]) + NID_SLLIW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLLIW, RISC_V_MNEMONICS[ID_SLLIW]) + NID_SRLIW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRLIW, RISC_V_MNEMONICS[ID_SRLIW]) + NID_SRAIW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRAIW, RISC_V_MNEMONICS[ID_SRAIW]) + + NID_ADDW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ADDW, RISC_V_MNEMONICS[ID_ADDW]) + NID_SUBW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SUBW, RISC_V_MNEMONICS[ID_SUBW]) + NID_SLLW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SLLW, RISC_V_MNEMONICS[ID_SLLW]) + NID_SRLW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRLW, RISC_V_MNEMONICS[ID_SRLW]) + NID_SRAW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SRAW, RISC_V_MNEMONICS[ID_SRAW]) + + # RV32M codes missing in RISC-U + + NID_F3_MULH = new_constant(OP_CONST, SID_FUNCT3, F3_MULH, "F3_MULH") + NID_F3_MULHSU = new_constant(OP_CONST, SID_FUNCT3, F3_MULHSU, "F3_MULHSU") + NID_F3_MULHU = new_constant(OP_CONST, SID_FUNCT3, F3_MULHU, "F3_MULHU") + NID_F3_DIV = new_constant(OP_CONST, SID_FUNCT3, F3_DIV, "F3_DIV") + NID_F3_REM = new_constant(OP_CONST, SID_FUNCT3, F3_REM, "F3_REM") + + # RV32M instruction switches + + if RISCUONLY: + RV32M = True + + NID_MULH = NID_DISABLED + NID_MULHSU = NID_DISABLED + NID_MULHU = NID_DISABLED + NID_DIV = NID_DISABLED + NID_REM = NID_DISABLED + + if not RISCUONLY: + if RV32M: + # MUL, DIVU, REMU already defined + NID_MULH = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_MULH, RISC_V_MNEMONICS[ID_MULH]) + NID_MULHSU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_MULHSU, RISC_V_MNEMONICS[ID_MULHSU]) + NID_MULHU = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_MULHU, RISC_V_MNEMONICS[ID_MULHU]) + NID_DIV = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_DIV, RISC_V_MNEMONICS[ID_DIV]) + NID_REM = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_REM, RISC_V_MNEMONICS[ID_REM]) + else: + NID_MUL = NID_DISABLED + NID_DIVU = NID_DISABLED + NID_REMU = NID_DISABLED + + # RV64M instruction switches + + if RISCUONLY: + RV64M = False + + if not IS64BITTARGET: + RV64M = False + + if RV64M: + NID_MULW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_MULW, RISC_V_MNEMONICS[ID_MULW]) + NID_DIVW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_DIVW, RISC_V_MNEMONICS[ID_DIVW]) + NID_DIVUW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_DIVUW, RISC_V_MNEMONICS[ID_DIVUW]) + NID_REMW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_REMW, RISC_V_MNEMONICS[ID_REMW]) + NID_REMUW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_REMUW, RISC_V_MNEMONICS[ID_REMUW]) + else: + NID_MULW = NID_DISABLED + NID_DIVW = NID_DISABLED + NID_DIVUW = NID_DISABLED + NID_REMW = NID_DISABLED + NID_REMUW = NID_DISABLED + +def init_compressed_instruction_sorts(): + global SID_OPCODE_C + + global NID_OP_C0 + global NID_OP_C1 + global NID_OP_C2 + global NID_OP_C3 + + global NID_F3_C_LI + global NID_F3_C_LUI_ADDI16SP + + global NID_F3_C_ADDI + global NID_F3_C_ADDIW_JAL + + global NID_F3_C_ADDI4SPN + + global NID_F3_C_SLLI + global NID_F3_C_SRLI_SRAI_ANDI + + global SID_FUNCT2 + + global NID_F2_C_SRLI + global NID_F2_C_SRAI + global NID_F2_C_ANDI + + global NID_F6_C_SUB_XOR_OR_AND + global NID_F6_C_ADDW_SUBW + + global NID_F2_C_SUB_SUBW + global NID_F2_C_XOR_ADDW + global NID_F2_C_OR + global NID_F2_C_AND + + global NID_F3_C_LWSP_LW + global NID_F3_C_LDSP_LD + + global NID_F3_C_SWSP_SW + global NID_F3_C_SDSP_SD + + global NID_F3_C_BEQZ + global NID_F3_C_BNEZ + + global NID_F3_C_J + + global SID_FUNCT4 + + global NID_F4_C_MV_JR + global NID_F4_C_ADD_JALR + + global SID_1_BIT_OFFSET + global SID_2_BIT_OFFSET + global SID_3_BIT_OFFSET + global SID_4_BIT_OFFSET + global SID_5_BIT_OFFSET + global SID_6_BIT_OFFSET + global SID_7_BIT_OFFSET + global SID_8_BIT_OFFSET + global SID_9_BIT_OFFSET + global SID_10_BIT_OFFSET + global SID_11_BIT_OFFSET + global SID_12_BIT_OFFSET + global SID_17_BIT_OFFSET + global SID_18_BIT_OFFSET + + global NID_1_BIT_OFFSET_0 + global NID_1_BIT_OFFSET_1 + global NID_2_BIT_OFFSET_0 + global NID_2_BIT_OFFSET_1 + global NID_3_BIT_OFFSET_0 + global NID_4_BIT_OFFSET_0 + global NID_12_BIT_OFFSET_0 + + global SID_COMPRESSED_REGISTER_ADDRESS + + global RVC + + global NID_C_LI + global NID_C_LUI + + global NID_C_ADDI + global NID_C_ADDIW + global NID_C_ADDI16SP + + global NID_C_ADDI4SPN + + global NID_C_ANDI + + global NID_C_SLLI + global NID_C_SRLI + global NID_C_SRAI + + global NID_C_MV + global NID_C_ADD + + global NID_C_SUB + global NID_C_XOR + global NID_C_OR + global NID_C_AND + + global NID_C_ADDW + global NID_C_SUBW + + global NID_C_LWSP + global NID_C_LW + + global NID_C_LDSP + global NID_C_LD + + global NID_C_SWSP + global NID_C_SW + + global NID_C_SDSP + global NID_C_SD + + global NID_C_BEQZ + global NID_C_BNEZ + + global NID_C_J + global NID_C_JAL + + global NID_C_JR + global NID_C_JALR + + # RVC codes + + SID_OPCODE_C = new_bitvec(2, "compressed opcode sort") + + NID_OP_C0 = new_constant(OP_CONST, SID_OPCODE_C, 0, "OP_C0") + NID_OP_C1 = new_constant(OP_CONST, SID_OPCODE_C, 1, "OP_C1") + NID_OP_C2 = new_constant(OP_CONST, SID_OPCODE_C, 2, "OP_C2") + NID_OP_C3 = new_constant(OP_CONST, SID_OPCODE_C, 3, "OP_C3") + + NID_F3_C_LI = new_constant(OP_CONST, SID_FUNCT3, F3_C_LI, "F3_C_LI") + NID_F3_C_LUI_ADDI16SP = new_constant(OP_CONST, SID_FUNCT3, F3_C_LUI_ADDI16SP, "F3_C_LUI_ADDI16SP") + + NID_F3_C_ADDI = new_constant(OP_CONST, SID_FUNCT3, F3_C_ADDI, "F3_C_ADDI") + NID_F3_C_ADDIW_JAL = new_constant(OP_CONST, SID_FUNCT3, F3_C_ADDIW_JAL, "F3_C_ADDIW_JAL") + + NID_F3_C_ADDI4SPN = new_constant(OP_CONST, SID_FUNCT3, F3_C_ADDI4SPN, "F3_C_ADDI4SPN") + + NID_F3_C_SLLI = new_constant(OP_CONST, SID_FUNCT3, F3_C_SLLI, "F3_C_SLLI") + NID_F3_C_SRLI_SRAI_ANDI = new_constant(OP_CONST, SID_FUNCT3, F3_C_SRLI_SRAI_ANDI, "F3_C_SRLI_SRAI_ANDI") + + SID_FUNCT2 = new_bitvec(2, "compressed funct2 sort") + + NID_F2_C_SRLI = new_constant(OP_CONST, SID_FUNCT2, F2_C_SRLI, "F2_C_SRLI") + NID_F2_C_SRAI = new_constant(OP_CONST, SID_FUNCT2, F2_C_SRAI, "F2_C_SRAI") + NID_F2_C_ANDI = new_constant(OP_CONST, SID_FUNCT2, F2_C_ANDI, "F2_C_ANDI") + + NID_F6_C_SUB_XOR_OR_AND = new_constant(OP_CONST, SID_FUNCT6, F6_C_SUB_XOR_OR_AND, "F6_C_SUB_XOR_OR_AND") + NID_F6_C_ADDW_SUBW = new_constant(OP_CONST, SID_FUNCT6, F6_C_ADDW_SUBW, "F6_C_ADDW_SUBW") + + NID_F2_C_SUB_SUBW = new_constant(OP_CONST, SID_FUNCT2, F2_C_SUB_SUBW, "F2_C_SUB_SUBW") + NID_F2_C_XOR_ADDW = new_constant(OP_CONST, SID_FUNCT2, F2_C_XOR_ADDW, "F2_C_XOR_ADDW") + NID_F2_C_OR = new_constant(OP_CONST, SID_FUNCT2, F2_C_OR, "F2_C_OR") + NID_F2_C_AND = new_constant(OP_CONST, SID_FUNCT2, F2_C_AND, "F2_C_AND") + + NID_F3_C_LWSP_LW = new_constant(OP_CONST, SID_FUNCT3, F3_C_LWSP_LW, "F3_C_LWSP_LW") + NID_F3_C_LDSP_LD = new_constant(OP_CONST, SID_FUNCT3, F3_C_LDSP_LD, "F3_C_LDSP_LD") + + NID_F3_C_SWSP_SW = new_constant(OP_CONST, SID_FUNCT3, F3_C_SWSP_SW, "F3_C_SWSP_SW") + NID_F3_C_SDSP_SD = new_constant(OP_CONST, SID_FUNCT3, F3_C_SDSP_SD, "F3_C_SDSP_SD") + + NID_F3_C_BEQZ = new_constant(OP_CONST, SID_FUNCT3, F3_C_BEQZ, "F3_C_BEQZ") + NID_F3_C_BNEZ = new_constant(OP_CONST, SID_FUNCT3, F3_C_BNEZ, "F3_C_BNEZ") + + NID_F3_C_J = new_constant(OP_CONST, SID_FUNCT3, F3_C_J, "F3_C_J") + + SID_FUNCT4 = new_bitvec(4, "compressed funct4 sort") + + NID_F4_C_MV_JR = new_constant(OP_CONST, SID_FUNCT4, F4_C_MV_JR, "F4_C_MV_JR") + NID_F4_C_ADD_JALR = new_constant(OP_CONST, SID_FUNCT4, F4_C_ADD_JALR, "F4_C_ADD_JALR") + + # offset sorts + + SID_1_BIT_OFFSET = new_bitvec(1, "1-bit offset sort") + SID_2_BIT_OFFSET = new_bitvec(2, "2-bit offset sort") + SID_3_BIT_OFFSET = new_bitvec(3, "3-bit offset sort") + SID_4_BIT_OFFSET = new_bitvec(4, "4-bit offset sort") + SID_5_BIT_OFFSET = new_bitvec(5, "5-bit offset sort") + SID_6_BIT_OFFSET = new_bitvec(6, "6-bit offset sort") + SID_7_BIT_OFFSET = new_bitvec(7, "7-bit offset sort") + SID_8_BIT_OFFSET = new_bitvec(8, "8-bit offset sort") + SID_9_BIT_OFFSET = new_bitvec(9, "9-bit offset sort") + SID_10_BIT_OFFSET = new_bitvec(10, "10-bit offset sort") + SID_11_BIT_OFFSET = new_bitvec(11, "11-bit offset sort") + SID_12_BIT_OFFSET = new_bitvec(12, "12-bit offset sort") + SID_17_BIT_OFFSET = new_bitvec(17, "17-bit offset sort") + SID_18_BIT_OFFSET = new_bitvec(18, "18-bit offset sort") + + NID_1_BIT_OFFSET_0 = new_constant(OP_CONST, SID_1_BIT_OFFSET, 0, "1-bit offset 0") + NID_1_BIT_OFFSET_1 = new_constant(OP_CONST, SID_1_BIT_OFFSET, 1, "1-bit offset 1") + NID_2_BIT_OFFSET_0 = new_constant(OP_CONST, SID_2_BIT_OFFSET, 0, "2-bit offset 0") + NID_2_BIT_OFFSET_1 = new_constant(OP_CONST, SID_2_BIT_OFFSET, 1, "2-bit offset 1, 01000 s0") + NID_3_BIT_OFFSET_0 = new_constant(OP_CONST, SID_3_BIT_OFFSET, 0, "3-bit offset 0") + NID_4_BIT_OFFSET_0 = new_constant(OP_CONST, SID_4_BIT_OFFSET, 0, "4-bit offset 0") + NID_12_BIT_OFFSET_0 = new_constant(OP_CONST, SID_12_BIT_OFFSET, 0, "12-bit offset 0") + + SID_COMPRESSED_REGISTER_ADDRESS = new_bitvec(3, "3-bit compressed register address") + + # RVC instruction switches + + if RISCUONLY: + RVC = False + + NID_C_LI = NID_DISABLED + NID_C_LUI = NID_DISABLED + + NID_C_ADDI = NID_DISABLED + NID_C_ADDIW = NID_DISABLED + NID_C_ADDI16SP = NID_DISABLED + + NID_C_ADDI4SPN = NID_DISABLED + + NID_C_ANDI = NID_DISABLED + + NID_C_SLLI = NID_DISABLED + NID_C_SRLI = NID_DISABLED + NID_C_SRAI = NID_DISABLED + + NID_C_MV = NID_DISABLED + NID_C_ADD = NID_DISABLED + + NID_C_SUB = NID_DISABLED + NID_C_XOR = NID_DISABLED + NID_C_OR = NID_DISABLED + NID_C_AND = NID_DISABLED + + NID_C_ADDW = NID_DISABLED + NID_C_SUBW = NID_DISABLED + + NID_C_LWSP = NID_DISABLED + NID_C_LW = NID_DISABLED + + NID_C_LDSP = NID_DISABLED + NID_C_LD = NID_DISABLED + + NID_C_SWSP = NID_DISABLED + NID_C_SW = NID_DISABLED + + NID_C_SDSP = NID_DISABLED + NID_C_SD = NID_DISABLED + + NID_C_BEQZ = NID_DISABLED + NID_C_BNEZ = NID_DISABLED + + NID_C_J = NID_DISABLED + NID_C_JAL = NID_DISABLED + + NID_C_JR = NID_DISABLED + NID_C_JALR = NID_DISABLED + + if not RVC: + # avoiding oversized then case + return + + NID_C_LI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LI, RISC_V_MNEMONICS[ID_C_LI]) + NID_C_LUI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LUI, RISC_V_MNEMONICS[ID_C_LUI]) + + NID_C_ADDI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADDI, RISC_V_MNEMONICS[ID_C_ADDI]) + if IS64BITTARGET: + NID_C_ADDIW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADDIW, RISC_V_MNEMONICS[ID_C_ADDIW]) + else: + NID_C_ADDIW = NID_DISABLED + NID_C_ADDI16SP = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADDI16SP, RISC_V_MNEMONICS[ID_C_ADDI16SP]) + + NID_C_ADDI4SPN = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADDI4SPN, RISC_V_MNEMONICS[ID_C_ADDI4SPN]) + + NID_C_ANDI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ANDI, RISC_V_MNEMONICS[ID_C_ANDI]) + + NID_C_SLLI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SLLI, RISC_V_MNEMONICS[ID_C_SLLI]) + NID_C_SRLI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SRLI, RISC_V_MNEMONICS[ID_C_SRLI]) + NID_C_SRAI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SRAI, RISC_V_MNEMONICS[ID_C_SRAI]) + + NID_C_MV = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_MV, RISC_V_MNEMONICS[ID_C_MV]) + NID_C_ADD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADD, RISC_V_MNEMONICS[ID_C_ADD]) + + NID_C_SUB = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SUB, RISC_V_MNEMONICS[ID_C_SUB]) + NID_C_XOR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_XOR, RISC_V_MNEMONICS[ID_C_XOR]) + NID_C_OR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_OR, RISC_V_MNEMONICS[ID_C_OR]) + NID_C_AND = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_AND, RISC_V_MNEMONICS[ID_C_AND]) + + if IS64BITTARGET: + NID_C_ADDW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_ADDW, RISC_V_MNEMONICS[ID_C_ADDW]) + NID_C_SUBW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SUBW, RISC_V_MNEMONICS[ID_C_SUBW]) + else: + NID_C_ADDW = NID_DISABLED + NID_C_SUBW = NID_DISABLED + + NID_C_LWSP = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LWSP, RISC_V_MNEMONICS[ID_C_LWSP]) + NID_C_LW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LW, RISC_V_MNEMONICS[ID_C_LW]) + + NID_C_SWSP = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SWSP, RISC_V_MNEMONICS[ID_C_SWSP]) + NID_C_SW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SW, RISC_V_MNEMONICS[ID_C_SW]) + + if IS64BITTARGET: + NID_C_LDSP = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LDSP, RISC_V_MNEMONICS[ID_C_LDSP]) + NID_C_LD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_LD, RISC_V_MNEMONICS[ID_C_LD]) + + NID_C_SDSP = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SDSP, RISC_V_MNEMONICS[ID_C_SDSP]) + NID_C_SD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_SD, RISC_V_MNEMONICS[ID_C_SD]) + else: + NID_C_LDSP = NID_DISABLED + NID_C_LD = NID_DISABLED + + NID_C_SDSP = NID_DISABLED + NID_C_SD = NID_DISABLED + + NID_C_BEQZ = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_BEQZ, RISC_V_MNEMONICS[ID_C_BEQZ]) + NID_C_BNEZ = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_BNEZ, RISC_V_MNEMONICS[ID_C_BNEZ]) + + NID_C_J = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_J, RISC_V_MNEMONICS[ID_C_J]) + if IS64BITTARGET: + NID_C_JAL = NID_DISABLED + else: + NID_C_JAL = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_JAL, RISC_V_MNEMONICS[ID_C_JAL]) + + NID_C_JR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_JR, RISC_V_MNEMONICS[ID_C_JR]) + NID_C_JALR = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_C_JALR, RISC_V_MNEMONICS[ID_C_JALR]) + +# system model + +class Bitvector_State(): + def __init__(self, core, sid, name, initials): + assert isinstance(sid, Bitvector), f"got {sid} but expected bitvector" + self.sid = sid + if core >= 0: + self.initial = new_constant(OP_CONSTD, self.sid, 0, f"initial core-{core} {name} value") + self.state = new_input(OP_STATE, self.sid, f"core-{core}-{initials}", f"{sid.size}-bit {name}") + else: + self.initial = new_constant(OP_CONSTD, self.sid, 0, f"initial {name} value") + self.state = new_input(OP_STATE, self.sid, f"{initials}", f"{sid.size}-bit {name}") + self.init = new_init(self.sid, self.state, self.initial, f"initializing {name}") + + def __str__(self): + return f"{self.state}" + +class Array_State(): + def __init__(self, core, array_sid, name, initials): + assert isinstance(array_sid, Array), f"got {array_sid} but expected array" + self.array_sid = array_sid + if core >= 0: + self.initial = new_constant(OP_CONSTD, array_sid.element_size_line, 0, f"initial core-{core} {name} value") + self.state = new_input(OP_STATE, array_sid, f"core-{core}-{initials}", f"{array_sid.array_size_line.size}-bit {name} of {array_sid.element_size_line.size}-bit bitvectors") + else: + self.initial = new_constant(OP_CONSTD, array_sid.element_size_line, 0, f"initial {name} value") + self.state = new_input(OP_STATE, array_sid, f"{initials}", f"{array_sid.array_size_line.size}-bit {name} of {array_sid.element_size_line.size}-bit bitvectors") + self.init = new_init(array_sid, self.state, self.initial, f"initializing {name}") + + def __str__(self): + return f"{self.state}" + +class PC(Bitvector_State): + def __init__(self, core): + super().__init__(core, SID_MACHINE_WORD, "program counter", 'pc') + +class Registers(Array_State): + def __init__(self, core): + super().__init__(core, SID_REGISTER_STATE, "register file", 'register-file') + +class Segment(Array_State): + def __init__(self, core, array_sid, start_nid, end_nid, name, initials): + assert isinstance(array_sid, Array) and isinstance(start_nid, Constant) and isinstance(end_nid, Constant) + super().__init__(core, array_sid, name, initials) + self.start_nid = start_nid + self.end_nid = end_nid + +class Memory(): + def __init__(self, core): + self.vaddr_sort_nid = SID_VIRTUAL_ADDRESS + self.code = Segment(core, SID_CODE_STATE, NID_CODE_START, NID_CODE_END, "code segment", 'code-segment') + self.data = Segment(core, SID_DATA_STATE, NID_DATA_START, NID_DATA_END, "data segment", 'data-segment') + self.heap = Segment(core, SID_HEAP_STATE, NID_HEAP_START, NID_HEAP_END, "heap segment", 'heap-segment') + self.stack = Segment(core, SID_STACK_STATE, NID_STACK_START, NID_STACK_END, "stack segment", 'stack-segment') + + def __str__(self): + return f"{self.vaddr_sort_nid.size}-bit virtual memory:\n{self.code}\n{self.data}\n{self.heap}\n{self.stack}" + +class Kernel(): + def __init__(self, core, memory): + assert isinstance(memory, Memory), f"got {memory} but expected memory" + self.memory = memory + self.program_break = Bitvector_State(-1, memory.vaddr_sort_nid, "program break", 'program-break') + self.file_descriptor = Bitvector_State(-1, SID_MACHINE_WORD, "file descriptor", 'file-descriptor') + self.input_buffer = Array_State(-1, SID_INPUT_BUFFER, "input buffer", 'input-buffer') + self.readable_bytes = Bitvector_State(core, SID_MACHINE_WORD, "readable bytes", 'readable-bytes') + self.read_bytes = Bitvector_State(core, SID_MACHINE_WORD, "read bytes", 'read-bytes') + + def __str__(self): + return f"kernel:\n{self.program_break}\n{self.file_descriptor}\n{self.input_buffer}\n{self.readable_bytes}\n{self.read_bytes}" + +class Core(): + cores = dict() + + def __init__(self): + self.core = len(Core.cores) + self.memory = Memory(self.core) + self.kernel = Kernel(self.core, self.memory) + self.pc = PC(self.core) + self.regs = Registers(self.core) + self.new_core() + + def __str__(self): + return f"{self.kernel}\n{self.memory}\ncore-{self.core}:\n{self.pc}\n{self.regs}" + + def new_core(self): + assert self.core not in Core.cores, f"{self.core} already defined" + Core.cores[self.core] = self + +class System(): + def __init__(self): + self.core = Core() # single core for now + + def __str__(self): + return f"{SID_MACHINE_WORD.size}-bit single-core system:\n{self.core}" + +# BTOR2 parser + +import re + +class syntax_error(Exception): + def __init__(self, expected, line_no): + super().__init__(f"syntax error in line {line_no}: {expected} expected") + +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 = get_token(tokens, expected, line_no) + if token.isdecimal(): + return int(token) + else: + raise syntax_error(expected, line_no) + +def get_nid_line(tokens, clss, expected, line_no): + nid = get_decimal(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 get_nid_line(tokens, Bitvector, "Boolean or bitvector sort nid", line_no) + +def get_bitvec_sid_line(tokens, line_no): + return get_nid_line(tokens, Bitvec, "bitvector sort nid", line_no) + +def get_sid_line(tokens, line_no): + return get_nid_line(tokens, Sort, "sort nid", line_no) + +def get_state_line(tokens, line_no): + return get_nid_line(tokens, State, "state nid", line_no) + +def get_exp_line(tokens, line_no): + return get_nid_line(tokens, Expression, "expression nid", line_no) + +def get_number(tokens, base, expected, line_no): + token = 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 get_token(tokens, None, None) + except: + return "" + +def get_comment(tokens, line_no): + comment = get_symbol(tokens) + if comment != "": + if comment[0] != ';': + raise syntax_error("comment", line_no) + return comment + +def parse_sort_line(tokens, nid, line_no): + token = get_token(tokens, "bitvector or array", line_no) + if token == Bitvec.keyword: + size = get_decimal(tokens, "bitvector size", line_no) + comment = get_comment(tokens, line_no) + # rotor-dependent Boolean declaration + if comment == "; Boolean" and size == 1: + return new_boolean(nid, line_no) + else: + return new_bitvec(size, comment, nid, line_no) + elif token == Array.keyword: + array_size_line = get_bitvec_sid_line(tokens, line_no) + element_size_line = get_bitvec_sid_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_array(array_size_line, element_size_line, comment, nid, line_no) + else: + raise syntax_error("bitvector or array", line_no) + +def parse_zero_one_line(tokens, nid, op, line_no): + sid_line = get_bool_or_bitvec_sid_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_zero_one(op, sid_line, comment, nid, line_no) + +def parse_constant_line(tokens, nid, op, line_no): + sid_line = get_bool_or_bitvec_sid_line(tokens, line_no) + if op == Constd.keyword: + value = get_number(tokens, 10, "signed integer", line_no) + elif op == Const.keyword: + value = get_number(tokens, 2, "binary number", line_no) + elif op == Consth.keyword: + value = get_number(tokens, 16, "hexadecimal number", line_no) + comment = get_comment(tokens, line_no) + return new_constant(op, sid_line, value, comment, nid, line_no) + +def parse_symbol_comment(tokens, line_no): + symbol = get_symbol(tokens) + comment = get_comment(tokens, line_no) + if symbol != "": + if symbol[0] == ';': + return "", symbol + return symbol, comment + +def parse_variable_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + symbol, comment = parse_symbol_comment(tokens, line_no) + return new_input(op, sid_line, symbol, comment, nid, line_no) + +def parse_ext_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + arg1_line = get_exp_line(tokens, line_no) + w = get_decimal(tokens, "bit width", line_no) + comment = get_comment(tokens, line_no) + return new_ext(op, sid_line, arg1_line, w, comment, nid, line_no) + +def parse_slice_line(tokens, nid, line_no): + sid_line = get_sid_line(tokens, line_no) + arg1_line = get_exp_line(tokens, line_no) + u = get_decimal(tokens, "upper bit", line_no) + l = get_decimal(tokens, "lower bit", line_no) + comment = get_comment(tokens, line_no) + return new_slice(sid_line, arg1_line, u, l, comment, nid, line_no) + +def parse_unary_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + arg1_line = get_exp_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_unary(op, sid_line, arg1_line, comment, nid, line_no) + +def parse_binary_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + arg1_line = get_exp_line(tokens, line_no) + arg2_line = get_exp_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_binary(op, sid_line, arg1_line, arg2_line, comment, nid, line_no) + +def parse_ternary_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + arg1_line = get_exp_line(tokens, line_no) + arg2_line = get_exp_line(tokens, line_no) + arg3_line = get_exp_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_ternary(op, sid_line, arg1_line, arg2_line, arg3_line, comment, nid, line_no) + +def parse_init_next_line(tokens, nid, op, line_no): + sid_line = get_sid_line(tokens, line_no) + state_line = get_state_line(tokens, line_no) + exp_line = get_exp_line(tokens, line_no) + comment = get_comment(tokens, line_no) + return new_init_next(op, sid_line, state_line, exp_line, comment, nid, line_no) + +def parse_property_line(tokens, nid, op, line_no): + property_line = get_exp_line(tokens, line_no) + symbol, comment = parse_symbol_comment(tokens, line_no) + return new_property(op, property_line, symbol, comment, nid, line_no) + +def parse_btor2_line(line, line_no): + current_nid = 0 + + if line.strip(): + tokens = tokenize_btor2(line) + token = get_token(tokens, None, None) if token[0] != ';': if token.isdecimal(): nid = int(token) @@ -1215,194 +4283,382 @@ def parse_btor2_line(line, line_no): raise syntax_error("nid", line_no) return line.strip() -def parse_btor2(modelfile): +def parse_btor2(modelfile, outputfile): + lines = dict() line_no = 1 for line in modelfile: try: - parse_btor2_line(line, line_no) + lines[line_no] = parse_btor2_line(line, line_no) line_no += 1 except Exception as message: - print(message) + print(f"exception during parsing: {message}") exit(1) + if outputfile: + for line in lines.values(): + print(line, file=outputfile) + for state in State.states.values(): - if state.init_line == state: + if state.init_line is None: # state has no init state.new_input() -def new_problem(set_solver): - for init in Init.inits.values(): - set_solver(init) - for constraint in Constraint.constraints.values(): - set_solver(constraint) - for bad in Bad.bads.values(): - set_solver(bad) - for next_line in Next.nexts.values(): - set_solver(next_line) + 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 + + print("#" * 80) + + 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) + + return are_there_state_transitions + +# Z3 and bitwuzla solver interface + +class Solver(): + def __init__(self, solver): + self.solver = solver + + def push(self): + self.solver.push() + + def pop(self): + self.solver.pop() + +class Z3_Solver(Solver): + def __init__(self): + super().__init__(z3.Solver()) + + def assert_this(self, assertions, step): + for assertion in assertions: + self.solver.add(assertion.get_z3_step(step)) + + def assert_not_this(self, assertions, step): + for assertion in assertions: + self.solver.add(assertion.get_z3_step(step) == False) + + def prove(self): + return self.solver.check() + + def is_SAT(self, result): + return result == z3.sat + + def is_UNSAT(self, result): + return result == z3.unsat + + def assert_change(self, next_line, step): + return self.solver.add(next_line.get_z3_change(step)) + + def print_pc(self, pc, step): + self.prove() + model = self.solver.model() + for decl in model.decls(): + if str(pc.get_z3_step(step)) in str(decl.name()): + pc_value = int(model[decl].as_long()) + print(pc) + print("%s = 0x%X" % (decl.name(), pc_value)) + + def print_inputs(self, inputs, step): + model = self.solver.model() + for input_variable in inputs.values(): + # only print value of uninitialized states + print(input_variable) + for decl in model.decls(): + if str(input_variable.get_z3_step(step)) in str(decl.name()): + print("%s = %s" % (decl.name(), model[decl])) + +class Bitwuzla_Solver(Solver): + def __init__(self): + self.tm = bitwuzla.TermManager() + self.options = bitwuzla.Options() + self.options.set(bitwuzla.Option.PRODUCE_MODELS, True) + super().__init__(bitwuzla.Bitwuzla(self.tm, self.options)) + + def assert_this(self, assertions, step): + for assertion in assertions: + self.solver.assert_formula(assertion.get_bitwuzla_step(step, self.tm)) + + def assert_not_this(self, assertions, step): + for assertion in assertions: + self.solver.assert_formula(self.tm.mk_term(bitwuzla.Kind.NOT, [assertion.get_bitwuzla_step(step, self.tm)])) -def new_z3(): - new_problem(lambda line: line.set_z3(0)) + def prove(self): + return self.solver.check_sat() -def new_bitwuzla(tm): - new_problem(lambda line: line.set_bitwuzla(0, tm)) + def is_SAT(self, result): + return result is bitwuzla.Result.SAT -def bmc_z3(kmin, kmax, print_pc): - s = z3.Solver() + def is_UNSAT(self, result): + return result is bitwuzla.Result.UNSAT - for init in Init.inits.values(): - s.add(init.z3) + def assert_change(self, next_line, step): + return self.solver.assert_formula(next_line.get_bitwuzla_change(step, self.tm)) - step = 0 + def print_pc(self, pc, step): + self.prove() + pc_value = int(self.solver.get_value(pc.get_bitwuzla_step(step, self.tm)).value(16), 16) + print(pc) + print("%s = 0x%X" % (pc.get_bitwuzla_step(step, self.tm), pc_value)) + def print_inputs(self, inputs, step): + for input_variable in inputs.values(): + # only print value of uninitialized states + print(input_variable) + print("%s = %s" % (input_variable.get_bitwuzla_step(step, self.tm), + self.solver.get_value(input_variable.get_bitwuzla_step(step, self.tm)))) + +# bitme bounded model checker + +def branching_bmc(solver, kmin, kmax, args, step, level): while step <= kmax: - print(step) + # check model up to kmax steps + if level == 0: + print(step) + else: + print(f"{step}-{level}") - if print_pc and State.pc: - s.check() - m = s.model() - for d in m.decls(): - if str(State.pc.next_line.current_step) in str(d.name()): - print(State.pc.next_line.state_line) - print("%s = %s" % (d.name(), m[d])) + if args.print_pc and State.pc: + # print current program counter value of single-core rotor model + solver.print_pc(State.pc, step) - for constraint in Constraint.constraints.values(): - s.add(constraint.z3) + # assert all constraints + solver.assert_this(Constraint.constraints.values(), step) if step >= kmin: + # check bad properties from kmin on for bad in Bad.bads.values(): - s.push() - s.add(bad.z3) - result = s.check() - if result == z3.sat: + # check all bad properties + solver.push() + solver.assert_this([bad], step) + result = solver.prove() + if solver.is_SAT(result): print("v" * 80) print(f"sat: {bad}") - m = s.model() - for d in m.decls(): - for input_variable in Variable.inputs.values(): - if str(input_variable.z3) in str(d.name()): - # only print value of uninitialized states - print(input_variable) - print("%s = %s" % (d.name(), m[d])) + solver.print_inputs(Variable.inputs, step) print("^" * 80) - s.pop() - if result == z3.unsat: - s.add(bad.z3 == False) - else: - for bad in Bad.bads.values(): - s.add(bad.z3 == False) + solver.pop() + + if not args.unconstraining_bad: + # assert all bad properties as negated constraints + solver.assert_not_this(Bad.bads.values(), step) + + # compute next step + solver.assert_this(Next.nexts.values(), step) + + if args.check_termination and step >= kmin: + state_change = False + for next_line in Next.nexts.values(): + # check if any of the states changes + solver.push() + solver.assert_change(next_line, step) + result = solver.prove() + solver.pop() + if solver.is_SAT(result): + state_change = True + print(f"state change: {next_line}") + # break for efficiency + if not state_change and next_line == list(Next.nexts.values())[-1]: + print("no states changed: terminating") + return - for next_line in Next.nexts.values(): - s.add(next_line.z3) + if args.branching and Ite.branching_conditions and Ite.non_branching_conditions: + solver.push() + solver.assert_this([Ite.branching_conditions], step) + branching_result = solver.is_SAT(solver.prove()) + solver.pop() - current_states = [next_line.current_step for next_line in Next.nexts.values()] - next_states = [next_line.next_step for next_line in Next.nexts.values()] - renaming = [current_next for current_next in zip(current_states, next_states)] + solver.push() + solver.assert_not_this([Ite.non_branching_conditions], step) + non_branching_result = solver.is_SAT(solver.prove()) + solver.pop() - for constraint in Constraint.constraints.values(): - constraint.z3 = z3.substitute(constraint.z3, renaming) - for bad in Bad.bads.values(): - bad.z3 = z3.substitute(bad.z3, renaming) + 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) - for next_line in Next.nexts.values(): - next_line.exp_line.z3 = z3.substitute(next_line.exp_line.z3, renaming) + if branching_result and non_branching_result: + print("v" * 80) + print(f"branching @ {step}-{level}") - for next_line in Next.nexts.values(): - next_line.set_z3(step + 1) + solver.push() + solver.assert_this([Ite.branching_conditions], step) + + branching_bmc(solver, kmin, kmax, args, step + 1, level + 1) + + solver.pop() + + print("-" * 80) + print(f"not branching @ {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("^" * 80) + return step += 1 -def bmc_bitwuzla(tm, options, kmin, kmax, print_pc): - s = bitwuzla.Bitwuzla(tm, options) +def bmc(solver, kmin, kmax, args): + print("#" * 80) - for init in Init.inits.values(): - s.assert_formula(init.bitwuzla) + print(f"bounded model checking: -kmin {kmin} -kmax {kmax}") - step = 0 + # initialize all states + solver.assert_this(Init.inits.values(), 0) - while step <= kmax: - print(step) + return branching_bmc(solver, kmin, kmax, args, 0, 0) - if print_pc and State.pc: - s.check_sat() - print(State.pc.next_line.state_line) - print("%s = %s" % (State.pc.next_line.current_step, - s.get_value(State.pc.next_line.current_step))) +# rotor model generator - for constraint in Constraint.constraints.values(): - s.assert_formula(constraint.bitwuzla) +def load_binary(): + global max_code_size - if step >= kmin: - for bad in Bad.bads.values(): - result = s.check_sat(bad.bitwuzla) - if result is bitwuzla.Result.SAT: - print("v" * 80) - print(f"sat: {bad}") - for input_variable in Variable.inputs.values(): - # only print value of uninitialized states - print(input_variable) - print("%s = %s" % (input_variable.bitwuzla, - s.get_value(input_variable.bitwuzla))) - print("^" * 80) - elif result is bitwuzla.Result.UNSAT: - s.assert_formula(tm.mk_term(bitwuzla.Kind.NOT, [bad.bitwuzla])) - else: - for bad in Bad.bads.values(): - s.assert_formula(tm.mk_term(bitwuzla.Kind.NOT, [bad.bitwuzla])) + global code_start + global code_size - for next_line in Next.nexts.values(): - s.assert_formula(next_line.bitwuzla) + global max_data_size - for state in State.states.values(): - state.set_bitwuzla(step + 1, tm) + global data_start + global data_size - for constraint in Constraint.constraints.values(): - constraint.set_bitwuzla(step + 1, tm) - for bad in Bad.bads.values(): - bad.set_bitwuzla(step + 1, tm) + global heap_initial_size - for next_line in Next.nexts.values(): - next_line.set_bitwuzla(step + 1, tm) + global heap_start + global heap_size - step += 1 + global stack_initial_size + + global stack_start + global stack_size + + max_code_size = 7 * INSTRUCTIONSIZE + + code_start = 4096; + code_size = max_code_size; + + max_data_size = WORDSIZE + + data_start = 8192; + data_size = max_data_size; + + heap_initial_size = 0; + + heap_start = 12288; + heap_size = heap_allowance; + + stack_initial_size = 0; + + stack_start = VIRTUALMEMORYSIZE * GIGABYTE - stack_allowance; + stack_size = stack_allowance; + + assert stack_start >= heap_start + heap_size > 0 + +def rotor_model(): + try: + load_binary() + + init_machine_interface() + init_kernel_interface() + init_register_file_sorts() + init_memory_sorts() + + new_segmentation() + + init_instruction_sorts() + init_compressed_instruction_sorts() + + print(System()) + except Exception as message: + print(f"exception during modeling: {message}") + exit(1) + +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="What the program does", - epilog="Text at the bottom of help") + 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') + parser.add_argument('modelfile', type=argparse.FileType('r')) + parser.add_argument('outputfile', nargs='?', type=argparse.FileType('w', encoding='UTF-8')) parser.add_argument('-kmin', nargs=1, type=int) parser.add_argument('-kmax', nargs=1, type=int) + parser.add_argument('--use-Z3', action='store_true') + parser.add_argument('--use-bitwuzla', action='store_true') + parser.add_argument('--print-pc', action='store_true') + parser.add_argument('--check-termination', action='store_true') + parser.add_argument('--unconstraining-bad', action='store_true') + parser.add_argument('--branching', action='store_true') args = parser.parse_args() - with open(args.modelfile) as modelfile: - parse_btor2(modelfile) + are_there_state_transitions = parse_btor2(args.modelfile, args.outputfile) if args.kmin or args.kmax: kmin = args.kmin[0] if args.kmin else 0 kmax = args.kmax[0] if args.kmax else 0 - kmax = max(kmin, kmax) - - use_Z3 = True - - if is_Z3_present and use_Z3: - new_z3() - bmc_z3(kmin, kmax, args.print_pc) + if are_there_state_transitions: + kmax = max(kmin, kmax) + else: + kmin = kmax = 0 - if is_bitwuzla_present: - tm = bitwuzla.TermManager() - options = bitwuzla.Options() - options.set(bitwuzla.Option.PRODUCE_MODELS, True) + if is_Z3_present and args.use_Z3: + solver = Z3_Solver() + bmc(solver, kmin, kmax, args) - new_bitwuzla(tm) - bmc_bitwuzla(tm, options, kmin, kmax, args.print_pc) + if is_bitwuzla_present and args.use_bitwuzla: + solver = Bitwuzla_Solver() + bmc(solver, kmin, kmax, args) if __name__ == '__main__': main() \ No newline at end of file diff --git a/tools/rotor.c b/tools/rotor.c index 6af3e2b8..4ca63e8e 100644 --- a/tools/rotor.c +++ b/tools/rotor.c @@ -11,6 +11,7 @@ selfie.cs.uni-salzburg.at Rotor is a tool for bit-precise reasoning about RISC-V machines and RISC-V code using BTOR2 and SMT-LIB as modeling format. +Rotor utilizes the compiler and bootloader of the selfie system. Rotor generates models of 64-bit and 32-bit RISC-V machines supporting 64-bit and 32-bit integer arithmetic (RV64I, RV32I) @@ -125,6 +126,8 @@ uint64_t* new_ternary(char* op, uint64_t* sid, uint64_t* first_nid, uint64_t* se uint64_t* new_init(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char* comment); uint64_t* new_next(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char* comment); +uint64_t* new_register_file_next(uint64_t* state_nid, uint64_t* value_nid, char* comment); + uint64_t* new_property(char* op, uint64_t* condition_nid, char* symbol, char* comment); // ------------------------ GLOBAL CONSTANTS ----------------------- @@ -140,6 +143,9 @@ char* ARRAY = (char*) 0; char* OP_SORT = (char*) 0; +char* OP_ZERO = (char*) 0; +char* OP_ONE = (char*) 0; + char* OP_CONST = (char*) 0; char* OP_CONSTD = (char*) 0; char* OP_CONSTH = (char*) 0; @@ -218,6 +224,9 @@ void init_model() { OP_SORT = "sort"; + OP_ZERO = "zero"; + OP_ONE = "one"; + OP_CONST = "const"; OP_CONSTD = "constd"; OP_CONSTH = "consth"; @@ -303,7 +312,10 @@ void print_nid(uint64_t nid, uint64_t* line); void print_comment(uint64_t* line); uint64_t print_sort(uint64_t nid, uint64_t* line); + +void print_boolean_and_constd(uint64_t* sid, uint64_t value); uint64_t print_constant(uint64_t nid, uint64_t* line); + uint64_t print_input(uint64_t nid, uint64_t* line); uint64_t print_ext(uint64_t nid, uint64_t* line); @@ -484,7 +496,7 @@ uint64_t* eval_good_nid = (uint64_t*) 0; // ----------------------------------------------------------------- // *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ -void print_interface_sorts(); +void print_machine_interface(); // ------------------------ GLOBAL CONSTANTS ----------------------- @@ -559,7 +571,7 @@ uint64_t* SID_DOUBLE_MACHINE_WORD = (uint64_t*) 0; // ------------------------- INITIALIZATION ------------------------ -void init_interface_sorts() { +void init_machine_interface() { SID_BOOLEAN = new_bitvec(1, "Boolean"); NID_FALSE = new_constant(OP_CONSTD, SID_BOOLEAN, 0, "false"); @@ -648,7 +660,7 @@ void init_interface_sorts() { // ---------------------------- KERNEL ----------------------------- // ----------------------------------------------------------------- -void print_interface_kernel(); +void print_kernel_interface(); uint64_t get_power_of_two_size_in_bytes(uint64_t size_in_bits); uint64_t calculate_address_space(uint64_t number_of_bytes, uint64_t word_size_in_bits); @@ -717,7 +729,7 @@ uint64_t* eval_more_than_one_readable_byte_to_read_nid = (uint64_t*) 0; // ------------------------- INITIALIZATION ------------------------ -void init_interface_kernel() { +void init_kernel_interface() { uint64_t saved_reuse_lines; NID_MAX_STRING_LENGTH = new_constant(OP_CONSTD, SID_MACHINE_WORD, @@ -775,10 +787,22 @@ void init_kernels(uint64_t number_of_cores) { // --------------------------- REGISTERS --------------------------- // ----------------------------------------------------------------- +uint64_t* allocate_array_nids() { + return smalloc(3 * sizeof(uint64_t*)); +} + +uint64_t* get_array_status_nid(uint64_t* array) { return (uint64_t*) *array; } +uint64_t* get_array_address_nid(uint64_t* array) { return (uint64_t*) *(array + 1); } +uint64_t* get_array_value_nid(uint64_t* array) { return (uint64_t*) *(array + 2); } + +void set_array_status_nid(uint64_t* array, uint64_t* status_nid) { *array = (uint64_t) status_nid; } +void set_array_address_nid(uint64_t* array, uint64_t* address_nid) { *(array + 1) = (uint64_t) address_nid; } +void set_array_value_nid(uint64_t* array, uint64_t* value_nid) { *(array + 2) = (uint64_t) value_nid; } + void print_register_sorts(); uint64_t* load_register_value(uint64_t* reg_nid, char* comment, uint64_t* register_file_nid); -uint64_t* store_register_value(uint64_t* reg_nid, uint64_t* value_nid, char* comment, uint64_t* register_file_nid); +uint64_t* store_register_value(uint64_t* sid, uint64_t* reg_nid, uint64_t* value_nid, char* comment, uint64_t* register_file_nid); uint64_t* get_5_bit_shamt(uint64_t* value_nid); uint64_t* get_shamt(uint64_t* value_nid); @@ -828,6 +852,8 @@ uint64_t* SID_REGISTER_STATE = (uint64_t*) 0; uint64_t SYNCHRONIZED_REGISTERS = 0; // flag for synchronized registers across cores uint64_t SHARED_REGISTERS = 0; // flag for shared registers across cores +uint64_t REGISTER_FILE_ARRAY = 1; + // ------------------------ GLOBAL VARIABLES ----------------------- uint64_t* init_zeroed_register_file_nids = (uint64_t*) 0; @@ -1177,6 +1203,8 @@ uint64_t* NID_BYTE_SIZE_IN_BASE_BITS = (uint64_t*) 0; // code segment +uint64_t max_code_size = 0; + uint64_t* init_zeroed_code_segment_nids = (uint64_t*) 0; uint64_t* next_zeroed_code_segment_nids = (uint64_t*) 0; @@ -1195,6 +1223,8 @@ uint64_t* initial_tail_nid = (uint64_t*) 0; // data segment +uint64_t max_data_size = 0; + uint64_t* init_zeroed_data_segment_nids = (uint64_t*) 0; uint64_t* next_zeroed_data_segment_nids = (uint64_t*) 0; @@ -1255,7 +1285,7 @@ uint64_t* eval_core_0_stack_segment_data_flow_nid = (uint64_t*) 0; // ------------------------- INITIALIZATION ------------------------ -void init_memory_sorts(uint64_t max_code_size, uint64_t max_data_size) { +void init_memory_sorts() { uint64_t saved_reuse_lines; if (VIRTUAL_ADDRESS_SPACE < WORDSIZEINBITS) @@ -1599,6 +1629,7 @@ uint64_t* store_no_seg_faults(uint64_t* ir_nid, uint64_t* register_file_nid, uint64_t* core_memory_data_flow(uint64_t* ir_nid, uint64_t* register_file_nid, uint64_t* segment_nid); +uint64_t* branch_conditions(uint64_t* ir_nid, uint64_t* register_file_nid, char* comment, uint64_t* non_branching_nid); uint64_t* get_pc_value_plus_SB_immediate(uint64_t* pc_nid, uint64_t* ir_nid); uint64_t* execute_branch(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* condition_nid); uint64_t* branch_control_flow(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* register_file_nid, uint64_t* other_control_flow_nid); @@ -1771,6 +1802,7 @@ uint64_t* compressed_store_no_seg_faults(uint64_t* c_ir_nid, uint64_t* register_ uint64_t* core_compressed_memory_data_flow(uint64_t* c_ir_nid, uint64_t* register_file_nid, uint64_t* segment_nid, uint64_t* other_memory_data_flow_nid); +uint64_t* compressed_branch_conditions(uint64_t* c_ir_nid, uint64_t* register_file_nid, char* comment, uint64_t* non_branching_nid); uint64_t* get_pc_value_plus_CB_offset(uint64_t* pc_nid, uint64_t* c_ir_nid); uint64_t* execute_compressed_branch(uint64_t* pc_nid, uint64_t* c_ir_nid, uint64_t* condition_nid); uint64_t* compressed_branch_control_flow(uint64_t* pc_nid, uint64_t* c_ir_nid, uint64_t* register_file_nid, uint64_t* other_control_flow_nid); @@ -2193,6 +2225,7 @@ uint64_t* NID_C_SUB = (uint64_t*) 0; uint64_t* NID_C_XOR = (uint64_t*) 0; uint64_t* NID_C_OR = (uint64_t*) 0; uint64_t* NID_C_AND = (uint64_t*) 0; + uint64_t* NID_C_ADDW = (uint64_t*) 0; uint64_t* NID_C_SUBW = (uint64_t*) 0; @@ -2219,7 +2252,7 @@ uint64_t* NID_C_JALR = (uint64_t*) 0; // instruction IDs -uint64_t ID_UNKOWN = 0; +uint64_t ID_UNKNOWN = 0; uint64_t ID_ECALL = 1; @@ -2315,69 +2348,69 @@ uint64_t ID_JAL = 63; // CR-type -uint64_t ID_C_MV = 64; // "c.mv"; -uint64_t ID_C_ADD = 65; // "c.add"; +uint64_t ID_C_MV = 64; +uint64_t ID_C_ADD = 65; -uint64_t ID_C_JR = 66; // "c.jr"; -uint64_t ID_C_JALR = 67; // "c.jalr"; +uint64_t ID_C_JR = 66; +uint64_t ID_C_JALR = 67; // CI-type -uint64_t ID_C_LI = 68; // "c.li"; -uint64_t ID_C_LUI = 69; // "c.lui"; +uint64_t ID_C_LI = 68; +uint64_t ID_C_LUI = 69; -uint64_t ID_C_ADDI = 70; // "c.addi"; -uint64_t ID_C_ADDIW = 71; // "c.addiw"; -uint64_t ID_C_ADDI16SP = 72; // "c.addi16sp"; +uint64_t ID_C_ADDI = 70; +uint64_t ID_C_ADDIW = 71; +uint64_t ID_C_ADDI16SP = 72; // CIW-type -uint64_t ID_C_ADDI4SPN = 73; // "c.addi4spn"; +uint64_t ID_C_ADDI4SPN = 73; // CI-type -uint64_t ID_C_SLLI = 74; // "c.slli"; +uint64_t ID_C_SLLI = 74; -uint64_t ID_C_LWSP = 75; // "c.lwsp"; -uint64_t ID_C_LDSP = 76; // "c.ldsp"; +uint64_t ID_C_LWSP = 75; +uint64_t ID_C_LDSP = 76; // CL-type -uint64_t ID_C_LW = 77; // "c.lw"; -uint64_t ID_C_LD = 78; // "c.ld"; +uint64_t ID_C_LW = 77; +uint64_t ID_C_LD = 78; // CS-type -uint64_t ID_C_SW = 79; // "c.sw"; -uint64_t ID_C_SD = 80; // "c.sd"; +uint64_t ID_C_SW = 79; +uint64_t ID_C_SD = 80; -uint64_t ID_C_SUB = 81; // "c.sub"; -uint64_t ID_C_XOR = 82; // "c.xor"; -uint64_t ID_C_OR = 83; // "c.or"; -uint64_t ID_C_AND = 84; // "c.and"; +uint64_t ID_C_SUB = 81; +uint64_t ID_C_XOR = 82; +uint64_t ID_C_OR = 83; +uint64_t ID_C_AND = 84; -uint64_t ID_C_ADDW = 85; // "c.addw"; -uint64_t ID_C_SUBW = 86; // "c.subw"; +uint64_t ID_C_ADDW = 85; +uint64_t ID_C_SUBW = 86; // CSS-type -uint64_t ID_C_SWSP = 87; // "c.swsp"; -uint64_t ID_C_SDSP = 88; // "c.sdsp"; +uint64_t ID_C_SWSP = 87; +uint64_t ID_C_SDSP = 88; // CB-type -uint64_t ID_C_BEQZ = 89; // "c.beqz"; -uint64_t ID_C_BNEZ = 90; // "c.bnez"; +uint64_t ID_C_BEQZ = 89; +uint64_t ID_C_BNEZ = 90; -uint64_t ID_C_ANDI = 91; // "c.andi"; +uint64_t ID_C_ANDI = 91; -uint64_t ID_C_SRLI = 92; // "c.srli"; -uint64_t ID_C_SRAI = 93; // "c.srai"; +uint64_t ID_C_SRLI = 92; +uint64_t ID_C_SRAI = 93; // CJ-type -uint64_t ID_C_J = 94; // "c.j"; -uint64_t ID_C_JAL = 95; // "c.jal"; +uint64_t ID_C_J = 94; +uint64_t ID_C_JAL = 95; // pseudoinstruction IDs @@ -2432,12 +2465,15 @@ uint64_t* eval_instruction_ID_nids = (uint64_t*) 0; uint64_t* eval_compressed_instruction_ID_nids = (uint64_t*) 0; uint64_t* eval_ID_nids = (uint64_t*) 0; +uint64_t* branching_conditions_nid = (uint64_t*) 0; +uint64_t* non_branching_conditions_nid = (uint64_t*) 0; + // ------------------------- INITIALIZATION ------------------------ void init_instruction_mnemonics() { RISC_V_MNEMONICS = smalloc((ID_P_JALR + 1) * sizeof(char*)); - *(RISC_V_MNEMONICS + ID_UNKOWN) = (uint64_t) "unknown RISC-V instruction"; + *(RISC_V_MNEMONICS + ID_UNKNOWN) = (uint64_t) "unknown RISC-V instruction"; *(RISC_V_MNEMONICS + ID_ECALL) = (uint64_t) "ecall"; @@ -2727,7 +2763,7 @@ void init_instruction_sorts() { SID_INSTRUCTION_ID = new_bitvec(7, "7-bit instruction ID"); - NID_DISABLED = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_UNKOWN, get_instruction_mnemonic(ID_UNKOWN)); + NID_DISABLED = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_UNKNOWN, get_instruction_mnemonic(ID_UNKNOWN)); NID_LUI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LUI, get_instruction_mnemonic(ID_LUI)); NID_ADDI = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_ADDI, get_instruction_mnemonic(ID_ADDI)); @@ -2741,7 +2777,6 @@ void init_instruction_sorts() { NID_LW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LW, get_instruction_mnemonic(ID_LW)); NID_SW = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SW, get_instruction_mnemonic(ID_SW)); - NID_LD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_LD, get_instruction_mnemonic(ID_LD)); NID_SD = new_constant(OP_CONSTD, SID_INSTRUCTION_ID, ID_SD, get_instruction_mnemonic(ID_SD)); @@ -3296,6 +3331,8 @@ void init_cores(uint64_t number_of_cores) { uint64_t* state_property(uint64_t core, uint64_t* good_nid, uint64_t* bad_nid, char* symbol, char* comment); +uint64_t* kernel_register_data_flow(uint64_t* sid, uint64_t* ir_nid, + uint64_t* register_data_flow_nid, uint64_t* read_return_value_nid, uint64_t* register_file_nid); void kernel_combinational(uint64_t core, uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* control_flow_nid, uint64_t* register_data_flow_nid, uint64_t* heap_segment_data_flow_nid, @@ -3338,6 +3375,7 @@ void print_model(); int rotor_argc = 0; char** rotor_argv = (char**) 0; // original rotor console invocation +char* custom_model_name_option = (char*) 0; char* evaluate_model_option = (char*) 0; char* debug_model_option = (char*) 0; char* disassemble_model_option = (char*) 0; @@ -3380,6 +3418,7 @@ uint64_t target_exit_code = 0; // model for given exit code uint64_t number_of_binaries = 0; // number of loaded binaries +uint64_t custom_model_name = 0; uint64_t evaluate_model = 0; uint64_t output_assembly = 0; uint64_t disassemble_model = 0; @@ -3463,6 +3502,7 @@ void init_rotor(int argc, char** argv) { argv = argv + 1; } + custom_model_name_option = "-o"; evaluate_model_option = "-m"; debug_model_option = "-d"; disassemble_model_option = "-s"; @@ -3596,9 +3636,6 @@ uint64_t* code_sizes = (uint64_t*) 0; uint64_t* data_starts = (uint64_t*) 0; uint64_t* data_sizes = (uint64_t*) 0; -uint64_t max_code_size = 0; -uint64_t max_data_size = 0; - uint64_t min_steps = -1; uint64_t max_steps = 0; @@ -3786,6 +3823,42 @@ uint64_t* new_next(uint64_t* sid, uint64_t* state_nid, uint64_t* value_nid, char return new_line(OP_NEXT, sid, state_nid, value_nid, UNUSED, comment); } +uint64_t* new_register_file_next(uint64_t* state_nid, uint64_t* value_nid, char* comment) { + uint64_t* next_nid; + uint64_t i; + + if (REGISTER_FILE_ARRAY) + return new_next(SID_REGISTER_STATE, state_nid, value_nid, comment); + else { + next_nid = smalloc(32 * sizeof(uint64_t*)); + + i = 0; + + while (i < 32) { + if (i == 0) + *next_nid = (uint64_t) new_next(SID_REGISTER_STATE, (uint64_t*) *state_nid, (uint64_t*) *state_nid, comment); + else + *(next_nid + i) = (uint64_t) new_next(SID_REGISTER_STATE, (uint64_t*) *(state_nid + i), + new_ternary(OP_ITE, SID_MACHINE_WORD, + new_binary_boolean(OP_AND, + get_array_status_nid(value_nid), + new_binary_boolean(OP_EQ, + get_array_address_nid(value_nid), + new_constant(OP_CONST, SID_REGISTER_ADDRESS, i, (char*) *(REGISTERS + i)), + ""), + ""), + get_array_value_nid(value_nid), + (uint64_t*) *(state_nid + i), + ""), + comment); + + i = i + 1; + } + + return next_nid; + } +} + uint64_t* new_property(char* op, uint64_t* condition_nid, char* symbol, char* comment) { return new_line(op, UNUSED, condition_nid, (uint64_t*) symbol, UNUSED, comment); } @@ -3987,6 +4060,22 @@ uint64_t print_sort(uint64_t nid, uint64_t* line) { return nid; } +void print_boolean_and_constd(uint64_t* sid, uint64_t value) { + if (printing_smt) { + if (sid == SID_BOOLEAN) + if (is_true(value)) w = w + dprintf(output_fd, "true"); else w = w + dprintf(output_fd, "false"); + else + w = w + dprintf(output_fd, "(_ bv%lu %lu)", value, eval_bitvec_size(sid)); + } else { + if (value == 0) + w = w + dprintf(output_fd, " %s %lu", OP_ZERO, get_nid(sid)); + else if (value == 1) + w = w + dprintf(output_fd, " %s %lu", OP_ONE, get_nid(sid)); + else + w = w + dprintf(output_fd, " %s %lu %ld", OP_CONSTD, get_nid(sid), value); + } +} + uint64_t print_constant(uint64_t nid, uint64_t* line) { uint64_t value; uint64_t size; @@ -3995,10 +4084,8 @@ uint64_t print_constant(uint64_t nid, uint64_t* line) { size = eval_bitvec_size(get_sid(line)); if (printing_smt) { define_fun(line, nid, PREFIX_CONST); - if (get_sid(line) == SID_BOOLEAN) - if (is_true(value)) w = w + dprintf(output_fd, "true"); else w = w + dprintf(output_fd, "false"); - else if (get_op(line) == OP_CONSTD) - w = w + dprintf(output_fd, "(_ bv%lu %lu)", value, size); + if (or(get_sid(line) == SID_BOOLEAN, get_op(line) == OP_CONSTD)) + print_boolean_and_constd(get_sid(line), value); else if (get_op(line) == OP_CONST) w = w + dprintf(output_fd, "#b%s", itoa(value, string_buffer, 2, 0, size)); else @@ -4007,14 +4094,9 @@ uint64_t print_constant(uint64_t nid, uint64_t* line) { w = w + dprintf(output_fd, ")"); } else { print_nid(nid, line); - if (get_op(line) == OP_CONSTD) { - if (value == 0) - w = w + dprintf(output_fd, " zero %lu", get_nid(get_sid(line))); - else if (value == 1) - w = w + dprintf(output_fd, " one %lu", get_nid(get_sid(line))); - else - w = w + dprintf(output_fd, " %s %lu %ld", get_op(line), get_nid(get_sid(line)), value); - } else if (get_op(line) == OP_CONST) + if (get_op(line) == OP_CONSTD) + print_boolean_and_constd(get_sid(line), value); + else if (get_op(line) == OP_CONST) w = w + dprintf(output_fd, " %s %lu %s", get_op(line), get_nid(get_sid(line)), itoa(value, string_buffer, 2, 0, size)); else @@ -4265,14 +4347,11 @@ uint64_t print_propagated_constant(uint64_t nid, uint64_t* line) { nid = print_line_once(nid, get_sid(line)); if (printing_smt) { define_fun(line, nid, PREFIX_EVAL); - if (get_sid(line) == SID_BOOLEAN) - if (is_true(get_state(line))) w = w + dprintf(output_fd, "true"); else w = w + dprintf(output_fd, "false"); - else - w = w + dprintf(output_fd, "(_ bv%lu %lu)", get_state(line), eval_bitvec_size(get_sid(line))); + print_boolean_and_constd(get_sid(line), get_state(line)); w = w + dprintf(output_fd, ")"); } else { print_nid(nid, line); - w = w + dprintf(output_fd, " %s %lu %lu", OP_CONSTD, get_nid(get_sid(line)), get_state(line)); + print_boolean_and_constd(get_sid(line), get_state(line)); } if (printing_comments) w = w + dprintf(output_fd, " ; %s propagated", get_comment(line)); w = w + dprintf(output_fd, "\n"); @@ -5931,7 +6010,7 @@ void reset_state_for(uint64_t core, uint64_t* lines) { // ----------------------------------------------------------------- // *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ *~*~ -void print_interface_sorts() { +void print_machine_interface() { print_line(SID_BOOLEAN); print_line(SID_BYTE); @@ -5987,7 +6066,7 @@ void print_interface_sorts() { // ---------------------------- KERNEL ----------------------------- // ----------------------------------------------------------------- -void print_interface_kernel() { +void print_kernel_interface() { print_break_comment("kernel interface"); print_line(NID_EXIT_SYSCALL_ID); @@ -6147,12 +6226,48 @@ void print_register_sorts() { print_line(SID_REGISTER_STATE); } +uint64_t* read_register_value(uint64_t* reg_nid, char* comment, uint64_t* register_file_nid) { + uint64_t i; + uint64_t* value_nid; + + i = 0; + + while (i < 32) { + if (i == 0) + value_nid = NID_MACHINE_WORD_0; + else + value_nid = new_ternary(OP_ITE, SID_MACHINE_WORD, + new_binary_boolean(OP_EQ, + reg_nid, + new_constant(OP_CONST, SID_REGISTER_ADDRESS, i, (char*) *(REGISTERS + i)), + ""), + (uint64_t*) *(register_file_nid + i), + value_nid, + comment); + + i = i + 1; + } + + return value_nid; +} + uint64_t* load_register_value(uint64_t* reg_nid, char* comment, uint64_t* register_file_nid) { - return new_binary(OP_READ, SID_MACHINE_WORD, register_file_nid, reg_nid, comment); + if (REGISTER_FILE_ARRAY) + return new_binary(OP_READ, SID_MACHINE_WORD, register_file_nid, reg_nid, comment); + else + return read_register_value(reg_nid, comment, register_file_nid); } -uint64_t* store_register_value(uint64_t* reg_nid, uint64_t* value_nid, char* comment, uint64_t* register_file_nid) { - return new_ternary(OP_WRITE, SID_REGISTER_STATE, register_file_nid, reg_nid, value_nid, comment); +uint64_t* store_register_value(uint64_t* sid, uint64_t* reg_nid, uint64_t* value_nid, char* comment, uint64_t* register_file_nid) { + if (sid == SID_REGISTER_STATE) + return new_ternary(OP_WRITE, SID_REGISTER_STATE, register_file_nid, reg_nid, value_nid, comment); + else if (sid == SID_BOOLEAN) + return NID_TRUE; + else if (sid == SID_REGISTER_ADDRESS) + return reg_nid; + else + // assert: sid == SID_MACHINE_WORD + return value_nid; } uint64_t* get_5_bit_shamt(uint64_t* value_nid) { @@ -6206,7 +6321,7 @@ void new_register_file_state(uint64_t core) { new_unary(OP_DEC, SID_VIRTUAL_ADDRESS, NID_STACK_END, "end of stack segment - 1")); initial_register_file_nid = - store_register_value(NID_SP, value_nid, + store_register_value(SID_REGISTER_STATE, NID_SP, value_nid, "write initial sp register value", state_register_file_nid); if (eval_line(load_register_value(NID_SP, "read initial sp register value", @@ -6233,7 +6348,7 @@ void new_register_file_state(uint64_t core) { reg, format_comment("%s", *(REGISTERS + reg))); initial_register_file_nid = - store_register_value(reg_nid, value_nid, + store_register_value(SID_REGISTER_STATE, reg_nid, value_nid, "write initial register value", initial_register_file_nid); if (eval_line(load_register_value(reg_nid, "read initial register value", initial_register_file_nid)) != value) { @@ -9178,13 +9293,15 @@ uint64_t* auipc_data_flow(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* other_da other_data_flow_nid); } -uint64_t* core_register_data_flow(uint64_t* pc_nid, uint64_t* ir_nid, - uint64_t* register_file_nid, uint64_t* data_segment_nid, uint64_t* heap_segment_nid, uint64_t* stack_segment_nid) { +uint64_t* core_register_data_flow(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* register_file_nid, + uint64_t* data_segment_nid, uint64_t* heap_segment_nid, uint64_t* stack_segment_nid) { uint64_t* opcode_nid; uint64_t* rd_nid; uint64_t* rd_value_nid; + uint64_t* is_there_register_data_flow_nid; + uint64_t* register_data_flow_nid; opcode_nid = get_instruction_opcode(ir_nid); @@ -9192,7 +9309,7 @@ uint64_t* core_register_data_flow(uint64_t* pc_nid, uint64_t* ir_nid, rd_nid = get_instruction_rd(ir_nid); rd_value_nid = load_register_value(rd_nid, "current rd value", register_file_nid); - register_data_flow_nid = new_binary_boolean(OP_AND, + is_there_register_data_flow_nid = new_binary_boolean(OP_AND, new_binary_boolean(OP_NEQ, rd_nid, NID_ZR, "rd != register zero?"), new_binary_boolean(OP_AND, new_binary_boolean(OP_NEQ, opcode_nid, NID_OP_STORE, "opcode != STORE?"), @@ -9210,11 +9327,21 @@ uint64_t* core_register_data_flow(uint64_t* pc_nid, uint64_t* ir_nid, lui_data_flow(ir_nid, auipc_data_flow(pc_nid, ir_nid, rd_value_nid))))))); - return new_ternary(OP_ITE, SID_REGISTER_STATE, - register_data_flow_nid, - store_register_value(rd_nid, rd_value_nid, "rd update", register_file_nid), - register_file_nid, - "register data flow"); + if (REGISTER_FILE_ARRAY) + return new_ternary(OP_ITE, SID_REGISTER_STATE, + is_there_register_data_flow_nid, + store_register_value(SID_REGISTER_STATE, rd_nid, rd_value_nid, "rd update", register_file_nid), + register_file_nid, + "register data flow"); + else { + register_data_flow_nid = allocate_array_nids(); + + set_array_status_nid(register_data_flow_nid, is_there_register_data_flow_nid); + set_array_address_nid(register_data_flow_nid, rd_nid); + set_array_value_nid(register_data_flow_nid, rd_value_nid); + + return register_data_flow_nid; + } } uint64_t* get_rs1_value_plus_S_immediate(uint64_t* ir_nid, uint64_t* register_file_nid) { @@ -9283,6 +9410,29 @@ uint64_t* core_memory_data_flow(uint64_t* ir_nid, uint64_t* register_file_nid, u return store_memory_data_flow(ir_nid, register_file_nid, segment_nid, segment_nid); } +uint64_t* branch_conditions(uint64_t* ir_nid, uint64_t* register_file_nid, char* comment, uint64_t* non_branching_nid) { + uint64_t* rs1_value_nid; + uint64_t* rs2_value_nid; + + // only needed for controlling branching in bitme + + // TODO: avoid code duplication with branch_control_flow + + rs1_value_nid = load_register_value(get_instruction_rs1(ir_nid), "rs1 value", register_file_nid); + rs2_value_nid = load_register_value(get_instruction_rs2(ir_nid), "rs2 value", register_file_nid); + + return decode_branch(SID_BOOLEAN, ir_nid, + new_binary_boolean(OP_EQ, rs1_value_nid, rs2_value_nid, "rs1 value == rs2 value?"), + new_binary_boolean(OP_NEQ, rs1_value_nid, rs2_value_nid, "rs1 value != rs2 value?"), + new_binary_boolean(OP_SLT, rs1_value_nid, rs2_value_nid, "rs1 value < rs2 value?"), + new_binary_boolean(OP_SGTE, rs1_value_nid, rs2_value_nid, "rs1 value >= rs2 value?"), + new_binary_boolean(OP_ULT, rs1_value_nid, rs2_value_nid, "rs1 value < rs2 value (unsigned)?"), + new_binary_boolean(OP_UGTE, rs1_value_nid, rs2_value_nid, "rs1 value >= rs2 value (unsigned)?"), + comment, + non_branching_nid, + non_branching_nid); +} + uint64_t* get_pc_value_plus_SB_immediate(uint64_t* pc_nid, uint64_t* ir_nid) { return new_binary(OP_ADD, SID_MACHINE_WORD, pc_nid, @@ -10470,16 +10620,39 @@ uint64_t* core_compressed_register_data_flow(uint64_t* pc_nid, uint64_t* c_ir_ni "register data flow", NID_MACHINE_WORD_0); - return new_ternary(OP_ITE, SID_REGISTER_STATE, - is_compressed_instruction(c_ir_nid), - new_ternary(OP_ITE, SID_REGISTER_STATE, - new_binary_boolean(OP_NEQ, rd_nid, NID_ZR, "rd != register zero?"), - store_register_value(rd_nid, rd_value_nid, - "compressed instruction rd update", register_file_nid), - register_file_nid, - "compressed instruction register data flow"), - other_register_data_flow_nid, - "compressed instruction and other register data flow"); + if (REGISTER_FILE_ARRAY) + return new_ternary(OP_ITE, SID_REGISTER_STATE, + is_compressed_instruction(c_ir_nid), + new_ternary(OP_ITE, SID_REGISTER_STATE, + new_binary_boolean(OP_NEQ, rd_nid, NID_ZR, "rd != register zero?"), + store_register_value(SID_REGISTER_STATE, rd_nid, rd_value_nid, + "compressed instruction rd update", register_file_nid), + register_file_nid, + "compressed instruction register data flow"), + other_register_data_flow_nid, + "compressed instruction and other register data flow"); + else { + set_array_status_nid(other_register_data_flow_nid, + new_ternary(OP_ITE, SID_BOOLEAN, + is_compressed_instruction(c_ir_nid), + new_binary_boolean(OP_NEQ, rd_nid, NID_ZR, "rd != register zero?"), + get_array_status_nid(other_register_data_flow_nid), + "compressed instruction and other register data flow status")); + set_array_address_nid(other_register_data_flow_nid, + new_ternary(OP_ITE, SID_REGISTER_ADDRESS, + is_compressed_instruction(c_ir_nid), + rd_nid, + get_array_address_nid(other_register_data_flow_nid), + "compressed instruction and other register data flow address")); + set_array_value_nid(other_register_data_flow_nid, + new_ternary(OP_ITE, SID_MACHINE_WORD, + is_compressed_instruction(c_ir_nid), + rd_value_nid, + get_array_value_nid(other_register_data_flow_nid), + "compressed instruction and other register data flow value")); + + return other_register_data_flow_nid; + } } else return other_register_data_flow_nid; } @@ -10609,6 +10782,22 @@ uint64_t* core_compressed_memory_data_flow(uint64_t* c_ir_nid, return other_memory_data_flow_nid; } +uint64_t* compressed_branch_conditions(uint64_t* c_ir_nid, uint64_t* register_file_nid, char* comment, uint64_t* non_branching_nid) { + uint64_t* rs1_shift_value_nid; + + // only needed for controlling branching in bitme + + // TODO: avoid code duplication with compressed_branch_control_flow + + rs1_shift_value_nid = load_register_value(get_compressed_instruction_rs1_shift(c_ir_nid), "rs1' value", register_file_nid); + + return decode_compressed_branch(SID_BOOLEAN, c_ir_nid, + new_binary_boolean(OP_EQ, rs1_shift_value_nid, NID_MACHINE_WORD_0, "rs1' value == 0?"), + new_binary_boolean(OP_NEQ, rs1_shift_value_nid, NID_MACHINE_WORD_0, "rs1' value != 0?"), + comment, + non_branching_nid); +} + uint64_t* get_pc_value_plus_CB_offset(uint64_t* pc_nid, uint64_t* c_ir_nid) { return new_binary(OP_ADD, SID_MACHINE_WORD, pc_nid, @@ -10805,6 +10994,83 @@ uint64_t* state_property(uint64_t core, uint64_t* good_nid, uint64_t* bad_nid, c } } +uint64_t* kernel_register_data_flow(uint64_t* sid, uint64_t* ir_nid, + uint64_t* register_data_flow_nid, uint64_t* read_return_value_nid, uint64_t* register_file_nid) { + uint64_t* active_ecall_nid; + + uint64_t* a7_value_nid; + + uint64_t* brk_syscall_nid; + uint64_t* open_at_syscall_nid; + + uint64_t* read_syscall_nid; + uint64_t* write_syscall_nid; + + uint64_t* a2_value_nid; + + // system call ABI control flow + + active_ecall_nid = new_binary_boolean(OP_EQ, ir_nid, NID_ECALL_I, "ir == ECALL?"); + + a7_value_nid = load_register_value(NID_A7, "a7 value", register_file_nid); + + brk_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_BRK_SYSCALL_ID, "a7 == brk syscall ID?"); + open_at_syscall_nid = new_binary_boolean(OP_OR, + new_binary_boolean(OP_EQ, a7_value_nid, NID_OPENAT_SYSCALL_ID, "a7 == openat syscall ID?"), + new_binary_boolean(OP_EQ, a7_value_nid, NID_OPEN_SYSCALL_ID, "a7 == open syscall ID?"), + "a7 == openat or open syscall ID?"); + + read_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_READ_SYSCALL_ID, "a7 == read syscall ID?"); + write_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_WRITE_SYSCALL_ID, "a7 == write syscall ID?"); + + // system call ABI data flow + + a2_value_nid = load_register_value(NID_A2, "a2 value", register_file_nid); + + return new_ternary(OP_ITE, sid, + active_ecall_nid, + new_ternary(OP_ITE, sid, + brk_syscall_nid, + store_register_value(sid, + NID_A0, + cast_virtual_address_to_machine_word(eval_program_break_nid), + "store new program break in a0", + register_file_nid), + new_ternary(OP_ITE, sid, + open_at_syscall_nid, + store_register_value(sid, + NID_A0, + eval_file_descriptor_nid, + "store new file descriptor in a0", + register_file_nid), + new_ternary(OP_ITE, sid, + new_binary_boolean(OP_AND, + read_syscall_nid, + new_unary_boolean(OP_NOT, + eval_more_than_one_readable_byte_to_read_nid, + "read system call returns if there is at most one more byte to read"), + "update a0 when read system call returns"), + store_register_value(sid, + NID_A0, + read_return_value_nid, + "store read return value in a0", + register_file_nid), + new_ternary(OP_ITE, sid, + write_syscall_nid, + store_register_value(sid, + NID_A0, + a2_value_nid, + "store write return value in a0", + register_file_nid), + register_file_nid, + "write system call register data flow"), + "read system call register data flow"), + "openat system call register data flow"), + "brk system call register data flow"), + register_data_flow_nid, + "register data flow"); +} + void kernel_combinational(uint64_t core, uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* control_flow_nid, uint64_t* register_data_flow_nid, uint64_t* heap_segment_data_flow_nid, @@ -10816,14 +11082,9 @@ void kernel_combinational(uint64_t core, uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* a7_value_nid; uint64_t* exit_syscall_nid; - uint64_t* brk_syscall_nid; - uint64_t* open_at_syscall_nid; - uint64_t* read_syscall_nid; uint64_t* active_read_nid; - uint64_t* write_syscall_nid; - uint64_t* a0_value_nid; uint64_t* a2_value_nid; @@ -10843,18 +11104,10 @@ void kernel_combinational(uint64_t core, uint64_t* pc_nid, uint64_t* ir_nid, a7_value_nid = load_register_value(NID_A7, "a7 value", register_file_nid); - exit_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_EXIT_SYSCALL_ID, "a7 == exit syscall ID?"); - brk_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_BRK_SYSCALL_ID, "a7 == brk syscall ID?"); - open_at_syscall_nid = new_binary_boolean(OP_OR, - new_binary_boolean(OP_EQ, a7_value_nid, NID_OPENAT_SYSCALL_ID, "a7 == openat syscall ID?"), - new_binary_boolean(OP_EQ, a7_value_nid, NID_OPEN_SYSCALL_ID, "a7 == open syscall ID?"), - "a7 == openat or open syscall ID?"); - + exit_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_EXIT_SYSCALL_ID, "a7 == exit syscall ID?"); read_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_READ_SYSCALL_ID, "a7 == read syscall ID?"); active_read_nid = new_binary_boolean(OP_AND, active_ecall_nid, read_syscall_nid, "active read system call"); - write_syscall_nid = new_binary_boolean(OP_EQ, a7_value_nid, NID_WRITE_SYSCALL_ID, "a7 == write syscall ID?"); - // system call ABI data flow a0_value_nid = load_register_value(NID_A0, "a0 value", register_file_nid); @@ -10975,48 +11228,18 @@ void kernel_combinational(uint64_t core, uint64_t* pc_nid, uint64_t* ir_nid, // kernel and instruction register data flow - eval_register_data_flow_nid = new_ternary(OP_ITE, SID_REGISTER_STATE, - active_ecall_nid, - new_ternary(OP_ITE, SID_REGISTER_STATE, - brk_syscall_nid, - store_register_value( - NID_A0, - cast_virtual_address_to_machine_word(eval_program_break_nid), - "store new program break in a0", - register_file_nid), - new_ternary(OP_ITE, SID_REGISTER_STATE, - open_at_syscall_nid, - store_register_value( - NID_A0, - eval_file_descriptor_nid, - "store new file descriptor in a0", - register_file_nid), - new_ternary(OP_ITE, SID_REGISTER_STATE, - new_binary_boolean(OP_AND, - read_syscall_nid, - new_unary_boolean(OP_NOT, - eval_more_than_one_readable_byte_to_read_nid, - "read system call returns if there is at most one more byte to read"), - "update a0 when read system call returns"), - store_register_value( - NID_A0, - read_return_value_nid, - "store read return value in a0", - register_file_nid), - new_ternary(OP_ITE, SID_REGISTER_STATE, - write_syscall_nid, - store_register_value( - NID_A0, - a2_value_nid, - "store write return value in a0", - register_file_nid), - register_file_nid, - "write system call register data flow"), - "read system call register data flow"), - "openat system call register data flow"), - "brk system call register data flow"), - register_data_flow_nid, - "register data flow"); + if (REGISTER_FILE_ARRAY) + eval_register_data_flow_nid = kernel_register_data_flow(SID_REGISTER_STATE, ir_nid, + register_data_flow_nid, read_return_value_nid, register_file_nid); + else { + eval_register_data_flow_nid = allocate_array_nids(); + + set_array_status_nid(eval_register_data_flow_nid, kernel_register_data_flow(SID_BOOLEAN, ir_nid, + get_array_status_nid(register_data_flow_nid), read_return_value_nid, register_file_nid)); + set_array_address_nid(eval_register_data_flow_nid, NID_A0); // only a0 gets updated + set_array_value_nid(eval_register_data_flow_nid, kernel_register_data_flow(SID_MACHINE_WORD, ir_nid, + get_array_value_nid(register_data_flow_nid), read_return_value_nid, register_file_nid)); + } set_for(core, eval_register_data_flow_nids, eval_register_data_flow_nid); @@ -11429,6 +11652,25 @@ void rotor_combinational(uint64_t core, uint64_t* pc_nid, set_for(core, eval_instruction_control_flow_nids, instruction_control_flow_nid); + if (core == 0) { + // TODO: multicore support + if (RVC) { + branching_conditions_nid = new_ternary(OP_ITE, SID_BOOLEAN, + is_compressed_instruction(eval_ir_nid), + compressed_branch_conditions(eval_c_ir_nid, register_file_nid, "compressed true condition", NID_FALSE), + branch_conditions(eval_ir_nid, register_file_nid, "uncompressed true condition", NID_FALSE), + "branch true condition"); + non_branching_conditions_nid = new_ternary(OP_ITE, SID_BOOLEAN, + is_compressed_instruction(eval_ir_nid), + compressed_branch_conditions(eval_c_ir_nid, register_file_nid, "compressed false condition", NID_TRUE), + branch_conditions(eval_ir_nid, register_file_nid, "uncompressed false condition", NID_TRUE), + "branch false condition"); + } else { + branching_conditions_nid = branch_conditions(eval_ir_nid, register_file_nid, "true condition", NID_FALSE); + non_branching_conditions_nid = branch_conditions(eval_ir_nid, register_file_nid, "false condition", NID_TRUE); + } + } + // compressed and uncompressed instruction control flow eval_non_kernel_control_flow_nid = @@ -11557,8 +11799,7 @@ void rotor_sequential(uint64_t core, uint64_t* pc_nid, uint64_t* register_file_n next_nid = new_next(SID_REGISTER_STATE, get_for(0, state_register_file_nids), register_data_flow_nid, "register file"); } else - next_nid = new_next(SID_REGISTER_STATE, - register_file_nid, register_data_flow_nid, "register file"); + next_nid = new_register_file_next(register_file_nid, register_data_flow_nid, "register file"); set_for(core, next_register_file_nids, next_nid); set_for(core, sync_register_file_nids, sync_nid); @@ -11871,12 +12112,14 @@ void load_binary(uint64_t binary) { void model_rotor() { uint64_t core; - if (number_of_binaries > 0) - model_name = (char*) get_for(0, binary_names); - else if (IS64BITTARGET) - model_name = "64-bit-riscv-machine.m"; - else - model_name = "32-bit-riscv-machine.m"; + if (custom_model_name == 0) { + if (number_of_binaries > 0) + model_name = (char*) get_for(0, binary_names); + else if (IS64BITTARGET) + model_name = "64-bit-riscv-machine.m"; + else + model_name = "32-bit-riscv-machine.m"; + } number_of_lines = 0; @@ -11891,11 +12134,11 @@ void model_rotor() { init_model(); - init_interface_sorts(); - init_interface_kernel(); + init_machine_interface(); + init_kernel_interface(); init_register_file_sorts(); - init_memory_sorts(max_code_size, max_data_size); + init_memory_sorts(); init_kernels(number_of_cores); init_register_files(number_of_cores); @@ -11983,25 +12226,27 @@ void open_model_file() { uint64_t i; - if (number_of_binaries == number_of_cores) - suffix = "-rotorized"; - else - suffix = "-synthesize"; - - if (printing_unrolled_model) { - sprintf(string_buffer, "-kmin-%lu-kmax-%lu%s", - min_steps_to_bad_state - 1, - max_steps_to_bad_state - 1, - suffix); - suffix = string_copy(string_buffer); - } + if (custom_model_name == 0) { + if (number_of_binaries == number_of_cores) + suffix = "-rotorized"; + else + suffix = "-synthesize"; + + if (printing_unrolled_model) { + sprintf(string_buffer, "-kmin-%lu-kmax-%lu%s", + min_steps_to_bad_state - 1, + max_steps_to_bad_state - 1, + suffix); + suffix = string_copy(string_buffer); + } - if (printing_smt) - extension = "smt"; - else - extension = "btor2"; + if (printing_smt) + extension = "smt"; + else + extension = "btor2"; - model_name = replace_extension(model_name, suffix, extension); + model_name = replace_extension(model_name, suffix, extension); + } // assert: model_name is mapped and not longer than MAX_FILENAME_LENGTH @@ -12132,6 +12377,12 @@ void print_model_for(uint64_t core) { print_break_comment_line_for(core, "decode instruction", eval_instruction_ID_nids); print_break_comment_line_for(core, "decode compressed instruction", eval_compressed_instruction_ID_nids); + if (core == 0) { + // TODO: multicore support + print_break_line(branching_conditions_nid); + print_break_line(non_branching_conditions_nid); + } + print_break_comment_line_for(core, "instruction control flow", eval_instruction_control_flow_nids); if (RVC) print_break_comment_line_for(core, "compressed and uncompressed instruction control flow", @@ -12250,8 +12501,8 @@ void print_model() { last_nid = 0; - print_interface_sorts(); - print_interface_kernel(); + print_machine_interface(); + print_kernel_interface(); print_register_sorts(); print_memory_sorts(); @@ -13303,7 +13554,18 @@ void print_unrolled_model() { // ----------------------------------------------------------------- uint64_t parse_engine_arguments() { - if (string_compare(peek_argument(1), evaluate_model_option)) { + if (string_compare(peek_argument(1), custom_model_name_option)) { + custom_model_name = 1; + + get_argument(); + + if (number_of_remaining_arguments() > 1) { + model_name = peek_argument(1); + + get_argument(); + } else + return EXITCODE_BADARGUMENTS; + } else if (string_compare(peek_argument(1), evaluate_model_option)) { evaluate_model = 1; get_argument();