Replace self-jmp in SPARC RzIL (#6632)

To perform the effect in a delay slot, if the branch was not taken, the
IL, which is already lifted as part of the delay slot instruction, would
explicitly jump to itself again, to execute the effect as normal.
This would create erroneous loop edges in the cfg.
It is actually not necessary to perform this jmp since we already have
the lifted effect and can inline it.
This commit is contained in:
Florian Märkl 2026-07-23 14:57:14 +02:00 committed by GitHub
parent e49ce34306
commit 3a22989501
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 129 additions and 125 deletions

View file

@ -139,11 +139,6 @@ typedef enum {
typedef struct {
RzILOpEffect *set_ea; ///< The RzIL Effect to write the target jump address to the local variable EA.
RzILOpEffect *perform_jmp; ///< The RzIL Effect to performing the jump to EA.
/**
* \brief The RzIL Effect to performing the jump if the branch condition is false.
* Might be NULL if no condition exists.
*/
RzILOpEffect *perform_fail_jmp;
RzILOpPure *cond; ///< The branch condition. NULL if branch has none.
bool annulled_bit; ///< The annulled bit.
} RzSparcDelatedBranchOp;

View file

@ -1816,7 +1816,6 @@ static inline void set_delayed_slot(HtUP *dl_table,
ut64 address,
RzILOpEffect *set_ea,
RzILOpEffect *jmp,
RZ_NULLABLE RzILOpEffect *fail_jmp,
RZ_NULLABLE RzILOpPure *cond,
bool annulled_bit) {
bool found;
@ -1829,14 +1828,12 @@ static inline void set_delayed_slot(HtUP *dl_table,
if (found) {
// Faulty disassembly or same address disassembled again.
rz_il_op_pure_free(eff->cond);
rz_il_op_effect_free(eff->perform_fail_jmp);
rz_il_op_effect_free(eff->perform_jmp);
rz_il_op_effect_free(eff->set_ea);
free(eff);
}
bop->cond = cond;
bop->annulled_bit = annulled_bit;
bop->perform_fail_jmp = fail_jmp;
bop->perform_jmp = jmp;
bop->set_ea = set_ea;
ht_up_update(dl_table, address, bop);
@ -1852,12 +1849,12 @@ static RzILOpEffect *branch_op(const csh handle, const cs_insn *insn, const cs_m
case SPARC_INS_JMPL: {
const char *link_reg = cs_reg_name(handle, INSOP(1).reg);
RzILOpPure *ea = rz_sparc_cs_get_operand(handle, insn, mode, 0, 0);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), NULL, NULL, false);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), NULL, false);
return SSETG(link_reg, UA(insn->address));
}
case SPARC_INS_CALL: {
RzILOpPure *ea = rz_sparc_cs_get_operand(handle, insn, mode, 0, 0);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), NULL, NULL, false);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), NULL, false);
return SETG("o7", UA(insn->address));
}
case SPARC_INS_B:
@ -1873,8 +1870,7 @@ static RzILOpEffect *branch_op(const csh handle, const cs_insn *insn, const cs_m
rz_il_op_pure_free(ea);
return NULL;
}
ut64 failed_addr = annul_delay_slot ? insn->address + (SPARC_INSN_SIZE * 2) : insn->address + SPARC_INSN_SIZE;
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), JMP(UA(failed_addr)), cond, annul_delay_slot);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, SETL("EA", CAST_UA(ea)), JMP(VARL("EA")), cond, annul_delay_slot);
return NOP();
}
case SPARC_INS_RETT: {
@ -1886,7 +1882,7 @@ static RzILOpEffect *branch_op(const csh handle, const cs_insn *insn, const cs_m
// The window_underflow/window_overflow cases are not handled here.
// Because Rizin doesn't model traps for now.
RzILOpPure *ea = rz_sparc_cs_get_operand(handle, insn, mode, 0, 0);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, EMPTY(), JMP(VARG("tnpc")), NULL, NULL, false);
set_delayed_slot(state->delayed_branch, insn->address + SPARC_INSN_SIZE, EMPTY(), JMP(VARG("tnpc")), NULL, false);
RzILOpEffect *restore = restore_op(handle, insn, mode);
return SEQ2(SETG("tnpc", CAST_UA(ea)), restore);
}

View file

@ -173,10 +173,24 @@ static int analyze_op(RzAnalysis *a, RzAnalysisOp *op, ut64 addr, const ut8 *buf
op->il_op = rz_il_op_new_empty();
}
if (op->il_op && delayed_branch->cond) {
// The branch is conditionally and annuls the delay slot if not taken (skips op->il_op).
op->il_op = rz_il_op_new_branch(delayed_branch->cond,
rz_il_op_new_seq(delayed_branch->set_ea, rz_il_op_new_seq(op->il_op, delayed_branch->perform_jmp)),
delayed_branch->perform_fail_jmp);
// The branch is conditional and optionally annuls the delay slot if not taken (skips op->il_op).
// clang-format off
if (delayed_branch->annulled_bit) {
op->il_op = rz_il_op_new_branch(delayed_branch->cond,
rz_il_op_new_seq(
delayed_branch->set_ea, rz_il_op_new_seq(
op->il_op,
delayed_branch->perform_jmp)),
rz_il_op_new_nop());
} else {
op->il_op = rz_il_op_new_seq(
delayed_branch->set_ea, rz_il_op_new_seq(
op->il_op,
rz_il_op_new_branch(delayed_branch->cond,
delayed_branch->perform_jmp,
rz_il_op_new_nop())));
}
// clang-format on
} else if (op->il_op) {
op->il_op = rz_il_op_new_seq(delayed_branch->set_ea, rz_il_op_new_seq(op->il_op, delayed_branch->perform_jmp));
}
@ -756,7 +770,6 @@ static bool sparc_fini(void *user) {
RzIterator *iter = ht_up_as_iter(sparc->delayed_branch);
RzSparcDelatedBranchOp **eff;
rz_iterator_foreach(iter, eff) {
rz_il_op_effect_free((*eff)->perform_fail_jmp);
rz_il_op_effect_free((*eff)->perform_jmp);
rz_il_op_effect_free((*eff)->set_ea);
free(*eff);

View file

@ -31,22 +31,22 @@ dE "jmpl g1, g2" 85c06000 0x40 (set g2 (bv 32 0x40))
dE "call g1+i2" 9fc0401a 0x40 (set o7 (bv 32 0x40))
dE "call o1+8" 9fc26008 0x40 (set o7 (bv 32 0x40))
dE "call g1" 9fc06000 0x40 (set o7 (bv 32 0x40))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(branch true (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(branch false (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bg 0x1000;nop" 1480040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "ble 0x1000;nop" 0480040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bge 0x1000;nop" 1680040001000000 0x0 nop;(branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bl 0x1000;nop" 0680040001000000 0x0 nop;(branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bgu 0x1000;nop" 1880040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bleu 0x1000;nop" 0880040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch true (jmp (var EA)) nop))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch false (jmp (var EA)) nop))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (jmp (var EA)) nop))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x2) false)) (jmp (var EA)) nop))
dE "bg 0x1000;nop" 1480040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (jmp (var EA)) nop))
dE "ble 0x1000;nop" 0480040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bge 0x1000;nop" 1680040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bl 0x1000;nop" 0680040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (jmp (var EA)) nop))
dE "bgu 0x1000;nop" 1880040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (jmp (var EA)) nop))
dE "bleu 0x1000;nop" 0880040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (jmp (var EA)) nop))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (! (lsb (var ccr))) (jmp (var EA)) nop))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (lsb (var ccr)) (jmp (var EA)) nop))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (jmp (var EA)) nop))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x3) false)) (jmp (var EA)) nop))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (jmp (var EA)) nop))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x1) false)) (jmp (var EA)) nop))
dE "ldsb [i0+l6], o2" d44e0016 0x0 (set o2 (cast 32 (msb (loadw 0 8 (+ (var i0) (var l6)))) (loadw 0 8 (+ (var i0) (var l6)))))
dE "ldsb [i0+0x20], o2" d44e2020 0x0 (set o2 (cast 32 (msb (loadw 0 8 (+ (var i0) (bv 32 0x20)))) (loadw 0 8 (+ (var i0) (bv 32 0x20)))))
dE "ldsb [g1], o4" d8484000 0x0 (set o4 (cast 32 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))

View file

@ -35,38 +35,38 @@ dE "call g1+i2" 9fc0401a 0x40 (set o7 (bv 64 0x40))
dE "call o1+8" 9fc26008 0x40 (set o7 (bv 64 0x40))
dE "call g1" 9fc06000 0x40 (set o7 (bv 64 0x40))
dE "call g1;nop;call g1;nop" 9fc06000010000009fc0600001000000 0x40 (set o7 (bv 64 0x40));(seq (set EA (cast 64 false (var g1))) empty (jmp (var EA)));(set o7 (bv 64 0x48));(seq (set EA (cast 64 false (var g1))) empty (jmp (var EA)))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bg 0x1000;nop" 1480040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ble 0x1000;nop" 0480040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bge 0x1000;nop" 1680040001000000 0x0 nop;(branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bl 0x1000;nop" 0680040001000000 0x0 nop;(branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bgu 0x1000;nop" 1880040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bleu 0x1000;nop" 0880040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch true (jmp (var EA)) nop))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch false (jmp (var EA)) nop))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (jmp (var EA)) nop))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x2) false)) (jmp (var EA)) nop))
dE "bg 0x1000;nop" 1480040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (jmp (var EA)) nop))
dE "ble 0x1000;nop" 0480040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bge 0x1000;nop" 1680040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bl 0x1000;nop" 0680040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (jmp (var EA)) nop))
dE "bgu 0x1000;nop" 1880040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (jmp (var EA)) nop))
dE "bleu 0x1000;nop" 0880040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (jmp (var EA)) nop))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (var ccr))) (jmp (var EA)) nop))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (var ccr)) (jmp (var EA)) nop))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (jmp (var EA)) nop))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x3) false)) (jmp (var EA)) nop))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (jmp (var EA)) nop))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x1) false)) (jmp (var EA)) nop))
dE "ba,a xcc, 0x1000;nop" 3068040001000000 0x0 (jmp (cast 64 false (bv 64 0x1000)));nop
dE "bn,a xcc, 0x1000;nop" 2068040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bne,a xcc, 0x1000;nop" 3268040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "be,a xcc, 0x1000;nop" 2268040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bg,a xcc, 0x1000;nop" 3468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "ble,a xcc, 0x1000;nop" 2468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bge,a xcc, 0x1000;nop" 3668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bl,a xcc, 0x1000;nop" 2668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bgu,a xcc, 0x1000;nop" 3868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bleu,a xcc, 0x1000;nop" 2868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bcc,a xcc, 0x1000;nop" 3a68040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x4) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bcs,a xcc, 0x1000;nop" 2a68040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x4) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bpos,a xcc, 0x1000;nop" 3c68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bneg,a xcc, 0x1000;nop" 2c68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bvc,a xcc, 0x1000;nop" 3e68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bvs,a xcc, 0x1000;nop" 2e68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bn,a xcc, 0x1000;nop" 2068040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bne,a xcc, 0x1000;nop" 3268040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "be,a xcc, 0x1000;nop" 2268040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bg,a xcc, 0x1000;nop" 3468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "ble,a xcc, 0x1000;nop" 2468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bge,a xcc, 0x1000;nop" 3668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bl,a xcc, 0x1000;nop" 2668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bgu,a xcc, 0x1000;nop" 3868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bleu,a xcc, 0x1000;nop" 2868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bcc,a xcc, 0x1000;nop" 3a68040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x4) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bcs,a xcc, 0x1000;nop" 2a68040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x4) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bpos,a xcc, 0x1000;nop" 3c68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bneg,a xcc, 0x1000;nop" 2c68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bvc,a xcc, 0x1000;nop" 3e68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "bvs,a xcc, 0x1000;nop" 2e68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "ldsb [i0+l6], o2" d44e0016 0x0 (set o2 (cast 64 (msb (loadw 0 8 (+ (var i0) (var l6)))) (loadw 0 8 (+ (var i0) (var l6)))))
dE "ldsb [i0+0x20], o2" d44e2020 0x0 (set o2 (cast 64 (msb (loadw 0 8 (+ (var i0) (bv 64 0x20)))) (loadw 0 8 (+ (var i0) (bv 64 0x20)))))
dE "ldsb [g1], o4" d8484000 0x0 (set o4 (cast 64 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))
@ -142,19 +142,19 @@ dE "tle icc, i3" 85d0001b 0x0 (branch (let ccf (var ccr) (|| (lsb (>> (var ccf)
dE "save o0, l1, i7" bfe20011 0x0 (seq (set add_result (+ (cast 64 false (var o0)) (cast 64 false (var l1)))) (set reg_window_base (* (var cwp) (bv 64 0x400))) (storew 1 (+ (var reg_window_base) (bv 64 0x0)) (var l0)) (storew 1 (+ (var reg_window_base) (bv 64 0x40)) (var l1)) (storew 1 (+ (var reg_window_base) (bv 64 0x80)) (var l2)) (storew 1 (+ (var reg_window_base) (bv 64 0xc0)) (var l3)) (storew 1 (+ (var reg_window_base) (bv 64 0x100)) (var l4)) (storew 1 (+ (var reg_window_base) (bv 64 0x140)) (var l5)) (storew 1 (+ (var reg_window_base) (bv 64 0x180)) (var l6)) (storew 1 (+ (var reg_window_base) (bv 64 0x1c0)) (var l7)) (storew 1 (+ (var reg_window_base) (bv 64 0x200)) (var i0)) (storew 1 (+ (var reg_window_base) (bv 64 0x240)) (var i1)) (storew 1 (+ (var reg_window_base) (bv 64 0x280)) (var i2)) (storew 1 (+ (var reg_window_base) (bv 64 0x2c0)) (var i3)) (storew 1 (+ (var reg_window_base) (bv 64 0x300)) (var i4)) (storew 1 (+ (var reg_window_base) (bv 64 0x340)) (var i5)) (storew 1 (+ (var reg_window_base) (bv 64 0x380)) (var fp)) (storew 1 (+ (var reg_window_base) (bv 64 0x3c0)) (var i7)) (set cwp (mod (+ (var cwp) (bv 64 0x1)) (bv 64 0x8))) (set i0 (var o0)) (set i1 (var o1)) (set i2 (var o2)) (set i3 (var o3)) (set i4 (var o4)) (set i5 (var o5)) (set fp (var sp)) (set i7 (var o7)) (set l0 (bv 64 0x0)) (set l1 (bv 64 0x0)) (set l2 (bv 64 0x0)) (set l3 (bv 64 0x0)) (set l4 (bv 64 0x0)) (set l5 (bv 64 0x0)) (set l6 (bv 64 0x0)) (set l7 (bv 64 0x0)) (set o0 (bv 64 0x0)) (set o1 (bv 64 0x0)) (set o2 (bv 64 0x0)) (set o3 (bv 64 0x0)) (set o4 (bv 64 0x0)) (set o5 (bv 64 0x0)) (set sp (bv 64 0x0)) (set o7 (bv 64 0x0)) (set i7 (var add_result)))
dE "restore o0, l1, i7" bfea0011 0x0 (seq (set add_result (+ (cast 64 false (var o0)) (cast 64 false (var l1)))) (set cwp (mod (- (var cwp) (bv 64 0x1)) (bv 64 0x8))) (set o0 (var i0)) (set o1 (var i1)) (set o2 (var i2)) (set o3 (var i3)) (set o4 (var i4)) (set o5 (var i5)) (set sp (var fp)) (set o7 (var i7)) (set reg_window_base (* (var cwp) (bv 64 0x400))) (set l0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x0)))) (set l1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x40)))) (set l2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x80)))) (set l3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0xc0)))) (set l4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x100)))) (set l5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x140)))) (set l6 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x180)))) (set l7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x1c0)))) (set i0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x200)))) (set i1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x240)))) (set i2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x280)))) (set i3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x2c0)))) (set i4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x300)))) (set i5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x340)))) (set fp (loadw 1 64 (+ (var reg_window_base) (bv 64 0x380)))) (set i7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x3c0)))) (set i7 (var add_result)))
dE "brz i0, 0x1000;nop" 02ce040001000000 0x0 nop;(branch (is_zero (var i0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brlez i0, 0x1000;nop" 04ce040001000000 0x0 nop;(branch (sle (var i0) (bv 64 0x0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brlz i0, 0x1000;nop" 06ce040001000000 0x0 nop;(branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brnz i0, 0x1000;nop" 0ace040001000000 0x0 nop;(branch (! (is_zero (var i0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brgz i0, 0x1000;nop" 0cce040001000000 0x0 nop;(branch (! (sle (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brgez i0, 0x1000;nop" 0ece040001000000 0x0 nop;(branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brz i0, 0x1000;nop" 02ce040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (is_zero (var i0)) (jmp (var EA)) nop))
dE "brlez i0, 0x1000;nop" 04ce040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (sle (var i0) (bv 64 0x0)) (jmp (var EA)) nop))
dE "brlz i0, 0x1000;nop" 06ce040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (jmp (var EA)) nop))
dE "brnz i0, 0x1000;nop" 0ace040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (is_zero (var i0))) (jmp (var EA)) nop))
dE "brgz i0, 0x1000;nop" 0cce040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (sle (var i0) (bv 64 0x0))) (jmp (var EA)) nop))
dE "brgez i0, 0x1000;nop" 0ece040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (jmp (var EA)) nop))
dE "brz,a i0, 0x1000;nop" 22ce040001000000 0x0 nop;(branch (is_zero (var i0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brlez,a i0, 0x1000;nop" 24ce040001000000 0x0 nop;(branch (sle (var i0) (bv 64 0x0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brlz,a i0, 0x1000;nop" 26ce040001000000 0x0 nop;(branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brnz,a i0, 0x1000;nop" 2ace040001000000 0x0 nop;(branch (! (is_zero (var i0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brgz,a i0, 0x1000;nop" 2cce040001000000 0x0 nop;(branch (! (sle (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brgez,a i0, 0x1000;nop" 2ece040001000000 0x0 nop;(branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brz,a i0, 0x1000;nop" 22ce040001000000 0x0 nop;(branch (is_zero (var i0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "brlez,a i0, 0x1000;nop" 24ce040001000000 0x0 nop;(branch (sle (var i0) (bv 64 0x0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "brlz,a i0, 0x1000;nop" 26ce040001000000 0x0 nop;(branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "brnz,a i0, 0x1000;nop" 2ace040001000000 0x0 nop;(branch (! (is_zero (var i0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "brgz,a i0, 0x1000;nop" 2cce040001000000 0x0 nop;(branch (! (sle (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "brgez,a i0, 0x1000;nop" 2ece040001000000 0x0 nop;(branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) nop)
dE "wr i0, g1, y" 81860001 0x0 (set y (^ (var i0) (var g1)))
dE "wr i0, g1, ccr" 85860001 0x0 (set ccr (cast 8 false (^ (var i0) (var g1))))
@ -301,38 +301,38 @@ dE "fors f0, f16, f30" bdb00fb0 0x0 (seq (set bv (| (fbits (float 0 (var f0) ))
# V9 only
dE "fba 0x4000;nop" 1180100001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbn 0x4000;nop" 0180100001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbu 0x4000;nop" 0f80100001000000 0x0 nop;(branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbg 0x4000;nop" 0d80100001000000 0x0 nop;(branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbug 0x4000;nop" 0b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbl 0x4000;nop" 0980100001000000 0x0 nop;(branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbul 0x4000;nop" 0780100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fblg 0x4000;nop" 0580100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbne 0x4000;nop" 0380100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbe 0x4000;nop" 1380100001000000 0x0 nop;(branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbue 0x4000;nop" 1580100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbge 0x4000;nop" 1780100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbuge 0x4000;nop" 1980100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fble 0x4000;nop" 1b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbule 0x4000;nop" 1d80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbo 0x4000;nop" 1f80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fba,a 0x4000;nop" 3180100001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbn,a 0x4000;nop" 2180100001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbu,a 0x4000;nop" 2f80100001000000 0x0 nop;(branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbg,a 0x4000;nop" 2d80100001000000 0x0 nop;(branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbug,a 0x4000;nop" 2b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbl,a 0x4000;nop" 2980100001000000 0x0 nop;(branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbul,a 0x4000;nop" 2780100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fblg,a 0x4000;nop" 2580100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbne,a 0x4000;nop" 2380100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbe,a 0x4000;nop" 3380100001000000 0x0 nop;(branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbue,a 0x4000;nop" 3580100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbge,a 0x4000;nop" 3780100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbuge,a 0x4000;nop" 3980100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fble,a 0x4000;nop" 3b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbule,a 0x4000;nop" 3d80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbo,a 0x4000;nop" 3f80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fba 0x4000;nop" 1180100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch true (jmp (var EA)) nop))
dE "fbn 0x4000;nop" 0180100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch false (jmp (var EA)) nop))
dE "fbu 0x4000;nop" 0f80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (jmp (var EA)) nop))
dE "fbg 0x4000;nop" 0d80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (jmp (var EA)) nop))
dE "fbug 0x4000;nop" 0b80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbl 0x4000;nop" 0980100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (jmp (var EA)) nop))
dE "fbul 0x4000;nop" 0780100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fblg 0x4000;nop" 0580100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbne 0x4000;nop" 0380100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbe 0x4000;nop" 1380100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (jmp (var EA)) nop))
dE "fbue 0x4000;nop" 1580100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbge 0x4000;nop" 1780100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbuge 0x4000;nop" 1980100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fble 0x4000;nop" 1b80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbule 0x4000;nop" 1d80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fbo 0x4000;nop" 1f80100001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (jmp (var EA)) nop))
dE "fba,a 0x4000;nop" 3180100001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbn,a 0x4000;nop" 2180100001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbu,a 0x4000;nop" 2f80100001000000 0x0 nop;(branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbg,a 0x4000;nop" 2d80100001000000 0x0 nop;(branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbug,a 0x4000;nop" 2b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbl,a 0x4000;nop" 2980100001000000 0x0 nop;(branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbul,a 0x4000;nop" 2780100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fblg,a 0x4000;nop" 2580100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbne,a 0x4000;nop" 2380100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbe,a 0x4000;nop" 3380100001000000 0x0 nop;(branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbue,a 0x4000;nop" 3580100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbge,a 0x4000;nop" 3780100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbuge,a 0x4000;nop" 3980100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fble,a 0x4000;nop" 3b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbule,a 0x4000;nop" 3d80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fbo,a 0x4000;nop" 3f80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) nop)
dE "fmovrsz g1, f0, f4" 89a844a0 0x0 (branch (is_zero (var g1)) (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrdlez g1, f0, f4" 89a848c0 0x0 (branch (sle (var g1) (bv 64 0x0)) (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
@ -437,22 +437,22 @@ dE "sdivx g1, i2, i0" b168401a 0x0 (set i0 (cast 64 false (sdiv (cast 64 false (
dE "sdivx g1, 0x3f, i0" b168603f 0x0 (set i0 (cast 64 false (sdiv (cast 64 false (var g1)) (cast 64 false (bv 64 0x3f)))))
dE "udivx g1, i2, i0" b068401a 0x0 (set i0 (cast 64 false (div (cast 64 false (var g1)) (cast 64 false (var i2)))))
dE "udivx g1, 0x3f, i0" b068603f 0x0 (set i0 (cast 64 false (div (cast 64 false (var g1)) (cast 64 false (bv 64 0x3f)))))
dE "ba icc, 0x1000;nop" 1048040001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bn icc, 0x1000;nop" 0048040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bne icc, 0x1000;nop" 1248040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "be icc, 0x1000;nop" 0248040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bg icc, 0x1000;nop" 1448040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ble icc, 0x1000;nop" 0448040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bge icc, 0x1000;nop" 1648040001000000 0x0 nop;(branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bl icc, 0x1000;nop" 0648040001000000 0x0 nop;(branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bgu icc, 0x1000;nop" 1848040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bleu icc, 0x1000;nop" 0848040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcc icc, 0x1000;nop" 1a48040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcs icc, 0x1000;nop" 0a48040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bpos icc, 0x1000;nop" 1c48040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bneg icc, 0x1000;nop" 0c48040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvc icc, 0x1000;nop" 1e48040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvs icc, 0x1000;nop" 0e48040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ba icc, 0x1000;nop" 1048040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch true (jmp (var EA)) nop))
dE "bn icc, 0x1000;nop" 0048040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch false (jmp (var EA)) nop))
dE "bne icc, 0x1000;nop" 1248040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (jmp (var EA)) nop))
dE "be icc, 0x1000;nop" 0248040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x2) false)) (jmp (var EA)) nop))
dE "bg icc, 0x1000;nop" 1448040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (jmp (var EA)) nop))
dE "ble icc, 0x1000;nop" 0448040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bge icc, 0x1000;nop" 1648040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (jmp (var EA)) nop))
dE "bl icc, 0x1000;nop" 0648040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (jmp (var EA)) nop))
dE "bgu icc, 0x1000;nop" 1848040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (jmp (var EA)) nop))
dE "bleu icc, 0x1000;nop" 0848040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (jmp (var EA)) nop))
dE "bcc icc, 0x1000;nop" 1a48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (var ccr))) (jmp (var EA)) nop))
dE "bcs icc, 0x1000;nop" 0a48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (var ccr)) (jmp (var EA)) nop))
dE "bpos icc, 0x1000;nop" 1c48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (jmp (var EA)) nop))
dE "bneg icc, 0x1000;nop" 0c48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x3) false)) (jmp (var EA)) nop))
dE "bvc icc, 0x1000;nop" 1e48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (jmp (var EA)) nop))
dE "bvs icc, 0x1000;nop" 0e48040001000000 0x0 nop;(seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (branch (lsb (>> (var ccr) (bv 8 0x1) false)) (jmp (var EA)) nop))
dE "swap [i0+l6], o2" d47e0016 0x0 (seq (set mem_val (loadw 0 32 (+ (var i0) (var l6)))) (storew 0 (+ (var i0) (var l6)) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val))))
dE "swap [i0+0x20], o2" d47e2020 0x0 (seq (set mem_val (loadw 0 32 (+ (var i0) (bv 64 0x20)))) (storew 0 (+ (var i0) (bv 64 0x20)) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val))))
dE "cas [i0], l6, o2" d5e61016 0x0 (seq (set mem_val (loadw 0 32 (var i0))) (branch (== (var mem_val) (cast 32 false (var l6))) (seq (storew 0 (var i0) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val)))) (set o2 (cast 64 false (var mem_val)))))