diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-01 00:17:26 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-01 00:17:26 -0700 |
commit | 49d8141bb9d7c59bd3e1ad70d524fecc9f6dda7e (patch) | |
tree | 65665890f6e69be24ec8705e21897a4924037b2d | |
parent | 6fa0aec445f9801aa5e0ff42c72f7e852b6a5b28 (diff) |
Update
-rwxr-xr-x | src/theory/rewriter/compiler.py | 172 | ||||
-rw-r--r-- | src/theory/rewriter/node.py | 56 | ||||
-rw-r--r-- | src/theory/rewriter/parser.py | 19 | ||||
-rw-r--r-- | src/theory/rewriter/rules/basic.rules | 79 |
4 files changed, 246 insertions, 80 deletions
diff --git a/src/theory/rewriter/compiler.py b/src/theory/rewriter/compiler.py index 20e34f7b1..0e8e98315 100755 --- a/src/theory/rewriter/compiler.py +++ b/src/theory/rewriter/compiler.py @@ -32,6 +32,8 @@ op_to_kind = { Op.BVUREM: 'BITVECTOR_UREM_TOTAL', Op.BVSMOD: 'BITVECTOR_SMOD', Op.BVSHL: 'BITVECTOR_SHL', + Op.BVLSHR: 'BITVECTOR_LSHR', + Op.BVASHR: 'BITVECTOR_ASHR', Op.ROTATE_LEFT: 'BITVECTOR_ROTATE_LEFT', Op.ROTATE_RIGHT: 'BITVECTOR_ROTATE_RIGHT', Op.BVNOT: 'BITVECTOR_NOT', @@ -58,11 +60,14 @@ op_to_kind = { op_to_const_eval = { Op.BVSHL: '({}.leftShift({}))', + Op.EXTRACT: '({2}.extract({0}, {1}))', Op.BVNOT: '(~{})', Op.PLUS: '({} + {})', Op.MINUS: '({} - {})', + Op.LT: '({} < {})', Op.GEQ: '({} >= {})', Op.NOT: '(!{})', + Op.AND: '({} && {})', Op.EQ: '({} == {})', } @@ -104,6 +109,8 @@ op_to_nindex = { Op.BVUREM: 0, Op.BVSMOD: 0, Op.BVSHL: 0, + Op.BVLSHR: 0, + Op.BVASHR: 0, Op.ROTATE_LEFT: 1, Op.ROTATE_RIGHT: 1, Op.BVNOT: 0, @@ -140,11 +147,16 @@ def mk_simple_block(cfg, next_block, instr): def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): - def expr_to_ir(const_checks, next_block, expr, node, vars_seen, in_loop=False): + def expr_to_ir(const_checks, + next_block, + expr, + node, + vars_seen, + in_loop=False): if isinstance(expr, Var): if expr.name in vars_seen: - return mk_simple_block(cfg, next_block, - Assert(Fn(Op.EQ, [expr, node]), in_loop)) + return mk_simple_block( + cfg, next_block, Assert(Fn(Op.EQ, [expr, node]), in_loop)) else: if expr.sort is not None and expr.sort.base == BaseSort.BitVec: width = expr.sort.children[0] @@ -164,20 +176,41 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): elif expr.sort.const: if isinstance(expr, Fn) and expr.op == Op.BVCONST: - # bvval = + # bvval = # next_block = mk_simple_block( # cfg, next_block, # Assert( # Fn(Op.EQ, # [Fn(Op.GET_KIND, [node]), # KindConst(expr.op)]), in_loop)) - return mk_simple_block( + + if isinstance(expr.children[0], + Var) and expr.children[0] not in vars_seen: + next_block = mk_simple_block( + cfg, next_block, + Assign(expr.children[0], Fn(Op.BV_SIZE, [node]))) + + next_block = expr_to_ir(const_checks, next_block, + expr.children[0], + Fn(Op.BV_SIZE, + [node]), vars_seen, in_loop) + + if isinstance(expr.children[1], + Var) and expr.children[1] not in vars_seen: + next_block = expr_to_ir(const_checks, next_block, + expr.children[1], + Fn(Op.BV_SIZE, + [node]), vars_seen, in_loop) + + next_block = mk_simple_block( cfg, next_block, Assert( Fn(Op.EQ, [Fn(Op.GET_KIND, [node]), KindConst(expr.op)]), in_loop)) + return next_block + # TODO: node.sort should not be None instr = None if node.sort and node.sort.const: @@ -185,19 +218,27 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): else: instr = Fn(Op.EQ, [node, Fn(Op.MK_CONST, [expr])]) - return mk_simple_block( - cfg, next_block, - Assert(instr, in_loop)) + return mk_simple_block(cfg, next_block, Assert(instr, in_loop)) elif isinstance(expr, Fn): if expr.op in commutative_ops: - nlist_children = [child for child in expr.children if child.sort.base != BaseSort.List] - loop_idxs = [Var(fresh_name('loopi'), Sort(BaseSort.Int, [], True)) for _ in nlist_children] + nlist_children = [ + child for child in expr.children + if child.sort.base != BaseSort.List + ] + loop_idxs = [ + Var(fresh_name('loopi'), Sort(BaseSort.Int, [], True)) + for _ in nlist_children + ] # Assign the remainder of the list if len(nlist_children) != len(expr.children): - list_child = next(child for child in expr.children if child.sort.base == BaseSort.List) - next_block = mk_simple_block(cfg, next_block, Assign(list_child, Fn(Op.GET_CHILDREN, [node] + loop_idxs))) + list_child = next(child for child in expr.children + if child.sort.base == BaseSort.List) + next_block = mk_simple_block( + cfg, next_block, + Assign(list_child, + Fn(Op.GET_CHILDREN, [node] + loop_idxs))) for i, child in reversed(list(enumerate(nlist_children))): sub_expr_vars_seen = vars_seen.copy() @@ -205,18 +246,22 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): sub_expr_vars_seen |= collect_vars(child2) loop_idx = loop_idxs[i] - loop_var = Var(fresh_name('loopv'), child.sort) - next_block = expr_to_ir(const_checks, next_block, child, loop_var, sub_expr_vars_seen, True) - next_block = mk_simple_block(cfg, next_block, Assign(loop_var, Fn( - Op.GET_CHILD, - [node, loop_idx]))) + loop_var_sort = Sort(child.sort.base, child.sort.children) + loop_var = Var(fresh_name('loopv'), loop_var_sort) + next_block = expr_to_ir(const_checks, next_block, child, + loop_var, sub_expr_vars_seen, True) + next_block = mk_simple_block( + cfg, next_block, + Assign(loop_var, Fn(Op.GET_CHILD, [node, loop_idx]))) for j in range(i): - check = Fn(Op.NOT, [Fn(Op.EQ, [loop_idx, loop_idxs[j]])]) + check = Fn(Op.NOT, + [Fn(Op.EQ, [loop_idx, loop_idxs[j]])]) # Use infer types check.sort = Sort(BaseSort.Bool, [], True) check.children[0].sort = Sort(BaseSort.Bool, [], True) - next_block = mk_simple_block(cfg, next_block, Assert(check, True)) + next_block = mk_simple_block(cfg, next_block, + Assert(check, True)) loop_block = fresh_name('loop') cfg[loop_block] = CFGLoop(loop_idx, node, next_block) @@ -234,17 +279,16 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): else: child_node = Fn( Op.GET_CHILD, - [node, - IntConst(i - op_to_nindex[expr.op])]) - next_block = expr_to_ir(const_checks, next_block, child, child_node, - sub_expr_vars_seen, in_loop) + [node, IntConst(i - op_to_nindex[expr.op])]) + next_block = expr_to_ir(const_checks, next_block, child, + child_node, sub_expr_vars_seen, + in_loop) return mk_simple_block( cfg, next_block, Assert( - Fn(Op.EQ, - [Fn(Op.GET_KIND, [node]), - KindConst(expr.op)]), in_loop)) + Fn(Op.EQ, [Fn(Op.GET_KIND, [node]), + KindConst(expr.op)]), in_loop)) elif isinstance(expr, BVConst): assert False @@ -269,9 +313,10 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs): vars_seen = set() const_check_block = fresh_name('block') const_checks = [] - entry = expr_to_ir(const_checks, const_check_block, lhs, node_var, vars_seen) + entry = expr_to_ir(const_checks, const_check_block, lhs, node_var, + vars_seen) cfg[const_check_block] = CFGNode(const_checks, - [CFGEdge(BoolConst(True), out_block)]) + [CFGEdge(BoolConst(True), out_block)]) return entry @@ -298,16 +343,19 @@ def rule_to_out_expr(cfg, next_block, res, expr): cfg[cond_block] = CFGNode([], edges) return cond_block elif expr.op == Op.FAIL: - return mk_simple_block(cfg, next_block, Assert(BoolConst(False), False)) + return mk_simple_block(cfg, next_block, + Assert(BoolConst(False), False)) elif expr.op == Op.LET: next_block = rule_to_out_expr(cfg, next_block, res, expr.children[2]) - next_block = rule_to_out_expr(cfg, next_block, expr.children[0], + next_block = rule_to_out_expr(cfg, next_block, + expr.children[0], expr.children[1]) return next_block elif expr.op == Op.BVCONST: new_vars = [ - Var(fresh_name('__v'), child.sort) for child in expr.children + Var(fresh_name('__v'), child.sort) + for child in expr.children ] bvc = Fn(Op.BVCONST, new_vars) bvc.sort = expr.sort @@ -330,14 +378,18 @@ def rule_to_out_expr(cfg, next_block, res, expr): return next_block else: new_vars = [ - Var(fresh_name('__v'), child.sort) for child in expr.children + Var(fresh_name('__v'), child.sort) + for child in expr.children ] assign = None if expr.sort.const: fn = Fn(expr.op, new_vars) fn.sort = expr.sort - assign = Assign(res, fn) + if res.sort and res.sort.const: + assign = Assign(res, fn) + else: + assign = Assign(res, Fn(Op.MK_CONST, [fn])) else: # If we have a non-constant expression with constant arguments, # we have to cast the constant arguments to terms @@ -347,6 +399,7 @@ def rule_to_out_expr(cfg, next_block, res, expr): new_args.append(Fn(Op.MK_CONST, [new_var])) else: new_args.append(new_var) + assign = Assign( res, Fn(Op.MK_NODE, [KindConst(expr.op)] + new_args)) @@ -366,8 +419,8 @@ def rule_to_out_expr(cfg, next_block, res, expr): res.sort = Sort(BaseSort.Bool, []) assign = Assign(res, expr) if next_block: - cfg[assign_block] = CFGNode([assign], - [CFGEdge(BoolConst(True), next_block)]) + cfg[assign_block] = CFGNode( + [assign], [CFGEdge(BoolConst(True), next_block)]) else: assign.expr = Fn(Op.MK_CONST, [assign.expr]) cfg[assign_block] = CFGNode([assign], []) @@ -377,8 +430,8 @@ def rule_to_out_expr(cfg, next_block, res, expr): res.sort = Sort(BaseSort.Int, [], True) assign = Assign(res, expr) if next_block: - cfg[assign_block] = CFGNode([assign], - [CFGEdge(BoolConst(True), next_block)]) + cfg[assign_block] = CFGNode( + [assign], [CFGEdge(BoolConst(True), next_block)]) else: cfg[assign_block] = CFGNode([assign], []) return assign_block @@ -387,8 +440,8 @@ def rule_to_out_expr(cfg, next_block, res, expr): assign = Assign(res, expr) res.sort = expr.sort if next_block: - cfg[assign_block] = CFGNode([assign], - [CFGEdge(BoolConst(True), next_block)]) + cfg[assign_block] = CFGNode( + [assign], [CFGEdge(BoolConst(True), next_block)]) else: cfg[assign_block] = CFGNode([assign], []) return assign_block @@ -414,16 +467,38 @@ def expr_to_code(expr): return 'nm->mkConst({})'.format(', '.join(args)) elif expr.op == Op.MK_NODE: kind = expr.children[0].val - if op_to_nindex[kind] != 0: - op = 'bv::utils::mkIndexedOp({})'.format(', '.join(args[:op_to_nindex[kind] + 1])) - return 'nm->mkNode({})'.format(', '.join([op] + args[op_to_nindex[kind] + 1:])) + + list_arg = None + for child in expr.children: + if child.sort and child.sort.base == BaseSort.List: + list_arg = child.sort + break + + arg_str = None + if list_arg: + vec = fresh_name('__vec') + arg_str = '{}, '.format(args[0]) + arg_str += '[&](){{ std::vector<Node> {0}; {1}; return {0}; }}()'.format( + vec, ';'.join( + ('{}.push_back({})'.format(vec, arg) + if child.sort and child.sort.base != BaseSort.List + else '{0}.insert({0}.end(), {1}.begin(), {1}.end())'. + format(vec, arg)) + for arg, child in zip(args[1:], expr.children[1:]))) + elif op_to_nindex[kind] != 0: + op = 'bv::utils::mkIndexedOp({})'.format(', '.join( + args[:op_to_nindex[kind] + 1])) + arg_str = ', '.join([op] + args[op_to_nindex[kind] + 1:]) else: - return 'nm->mkNode({})'.format(', '.join(args)) + arg_str = ', '.join(args) + + return 'nm->mkNode({})'.format(arg_str) elif expr.op == Op.GET_CHILD: return '{}[{}]'.format(args[0], args[1]) elif expr.op == Op.GET_CHILDREN: cond = ' && '.join('i != {}'.format(arg) for arg in args[1:]) - return 'bv::utils::getChildren({}, [&](size_t i) {{ return {}; }})'.format(args[0], cond) + return 'bv::utils::getChildren({}, [&](size_t i) {{ return {}; }})'.format( + args[0], cond) elif expr.op == Op.GET_INDEX: return 'bv::utils::getIndex({}, {})'.format(args[0], args[1]) elif expr.sort and expr.sort.const: @@ -465,9 +540,8 @@ def ir_to_code(match_instrs): expr_to_code(instr.expr))) elif isinstance(instr, Assert): exit = 'continue' if instr.in_loop else 'return RewriteResponse(REWRITE_DONE, __node, RewriteRule::NONE)' - code.append( - 'if (!({})) {};' - .format(expr_to_code(instr.expr), exit)) + code.append('if (!({})) {};'.format(expr_to_code(instr.expr), + exit)) return '\n'.join(code) @@ -478,7 +552,9 @@ def cfg_to_code(block, cfg): return """ for ({} = 0; {} < {}.getNumChildren(); {}++) {{ {} - }}""".format(cfg[block].loop_var, cfg[block].loop_var, cfg[block].domain, cfg[block].loop_var, body) + }}""".format(cfg[block].loop_var, cfg[block].loop_var, + expr_to_code(cfg[block].domain), cfg[block].loop_var, + body) else: result = ir_to_code(cfg[block].instrs) first_edge = True diff --git a/src/theory/rewriter/node.py b/src/theory/rewriter/node.py index 8a69b3896..09ccd47ac 100644 --- a/src/theory/rewriter/node.py +++ b/src/theory/rewriter/node.py @@ -31,6 +31,8 @@ class Op(Enum): # Bit-vector shifts BVSHL = auto() + BVLSHR = auto() + BVASHR = auto() ROTATE_LEFT = auto() ROTATE_RIGHT = auto() @@ -69,6 +71,7 @@ class Op(Enum): PLUS = auto() MINUS = auto() MULT = auto() + LT = auto() GEQ = auto() ########################################################################### @@ -89,6 +92,7 @@ class Op(Enum): MK_NODE = auto() MK_CONST = auto() BV_SIZE = auto() + APPEND = auto() ########################################################################### # Language operators @@ -102,8 +106,9 @@ class Op(Enum): LET = auto() FAIL = auto() -commutative_ops = set([Op.AND, Op.XOR, Op.EQ]) -nary_ops = set([Op.AND]) + +commutative_ops = set([Op.BVADD, Op.BVXOR, Op.AND, Op.XOR, Op.EQ]) +nary_ops = set([Op.BVADD, Op.AND]) class BaseSort(Enum): @@ -247,9 +252,8 @@ class Sort(Node): def __repr__(self): return '({} {}{})'.format( - self.base, ' '.join( - str(child) - for child in self.children), ' :const' if self.const else '') + self.base, ' '.join(str(child) for child in self.children), + ' :const' if self.const else '') def collect_vars(node): @@ -294,6 +298,16 @@ def unify_types(t1, t2): return t1 +def are_types_compatible(t1, t2): + if t1.base == t2.base: + return True + if t1.base == BaseSort.List: + return are_types_compatible(t1.children[0], t2) + elif t2.base == BaseSort.List: + return are_types_compatible(t1, t2.children[0]) + return False + + def infer_types(context, node): if node.sort: return @@ -323,14 +337,21 @@ def infer_types(context, node): assert node.children[0].sort.base == BaseSort.BitVec assert node.children[0].sort == node.children[1].sort sort = Sort(BaseSort.Bool, []) - elif node.op in [ - Op.BVREDAND, Op.BVREDOR - ]: + elif node.op in [Op.BVREDAND, Op.BVREDOR]: assert node.children[0].sort.base == BaseSort.BitVec sort = Sort(BaseSort.Bool, []) - elif node.op in [Op.BVADD, Op.BVSUB, Op.BVSDIV, Op.BVUDIV, Op.BVSREM, Op.BVUREM, Op.BVSMOD, Op.BVSHL, Op.BVAND, Op.BVOR, Op.BVXOR, Op.BVNAND, Op.BVNOR, Op.BVXNOR]: - assert node.children[0].sort.base == BaseSort.BitVec - assert node.children[0].sort == node.children[1].sort + elif node.op in [ + Op.BVADD, Op.BVSUB, Op.BVSDIV, Op.BVUDIV, Op.BVSREM, Op.BVUREM, + Op.BVSMOD, Op.BVSHL, Op.BVLSHR, Op.BVASHR, Op.BVAND, Op.BVOR, + Op.BVXOR, Op.BVNAND, Op.BVNOR, Op.BVXNOR + ]: + assert node.children[0].sort.base == BaseSort.BitVec or ( + node.children[0].sort.base == BaseSort.List + and node.children[0].sort.children[0].base == BaseSort.BitVec) + arg_sort = node.children[0].sort + assert all( + are_types_compatible(arg_sort, child.sort) + for child in node.children) sort = Sort(BaseSort.BitVec, [node.children[0].sort.children[0]]) elif node.op in [Op.ROTATE_LEFT, Op.ROTATE_RIGHT]: assert node.children[0].sort.base == BaseSort.Int @@ -367,8 +388,10 @@ def infer_types(context, node): assert node.children[1].sort.base == BaseSort.Int assert node.children[2].sort.base == BaseSort.BitVec sort = Sort(BaseSort.BitVec, [ - Fn(Op.PLUS, [Fn(Op.MINUS, - [node.children[0], node.children[1]]), IntConst(1)]) + Fn(Op.PLUS, [ + Fn(Op.MINUS, [node.children[0], node.children[1]]), + IntConst(1) + ]) ]) elif node.op in [Op.BVNEG, Op.BVNOT]: assert node.children[0].sort.base == BaseSort.BitVec @@ -410,7 +433,7 @@ def infer_types(context, node): assert node.children[0].sort.base == BaseSort.Int assert node.children[1].sort.base == BaseSort.Int sort = Sort(BaseSort.Int, []) - elif node.op in [Op.GEQ]: + elif node.op in [Op.LT, Op.GEQ]: assert node.children[0].sort.base == BaseSort.Int assert node.children[1].sort.base == BaseSort.Int sort = Sort(BaseSort.Bool, []) @@ -419,7 +442,10 @@ def infer_types(context, node): assert node.children[1].sort.base == BaseSort.Bool sort = Sort(BaseSort.Bool, []) elif node.op in [Op.AND]: - assert all(child.sort.base == BaseSort.Bool or (child.sort.base == BaseSort.List and child.sort.children[0].base == BaseSort.Bool) for child in node.children) + assert all(child.sort.base == BaseSort.Bool or ( + child.sort.base == BaseSort.List + and child.sort.children[0].base == BaseSort.Bool) + for child in node.children) # TODO: Check that list is used correctly sort = Sort(BaseSort.Bool, []) elif node.op == Op.FAIL: diff --git a/src/theory/rewriter/parser.py b/src/theory/rewriter/parser.py index f6a4673de..7bfeeb5f4 100644 --- a/src/theory/rewriter/parser.py +++ b/src/theory/rewriter/parser.py @@ -23,6 +23,8 @@ symbol_to_op = { 'bvurem': Op.BVUREM, 'bvsmod': Op.BVSMOD, 'bvshl': Op.BVSHL, + 'bvlshr': Op.BVLSHR, + 'bvashr': Op.BVASHR, 'rotate_left': Op.ROTATE_LEFT, 'rotate_right': Op.ROTATE_RIGHT, 'bvnot': Op.BVNOT, @@ -45,6 +47,7 @@ symbol_to_op = { 'xor': Op.XOR, '+': Op.PLUS, '-': Op.MINUS, + '<': Op.LT, '>=': Op.GEQ, '=': Op.EQ, 'ite': Op.ITE, @@ -60,14 +63,16 @@ def symbol(): special_chars = '=' + '_' + '+' + '-' + '<' + '>' return pp.Word(pp.alphas + special_chars, pp.alphanums + special_chars) + def mk_let(let): body = let[-1] for binding in reversed(let[0:-1]): body = Fn(Op.LET, [binding[0], binding[1], body]) return body + def mk_case(cases): - if cases[-1].op != Op.CASE: + if not isinstance(cases[-1], Fn) or cases[-1].op != Op.CASE: cases[-1] = Fn(Op.CASE, [BoolConst(True), cases[-1]]) else: cases.append(Fn(Op.CASE, [BoolConst(True), Fn(Op.FAIL, [])])) @@ -99,11 +104,11 @@ def expr(): ).setParseAction(lambda s, l, t: Fn(symbol_to_op[t[0]], t[1:])) # Let bindings - binding = (pp.Suppress('(') + var + expr + pp.Suppress(')') - ).setParseAction(lambda s, l, t: (t[0], t[1])) + binding = (pp.Suppress('(') + var + expr + + pp.Suppress(')')).setParseAction(lambda s, l, t: (t[0], t[1])) let = (pp.Suppress('(') + pp.Keyword('let') + pp.Suppress('(') + - pp.OneOrMore(binding) + pp.Suppress(')') + expr + pp.Suppress(')') - ).setParseAction(lambda s, l, t: mk_let(t[1:])) + pp.OneOrMore(binding) + pp.Suppress(')') + expr + + pp.Suppress(')')).setParseAction(lambda s, l, t: mk_let(t[1:])) # Conditionals case = (pp.Suppress('(') + expr + expr + pp.Suppress(')') @@ -139,9 +144,11 @@ def process_var_decl(name, sort, attrs): def attrs(): return pp.Keyword(':list') | pp.Keyword(':const') + def var_decl(): return (pp.Suppress('(') + symbol() + sort() + pp.ZeroOrMore(attrs()) + - pp.Suppress(')')).setParseAction(lambda s, l, t: process_var_decl(t[0], t[1], t[2:])) + pp.Suppress(')')).setParseAction( + lambda s, l, t: process_var_decl(t[0], t[1], t[2:])) def var_list(): diff --git a/src/theory/rewriter/rules/basic.rules b/src/theory/rewriter/rules/basic.rules index 19a712c97..0d39f8050 100644 --- a/src/theory/rewriter/rules/basic.rules +++ b/src/theory/rewriter/rules/basic.rules @@ -31,6 +31,13 @@ ((_ extract i j) (bvnot x)) (bvnot ((_ extract i j) x))) +(define-rule ExtractSignExtend ((i Int :const) (j Int :const) (k Int :const) (n Int :const) (x (_ BitVec n))) + ((_ extract i j) ((_ sign_extend k) x)) + (cond + ((< i n) ((_ extract i j) x)) + ((and (< j n) (>= i n)) ((_ sign_extend (+ (- i n) 1)) ((_ extract (- n 1) j) x))) + (true ((_ repeat (+ (- i j) 1)) ((_ extract (- n 1) (- n 1)) x))))) + /****************************************************************************** * Operator Elimination ******************************************************************************/ @@ -167,25 +174,21 @@ * Simplification ******************************************************************************/ -/* (define-rule BvIteConstCond ((m Int :const) (x (_ BitVec n)) (y (_ BitVec n))) (bvite (_ bv m 1) x y) (cond ((= m 1) x) y)) -*/ (define-rule BvIteEqualChildren ((c (_ BitVec 1)) (x (_ BitVec m))) (bvite c x x) x) -/* -(define-rule BvIteConstChildren ((n Int) (m Int) (x (_ BitVec o))) +(define-rule BvIteConstChildren ((n Int :const) (m Int :const) (x (_ BitVec o))) (bvite x (_ bv n 1) (_ bv m 1)) (cond ((and (= n 1) (= m 0)) x) - (bvnot x))) -*/ + (true (bvnot x)))) (define-rule BvIteEqualCondThen ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n))) (bvite c (bvite c x y) z) @@ -211,10 +214,11 @@ (bvite c0 x (bvite c1 y x)) (bvite (bvand (bvnot c0) c1) y x)) -/* -(define-rule BvComp ((n Int) (x (_ BitVec 1))) +(define-rule BvComp ((n Int :const) (x (_ BitVec 1))) (bvcomp (_ bv n 1) x) - (ite (= n 0) (bvnot x) x)) + (cond + ((= n 0) (bvnot x)) + x)) (define-rule ShlByConst ((n Int :const) (m Int :const) (x (_ BitVec m))) (bvshl x (_ bv n m)) @@ -222,13 +226,20 @@ ((= n 0) x) ((>= n m) (_ bv 0 m)) (concat ((_ extract (- m (+ n 1)) 0) x) (_ bv 0 n)))) -*/ /* +(define-rule XorOne ((n Int :const) (xs (_ BitVec n) :list)) + (bvxor (bvnot (_ bv 0 n)) xs) + (bvxor xs)) +*/ + +(define-rule XorZero ((n Int :const) (xs (_ BitVec n) :list)) + (bvxor (_ bv 0 n) xs) + (bvxor xs)) + (define-rule NotXor ((x (_ BitVec n)) (xs (_ BitVec n) :list)) (bvnot (bvxor x xs)) (bvxor (bvnot x) xs)) -*/ (define-rule NotIdemp ((x (_ BitVec n))) (bvnot (bvnot x)) @@ -250,11 +261,31 @@ (bvsle x x) true) +(define-rule ZeroUlt ((n Int :const) (x (_ BitVec n))) + (bvult (_ bv 0 n) x) + (not (= (_ bv 0 n) x))) + +(define-rule UltZero ((n Int :const) (x (_ BitVec n))) + (bvult x (_ bv 0 n)) + false) + +(define-rule UltOne ((n Int :const) (x (_ BitVec n))) + (bvult x (_ bv 1 n)) + (= x (_ bv 0 n))) + +(define-rule SltZero ((n Int :const) (x (_ BitVec n))) + (bvslt x (_ bv 0 n)) + (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1))) + /* Note: Duplicate of LtSelfUlt */ (define-rule UltSelf ((x (_ BitVec n))) (bvult x x) false) +(define-rule UleZero ((n Int :const) (x (_ BitVec n))) + (bvule x (_ bv 0 n)) + (= x (_ bv 0 n))) + /* Note: Duplicate of LteSelfUle */ (define-rule UleSelf ((x (_ BitVec n))) (bvule x x) @@ -290,10 +321,26 @@ (bvudiv x (_ bv 1 n)) x) +(define-rule UremOne ((n Int :const) (x (_ BitVec n))) + (bvudiv x (_ bv 1 n)) + (_ bv 0 n)) + (define-rule UremSelf ((n Int :const) (x (_ BitVec n))) (bvudiv x x) (_ bv 0 n)) +(define-rule ShiftZeroShl ((n Int :const) (x (_ BitVec n))) + (bvshl (_ bv 0 n) x) + (_ bv 0 n)) + +(define-rule ShiftZeroLshr ((n Int :const) (x (_ BitVec n))) + (bvlshr (_ bv 0 n) x) + (_ bv 0 n)) + +(define-rule ShiftZeroAshr ((n Int :const) (x (_ BitVec n))) + (bvashr (_ bv 0 n) x) + (_ bv 0 n)) + (define-rule MergeSignExtendSign ((i Int :const) (j Int :const) (n Int :const) (x (_ BitVec n))) ((_ sign_extend i) ((_ sign_extend j) x)) ((_ sign_extend (+ i j)) x)) @@ -304,6 +351,16 @@ ((= j 0) ((_ sign_extend i) x)) (true ((_ zero_extend (+ i j)) x)))) +(define-rule ZeroExtendEqConst ((i Int :const) (n Int :const) (m Int :const) (x (_ BitVec n))) + (= ((_ zero_extend i) x) (_ bv m n)) + (cond + ((= ((_ extract (- (+ n m) 1) n) (_ bv m n)) (_ bv 0 n)) (= x ((_ extract (- n 1) 0) (_ bv m n)))) + false)) + +(define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n))) + (bvult x (bvadd y (_ bv 1 n))) + (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n)))))) + /****************************************************************************** * Experimental ******************************************************************************/ |