-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Adding encoding of sha1 collision for the hashing example
- Loading branch information
Showing
7 changed files
with
158 additions
and
16 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; | ||
| } | ||
| } | ||
|
|
||
|
|
||
|
|
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters