blob: ef5191cb7c7ead54a550ec31faf7058053f11750 (
plain)
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
108
109
110
|
/********************* */
/*! \file sha1_inversion.cpp
** \verbatim
** Top contributors (to current version):
** Dejan Jovanovic, Tim King, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. 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/version.hpp>
#if BOOST_VERSION > 106700
#include <boost/uuid/detail/sha1.hpp>
#else
#include <boost/uuid/sha1.hpp>
#endif
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#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;
int main(int argc, char* argv[]) {
try {
// Check the arguments
if (argc != 3) {
cerr << "usage: sha1smt message output-file" << std::endl;
return 1;
}
// Get the message to encode and the output file
string msg = argv[1];
unsigned msgSize = msg.size();
ofstream output(argv[2]);
output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
output << SetBenchmarkLogicCommand("QF_BV") << endl;
output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
// Make the variables the size of the string
std::vector<hashsmt::cvc4_uchar8> cvc4input(msgSize);
for (unsigned i = 0; i < msgSize; ++ i) {
stringstream ss;
ss << "x" << i;
cvc4input[i] = hashsmt::cvc4_uchar8(ss.str());
output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl;
// Ouput the solution also
Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i]));
output << "; " << AssertCommand(solution) << endl;
}
// Do the cvc4 encoding
hashsmt::sha1 cvc4encoder;
cvc4encoder.process_bytes(cvc4input.data(), msgSize);
// Get the digest as bitvectors
hashsmt::cvc4_uint32 cvc4digest[5];
cvc4encoder.get_digest(cvc4digest);
// Do the actual sha1 encoding
boost::uuids::detail::sha1 sha1encoder;
sha1encoder.process_bytes(msg.c_str(), msgSize);
unsigned sha1digest[5];
sha1encoder.get_digest(sha1digest);
// Create the assertion
Expr assertion;
for (unsigned i = 0; i < 5; ++ i) {
Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i]));
if (i > 0) {
assertion = assertion.andExpr(conjunct);
} else {
assertion = conjunct;
}
}
output << AssertCommand(assertion) << endl;
// Checksat command
output << CheckSatCommand() << endl;
} catch (CVC4::Exception& e) {
cerr << e << endl;
}
}
|
