Commit 2a5361d1 authored by phlo's avatar phlo

added MUL[I]

parent 5d6bb4c4
......@@ -163,6 +163,8 @@ struct Encoder
virtual std::string encode (Addi &) = 0;
virtual std::string encode (Sub &) = 0;
virtual std::string encode (Subi &) = 0;
virtual std::string encode (Mul &) = 0;
virtual std::string encode (Muli &) = 0;
virtual std::string encode (Cmp &) = 0;
virtual std::string encode (Jmp &) = 0;
......@@ -344,6 +346,8 @@ struct SMTLib_Encoder : public Encoder
virtual std::string encode (Addi &);
virtual std::string encode (Sub &);
virtual std::string encode (Subi &);
virtual std::string encode (Mul &);
virtual std::string encode (Muli &);
virtual std::string encode (Cmp &);
virtual std::string encode (Jmp &);
......@@ -500,6 +504,8 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
virtual std::string encode (Addi &);
virtual std::string encode (Sub &);
virtual std::string encode (Subi &);
virtual std::string encode (Mul &);
virtual std::string encode (Muli &);
virtual std::string encode (Cmp &);
virtual std::string encode (Jmp &);
......@@ -763,6 +769,8 @@ struct Btor2_Encoder : public Encoder
virtual std::string encode (Addi &);
virtual std::string encode (Sub &);
virtual std::string encode (Subi &);
virtual std::string encode (Mul &);
virtual std::string encode (Muli &);
virtual std::string encode (Cmp &);
virtual std::string encode (Jmp &);
......
......@@ -1448,6 +1448,24 @@ string Btor2_Encoder::encode (Subi & s)
return nid_subi;
}
string Btor2_Encoder::encode (Mul & m)
{
string nid_mul = load(m.arg, m.indirect);
formula << btor2::mul(nid_mul = nid(), sid_bv, nids_accu[thread], nid_mul);
return nid_mul;
}
string Btor2_Encoder::encode (Muli & m)
{
string nid_muli = nids_const[m.arg];
formula << btor2::mul(nid_muli = nid(), sid_bv, nids_accu[thread], nid_muli);
return nid_muli;
}
string Btor2_Encoder::encode (Cmp & c)
{
string nid_sub = load(c.arg, c.indirect);
......
......@@ -862,6 +862,16 @@ string SMTLib_Encoder::encode (Subi & s)
return smtlib::bvsub({accu_var(prev, thread), smtlib::word2hex(s.arg)});
}
string SMTLib_Encoder::encode (Mul & m)
{
return smtlib::bvmul({accu_var(prev, thread), load(m.arg, m.indirect)});
}
string SMTLib_Encoder::encode (Muli & m)
{
return smtlib::bvmul({accu_var(prev, thread), smtlib::word2hex(m.arg)});
}
string SMTLib_Encoder::encode (Cmp & c)
{
return smtlib::bvsub({accu_var(prev, thread), load(c.arg, c.indirect)});
......
......@@ -471,6 +471,22 @@ string SMTLib_Encoder_Relational::encode (Subi & s)
return state;
}
string SMTLib_Encoder_Relational::encode (Mul & m)
{
state.accu = set_accu(m);
state.stmt = set_stmt_next();
return state;
}
string SMTLib_Encoder_Relational::encode (Muli & m)
{
state.accu = set_accu(m);
state.stmt = set_stmt_next();
return state;
}
string SMTLib_Encoder_Relational::encode (Cmp & c)
{
state.accu = set_accu(c);
......
......@@ -167,6 +167,8 @@ DEFINE_MEMORY (Add, "ADD", accu | read)
DEFINE_UNARY (Addi, "ADDI", accu)
DEFINE_MEMORY (Sub, "SUB", accu | read)
DEFINE_UNARY (Subi, "SUBI", accu)
DEFINE_MEMORY (Mul, "MUL", accu | read)
DEFINE_UNARY (Muli, "MULI", accu)
DEFINE_MEMORY (Cmp, "CMP", accu | read)
DEFINE_UNARY (Jmp, "JMP", control)
......
......@@ -156,6 +156,8 @@ DECLARE_MEMORY (Add, Load)
DECLARE_UNARY (Addi, Unary)
DECLARE_MEMORY (Sub, Load)
DECLARE_UNARY (Subi, Unary)
DECLARE_MEMORY (Mul, Load)
DECLARE_UNARY (Muli, Unary)
DECLARE_MEMORY (Cmp, Load)
DECLARE_UNARY (Jmp, Unary)
......
......@@ -352,6 +352,20 @@ void Thread::execute (Subi & s)
PUSH_BACK(pc++);
}
void Thread::execute (Mul & s)
{
accu *= load(s.arg, s.indirect);
PUSH_BACK(pc++);
}
void Thread::execute (Muli & s)
{
accu *= s.arg;
PUSH_BACK(pc++);
}
void Thread::execute (Cmp & c)
{
accu -= load(c.arg, c.indirect);
......
......@@ -142,6 +142,8 @@ struct Thread
void execute (Addi &);
void execute (Sub &);
void execute (Subi &);
void execute (Mul &);
void execute (Muli &);
void execute (Cmp &);
void execute (Jmp &);
......
......@@ -183,6 +183,9 @@ namespace smtlib
/* bit-vector sub ***********************************************************/
EXPR_BINARY_OR_MORE(bvsub, "bvsub")
/* bit-vector mul ***********************************************************/
EXPR_BINARY_OR_MORE(bvmul, "bvmul")
/* array select *************************************************************/
inline std::string select (const std::string array, const std::string index)
{
......
......@@ -3402,6 +3402,101 @@ TEST_F(Btor2_Encoder_Test, SUBI)
ASSERT_EQ(expected(), encoder->str());
}
TEST_F(Btor2_Encoder_Test, MUL)
{
add_dummy_programs(1);
reset_encoder();
init_state_definitions();
btor2::nid_t nid = encoder->node;
word_t address = 0;
Mul mul {address};
string nid_mul = encoder->encode(mul);
expected = [this, &nid, &address, &nid_mul] {
ostringstream s;
s << expected_load(nid, address);
s <<
btor2::mul(
nid_mul,
encoder->sid_bv,
encoder->nids_accu[encoder->thread],
to_string(nid - 1));
nid++;
return s.str();
};
ASSERT_EQ(expected(), encoder->str());
}
TEST_F(Btor2_Encoder_Test, MUL_indirect)
{
add_dummy_programs(1);
reset_encoder();
init_state_definitions();
btor2::nid_t nid = encoder->node;
word_t address = 0;
Mul mul {address, true};
string nid_mul = encoder->encode(mul);
expected = [this, &nid, &address, &nid_mul] {
ostringstream s;
s << expected_load_indirect(nid, address);
s <<
btor2::mul(
nid_mul,
encoder->sid_bv,
encoder->nids_accu[encoder->thread],
to_string(nid - 1));
nid++;
return s.str();
};
ASSERT_EQ(expected(), encoder->str());
}
TEST_F(Btor2_Encoder_Test, MULI)
{
add_dummy_programs(1);
reset_encoder();
init_state_definitions();
btor2::nid_t nid = encoder->node;
word_t value = 0;
Muli muli {value};
string nid_muli = encoder->encode(muli);
expected = [this, &nid, &value, &nid_muli] {
ostringstream s;
s <<
btor2::mul(
nid_muli,
encoder->sid_bv,
encoder->nids_accu[encoder->thread],
encoder->nids_const[value]);
nid++;
return s.str();
};
ASSERT_EQ(expected(), encoder->str());
}
TEST_F(Btor2_Encoder_Test, CMP)
{
add_dummy_programs(1);
......
......@@ -1565,21 +1565,21 @@ TEST_F(SMTLib_Encoder_Test, define_checkpoint_contraints_empty)
/* SMTLib_Encoder::encode *****************************************************/
TEST_F(SMTLib_Encoder_Test, LOAD)
{
Load load = Load(1);
Load load {1};
ASSERT_EQ(encoder->load(load.arg), encoder->encode(load));
}
TEST_F(SMTLib_Encoder_Test, LOAD_indirect)
{
Load load = Load(1, true);
Load load {1, true};
ASSERT_EQ(encoder->load(load.arg, load.indirect), encoder->encode(load));
}
TEST_F(SMTLib_Encoder_Test, STORE)
{
Store store = Store(1);
Store store {1};
encoder->update = ::Encoder::Update::sb_adr;
ASSERT_EQ("#x0001", encoder->encode(store));
......@@ -1590,7 +1590,7 @@ TEST_F(SMTLib_Encoder_Test, STORE)
TEST_F(SMTLib_Encoder_Test, STORE_indirect)
{
Store store = Store(1, true);
Store store {1, true};
encoder->update = ::Encoder::Update::sb_adr;
ASSERT_EQ(encoder->load(store.arg), encoder->encode(store));
......@@ -1601,7 +1601,7 @@ TEST_F(SMTLib_Encoder_Test, STORE_indirect)
TEST_F(SMTLib_Encoder_Test, ADD)
{
Add add = Add(1);
Add add {1};
ASSERT_EQ(
"(bvadd accu_0_0 " + encoder->load(add.arg) + ")",
......@@ -1610,7 +1610,7 @@ TEST_F(SMTLib_Encoder_Test, ADD)
TEST_F(SMTLib_Encoder_Test, ADD_indirect)
{
Add add = Add(1, true);
Add add {1, true};
ASSERT_EQ(
"(bvadd accu_0_0 " + encoder->load(add.arg, add.indirect) + ")",
......@@ -1619,14 +1619,14 @@ TEST_F(SMTLib_Encoder_Test, ADD_indirect)
TEST_F(SMTLib_Encoder_Test, ADDI)
{
Addi addi = Addi(1);
Addi addi {1};
ASSERT_EQ("(bvadd accu_0_0 #x0001)", encoder->encode(addi));
}
TEST_F(SMTLib_Encoder_Test, SUB)
{
Sub sub = Sub(1);
Sub sub {1};
ASSERT_EQ(
"(bvsub accu_0_0 " + encoder->load(sub.arg) + ")",
......@@ -1635,7 +1635,7 @@ TEST_F(SMTLib_Encoder_Test, SUB)
TEST_F(SMTLib_Encoder_Test, SUB_indirect)
{
Sub sub = Sub(1, true);
Sub sub {1, true};
ASSERT_EQ(
"(bvsub accu_0_0 " + encoder->load(sub.arg, sub.indirect) + ")",
......@@ -1644,14 +1644,39 @@ TEST_F(SMTLib_Encoder_Test, SUB_indirect)
TEST_F(SMTLib_Encoder_Test, SUBI)
{
Subi subi = Subi(1);
Subi subi {1};
ASSERT_EQ("(bvsub accu_0_0 #x0001)", encoder->encode(subi));
}
TEST_F(SMTLib_Encoder_Test, MUL)
{
Mul mul {1};
ASSERT_EQ(
"(bvmul accu_0_0 " + encoder->load(mul.arg) + ")",
encoder->encode(mul));
}
TEST_F(SMTLib_Encoder_Test, MUL_indirect)
{
Mul mul {1, true};
ASSERT_EQ(
"(bvmul accu_0_0 " + encoder->load(mul.arg, mul.indirect) + ")",
encoder->encode(mul));
}
TEST_F(SMTLib_Encoder_Test, MULI)
{
Muli muli {1};
ASSERT_EQ("(bvmul accu_0_0 #x0001)", encoder->encode(muli));
}
TEST_F(SMTLib_Encoder_Test, CMP)
{
Cmp cmp = Cmp(1);
Cmp cmp {1};
ASSERT_EQ(
"(bvsub accu_0_0 " + encoder->load(cmp.arg) + ")",
......@@ -1660,7 +1685,7 @@ TEST_F(SMTLib_Encoder_Test, CMP)
TEST_F(SMTLib_Encoder_Test, CMP_indirect)
{
Cmp cmp = Cmp(1, true);
Cmp cmp {1, true};
ASSERT_EQ(
"(bvsub accu_0_0 " + encoder->load(cmp.arg, cmp.indirect) + ")",
......@@ -1669,28 +1694,28 @@ TEST_F(SMTLib_Encoder_Test, CMP_indirect)
TEST_F(SMTLib_Encoder_Test, JMP)
{
Jmp jmp = Jmp(1);
Jmp jmp {1};
ASSERT_TRUE(encoder->encode(jmp).empty());
}
TEST_F(SMTLib_Encoder_Test, JZ)
{
Jz jz = Jz(1);
Jz jz {1};
ASSERT_EQ("(= accu_0_0 #x0000)", encoder->encode(jz));
}
TEST_F(SMTLib_Encoder_Test, JNZ)
{
Jnz jnz = Jnz(1);
Jnz jnz {1};
ASSERT_EQ("(not (= accu_0_0 #x0000))", encoder->encode(jnz));
}
TEST_F(SMTLib_Encoder_Test, JS)
{
Js js = Js(1);
Js js {1};
ASSERT_EQ(
"(= #b1 ((_ extract " +
......@@ -1704,7 +1729,7 @@ TEST_F(SMTLib_Encoder_Test, JS)
TEST_F(SMTLib_Encoder_Test, JNS)
{
Jns jns = Jns(1);
Jns jns {1};
ASSERT_EQ(
"(= #b0 ((_ extract " +
......@@ -1718,7 +1743,7 @@ TEST_F(SMTLib_Encoder_Test, JNS)
TEST_F(SMTLib_Encoder_Test, JNZNS)
{
Jnzns jnzns = Jnzns(1);
Jnzns jnzns {1};
ASSERT_EQ(
"(and (not (= accu_0_0 #x0000)) (= #b0 ((_ extract " +
......@@ -1731,21 +1756,21 @@ TEST_F(SMTLib_Encoder_Test, JNZNS)
TEST_F(SMTLib_Encoder_Test, MEM)
{
Mem mem = Mem(1);
Mem mem {1};
ASSERT_EQ(encoder->load(mem.arg), encoder->encode(mem));
}
TEST_F(SMTLib_Encoder_Test, MEM_indirect)
{
Mem mem = Mem(1, true);
Mem mem {1, true};
ASSERT_EQ(encoder->load(mem.arg, mem.indirect), encoder->encode(mem));
}
TEST_F(SMTLib_Encoder_Test, CAS)
{
Cas cas = Cas(1);
Cas cas {1};
encoder->update = ::Encoder::Update::accu;
......@@ -1765,7 +1790,7 @@ TEST_F(SMTLib_Encoder_Test, CAS)
TEST_F(SMTLib_Encoder_Test, CAS_indirect)
{
Cas cas = Cas(1, true);
Cas cas {1, true};
encoder->update = ::Encoder::Update::accu;
......@@ -1785,14 +1810,14 @@ TEST_F(SMTLib_Encoder_Test, CAS_indirect)
TEST_F(SMTLib_Encoder_Test, CHECK)
{
Check check = Check(1);
Check check {1};
ASSERT_TRUE(encoder->encode(check).empty());
}
TEST_F(SMTLib_Encoder_Test, EXIT)
{
Exit exit = Exit(1);
Exit exit {1};
ASSERT_EQ("#x0001", encoder->encode(exit));
}
......@@ -758,6 +758,144 @@ TEST_F(SMTLib_Encoder_Relational_Test, SUBI)
encoder->encode(subi));
}
TEST_F(SMTLib_Encoder_Relational_Test, MUL)
{
add_instruction_set(1);
reset_encoder();
encoder->pc = 4;
Mul mul {1};
ASSERT_EQ(
"(and "
"(= accu_1_0 "
"(bvmul "
"accu_0_0 "
"(ite (and sb-full_0_0 (= sb-adr_0_0 #x0001)) "
"sb-val_0_0 "
"(select heap_0 #x0001)))) "
"(= mem_1_0 mem_0_0) "
"(= sb-adr_1_0 sb-adr_0_0) "
"(= sb-val_1_0 sb-val_0_0) "
"(= sb-full_1_0 sb-full_0_0) "
"(and "
"(not stmt_1_0_0) "
"(not stmt_1_0_1) "
"(not stmt_1_0_2) "
"(not stmt_1_0_3) "
"(not stmt_1_0_4) "
"stmt_1_0_5 "
"(not stmt_1_0_6) "
"(not stmt_1_0_7) "
"(not stmt_1_0_8) "
"(not stmt_1_0_9) "
"(not stmt_1_0_10) "
"(not stmt_1_0_11) "
"(not stmt_1_0_12) "
"(not stmt_1_0_13) "
"(not stmt_1_0_14) "
"(not stmt_1_0_15) "
"(not stmt_1_0_16)) "
"(= block_1_1_0 (ite check_0_1 false block_0_1_0)) "
"(= heap_1 heap_0) "
"(not exit_1))",
encoder->encode(mul));
}
TEST_F(SMTLib_Encoder_Relational_Test, MUL_indirect)
{
add_instruction_set(1);
reset_encoder();
encoder->pc = 4;
Mul mul {1, true};
ASSERT_EQ(
"(and "
"(= accu_1_0 "
"(bvmul "
"accu_0_0 "
"(ite sb-full_0_0 "
"(ite (= sb-adr_0_0 #x0001) "
"(ite (= sb-val_0_0 #x0001) "
"sb-val_0_0 "
"(ite (= sb-adr_0_0 (select heap_0 sb-val_0_0)) "
"sb-val_0_0 "
"(select heap_0 (select heap_0 sb-val_0_0)))) "
"(ite (= sb-adr_0_0 (select heap_0 #x0001)) "
"sb-val_0_0 "
"(select heap_0 (select heap_0 #x0001)))) "
"(select heap_0 (select heap_0 #x0001))))) "
"(= mem_1_0 mem_0_0) "
"(= sb-adr_1_0 sb-adr_0_0) "
"(= sb-val_1_0 sb-val_0_0) "
"(= sb-full_1_0 sb-full_0_0) "
"(and "
"(not stmt_1_0_0) "
"(not stmt_1_0_1) "
"(not stmt_1_0_2) "
"(not stmt_1_0_3) "
"(not stmt_1_0_4) "
"stmt_1_0_5 "
"(not stmt_1_0_6) "
"(not stmt_1_0_7) "
"(not stmt_1_0_8) "
"(not stmt_1_0_9) "
"(not stmt_1_0_10) "
"(not stmt_1_0_11) "
"(not stmt_1_0_12) "
"(not stmt_1_0_13) "
"(not stmt_1_0_14) "
"(not stmt_1_0_15) "
"(not stmt_1_0_16)) "
"(= block_1_1_0 (ite check_0_1 false block_0_1_0)) "
"(= heap_1 heap_0) "
"(not exit_1))",
encoder->encode(mul));
}
TEST_F(SMTLib_Encoder_Relational_Test, MULI)
{
add_instruction_set(1);
reset_encoder();
encoder->pc = 5;
Muli muli {1};
ASSERT_EQ(
"(and "
"(= accu_1_0 (bvmul accu_0_0 #x0001)) "
"(= mem_1_0 mem_0_0) "
"(= sb-adr_1_0 sb-adr_0_0) "
"(= sb-val_1_0 sb-val_0_0) "
"(= sb-full_1_0 sb-full_0_0) "
"(and "
"(not stmt_1_0_0) "
"(not stmt_1_0_1) "
"(not stmt_1_0_2) "
"(not stmt_1_0_3) "
"(not stmt_1_0_4) "
"(not stmt_1_0_5) "
"stmt_1_0_6 "
"(not stmt_1_0_7) "
"(not stmt_1_0_8) "
"(not stmt_1_0_9) "
"(not stmt_1_0_10) "
"(not stmt_1_0_11) "
"(not stmt_1_0_12) "
"(not stmt_1_0_13) "
"(not stmt_1_0_14) "
"(not stmt_1_0_15) "
"(not stmt_1_0_16)) "
"(= block_1_1_0 (ite check_0_1 false block_0_1_0)) "
"(= heap_1 heap_0) "
"(not exit_1))",
encoder->encode(muli));
}
TEST_F(SMTLib_Encoder_Relational_Test, CMP)
{
add_instruction_set(1);
......
......@@ -133,6 +133,16 @@ TEST(SMTLib_Test, bvsub)
ASSERT_EQ("(bvsub x1 x2 x3)", smtlib::bvsub({"x1", "x2", "x3"}));
}
/* bvmul **********************************************************************/
TEST(SMTLib_Test, bvmul)
{
ASSERT_THROW(smtlib::bvmul({}), runtime_error);
ASSERT_THROW(smtlib::bvmul({"x1"}), runtime_error);
ASSERT_EQ("(bvmul x1 x2 x3)", smtlib::bvmul({"x1", "x2", "x3"}));
}
/* select *********************************************************************/
TEST(SMTLib_Test, select)
{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment