diff options
author | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-05-07 23:26:42 -0700 |
---|---|---|
committer | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-05-07 23:26:42 -0700 |
commit | fdbc8e0582dfe1addb229d406201a2ec1d513959 (patch) | |
tree | ed2c0e8782a88386d1977f53b8b3cbd26ed5d3a4 /examples/hashsmt/sha1_collision.cpp | |
parent | 021be18a8d84179966703f07f8f98d2c9193e248 (diff) |
Adding encoding of sha1 collision for the hashing example
Diffstat (limited to 'examples/hashsmt/sha1_collision.cpp')
-rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp new file mode 100644 index 000000000..b517f1b03 --- /dev/null +++ b/examples/hashsmt/sha1_collision.cpp @@ -0,0 +1,108 @@ +/********************* */ +/*! \file sha1smt.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +/* + * sha1smt.cpp + * + * Created on: Jul 13, 2012 + * Author: dejan + */ + +#include <string> +#include <fstream> +#include <iostream> +#include <sstream> + +#include "word.h" +#include "sha1.hpp" +#include "expr/command.h" + +#include <boost/uuid/sha1.hpp> + +using namespace std; +using namespace CVC4; + +hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) { + hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size]; + for(unsigned i = 0; i < size; ++i) { + stringstream ss; + ss << prefix << i; + input[i] = hashsmt::cvc4_uchar8(ss.str()); + output << DeclareFunctionCommand(ss.str(), input[i].getExpr(), input[i].getExpr().getType()) << endl; + } + return input; +} + +int main(int argc, char* argv[]) { + + try { + + // Check the arguments + if (argc != 4) { + cerr << "usage: sha1smt size rounds (1..80) output-file" << std::endl; + return 1; + } + + // Get the input size to encode + unsigned msgSize; + istringstream msgSize_is(argv[1]); + msgSize_is >> msgSize; + + // Get the number of rounds to use + unsigned rounds; + istringstream rounds_is(argv[2]); + rounds_is >> rounds; + + // The output + ofstream output(argv[3]); + output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << SetBenchmarkLogicCommand("QF_BV") << endl; + output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl; + + // Make the variables the size of the string + hashsmt::cvc4_uchar8 *cvc4input1 = createInput(msgSize, "x", output); + hashsmt::cvc4_uchar8 *cvc4input2 = createInput(msgSize, "y", output); + + // Do the cvc4 encoding for first message + hashsmt::sha1 cvc4encoder1(rounds); + cvc4encoder1.process_bytes(cvc4input1, msgSize); + hashsmt::cvc4_uint32 cvc4digest1[5]; + cvc4encoder1.get_digest(cvc4digest1); + + // Do the cvc4 encoding for second message + hashsmt::sha1 cvc4encoder2(rounds); + cvc4encoder2.process_bytes(cvc4input2, msgSize); + hashsmt::cvc4_uint32 cvc4digest2[5]; + cvc4encoder2.get_digest(cvc4digest2); + + // Create the assertion + Expr inputEqual = (hashsmt::Word::concat(cvc4input1, msgSize) == hashsmt::Word::concat(cvc4input2, msgSize)); + Expr digestEqual = (hashsmt::Word::concat(cvc4digest1, 5) == hashsmt::Word::concat(cvc4digest2, 5)); + Expr assertion = inputEqual.notExpr().andExpr(digestEqual); + + output << AssertCommand(assertion) << endl; + + // Checksat command + output << CheckSatCommand() << endl; + + } catch (CVC4::Exception& e) { + cerr << e << endl; + } +} + + + |