1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
/********************* */
/*! \file sha1_collision.cpp
** \verbatim
** Original author: Dejan Jovanovic
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 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 <boost/uuid/sha1.hpp>
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include "expr/expr_iomanip.h"
#include "options/language.h"
#include "options/set_language.h"
#include "sha1.hpp"
#include "smt/command.h"
#include "word.h"
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) << language::SetLanguage(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;
}
}
|
