diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-14 13:07:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-14 13:07:19 +0000 |
commit | 35637c2a760c35ca1c61edc276875cd91df0ab11 (patch) | |
tree | 0f8c24212b425b977e4c22561347cd3ae9f28aac /examples/hashsmt/word.cpp | |
parent | 587e71e5de725968d8924cceb91c79d615edb660 (diff) |
an example that uses bitvectors to simulate sha1 computation and dumps an smt problem corresponding to the hash-inversion problem
Diffstat (limited to 'examples/hashsmt/word.cpp')
-rw-r--r-- | examples/hashsmt/word.cpp | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp new file mode 100644 index 000000000..46687db14 --- /dev/null +++ b/examples/hashsmt/word.cpp @@ -0,0 +1,143 @@ +/* + * word.cpp + * + * Created on: Jul 13, 2012 + * Author: dejan + */ + +#include "word.h" + +using namespace std; +using namespace hashsmt; +using namespace CVC4; + +Expr Word::extendToSize(unsigned newSize) const { + if (newSize <= size()) { + return d_expr; + } else { + // 0-extend to size + Expr extendOp = em()->mkConst(BitVectorZeroExtend(newSize - size())); + return em()->mkExpr(extendOp, d_expr); + } +} + +ExprManager* Word::s_manager = 0; + +ExprManager* Word::em() { + if (s_manager == 0) { + CVC4::Options options; + options.inputLanguage = language::input::LANG_SMTLIB_V2; + options.outputLanguage = language::output::LANG_SMTLIB_V2; + s_manager = new CVC4::ExprManager(options); + } + return s_manager; +} + +BoolExpr Word::operator == (const Word& b) const { + return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr()); +} + +void Word::print(ostream& out) const { + out << CVC4::Expr::setdepth(-1) << d_expr; +} + +Word::Word(unsigned newSize, unsigned value) { + d_expr = em()->mkConst(BitVector(newSize, value)); +}; + +Word::Word(unsigned newSize, string name) { + d_expr = em()->mkVar(name, em()->mkBitVectorType(newSize)); +}; + +Word& Word::operator = (const Word& b) { + d_expr = b.d_expr; + return *this; +} + +Word Word::operator + (const Word& b) const { + unsigned newSize = std::max(size(), b.size()); + Expr lhs = extendToSize(newSize); + Expr rhs = b.extendToSize(newSize); + return em()->mkExpr(kind::BITVECTOR_PLUS, lhs, rhs); +} + +Word& Word::operator += (const Word& b) { + (*this) = (*this) + b; + return (*this); +} + +Word Word::operator ~ () const { + return em()->mkExpr(kind::BITVECTOR_NOT, d_expr); +} + +Word Word::operator & (const Word& b) const { + unsigned newSize = std::max(size(), b.size()); + Expr lhs = extendToSize(newSize); + Expr rhs = b.extendToSize(newSize); + return em()->mkExpr(kind::BITVECTOR_AND, lhs, rhs); +} + +Word Word::operator | (const Word& b) const { + unsigned newSize = std::max(size(), b.size()); + Expr lhs = extendToSize(newSize); + Expr rhs = b.extendToSize(newSize); + return em()->mkExpr(kind::BITVECTOR_OR, lhs, rhs); +} + +Word& Word::operator |= (const Word& b) { + (*this) = (*this) | b; + return (*this); +} + +Word Word::operator ^ (const Word& b) const { + unsigned newSize = std::max(size(), b.size()); + Expr lhs = extendToSize(newSize); + Expr rhs = b.extendToSize(newSize); + return em()->mkExpr(kind::BITVECTOR_XOR, lhs, rhs); +} + +Word Word::operator << (unsigned amount) const { + // Instead of shifting we just add zeroes, to ensure that ((char)x << 24) return 32 bits + Word padding(amount, 0); + return em()->mkExpr(kind::BITVECTOR_CONCAT, d_expr, padding.d_expr); +} + +Word Word::operator >> (unsigned amount) const { + Word shiftAmount(size(), amount); + return em()->mkExpr(kind::BITVECTOR_LSHR, d_expr, shiftAmount.d_expr); +} + +unsigned Word::size() const { + BitVectorType type = d_expr.getType(); + return type.getSize(); +} + +cvc4_uint32::cvc4_uint32(const Word& b) { + if (b.size() > 32) { + // Extract the first 32 bits + Expr extractOp = em()->mkConst(BitVectorExtract(31, 0)); + d_expr = em()->mkExpr(extractOp, b.getExpr()); + } else if (b.size() < 32) { + // 0-extend to 32 bits + Expr extendOp = em()->mkConst(BitVectorZeroExtend(32 - b.size())); + d_expr = em()->mkExpr(extendOp, b.getExpr()); + } else { + d_expr = b.getExpr(); + } +} + +cvc4_uchar8::cvc4_uchar8(const Word& b) { + if (b.size() > 8) { + // Extract the first 8 bits + Expr extractOp = em()->mkConst(BitVectorExtract(7, 0)); + d_expr = em()->mkExpr(extractOp, b.getExpr()); + } else if (b.size() < 8) { + // 0-extend to 8 bits + Expr extendOp = em()->mkConst(BitVectorZeroExtend(8 - b.size())); + d_expr = em()->mkExpr(extendOp, b.getExpr()); + } else { + d_expr = b.getExpr(); + } +} + + |