<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
<externalSettings/>
<extensions>
- <extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GmakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.CWDLocator" point="org.eclipse.cdt.core.ErrorParser"/>
+ <extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
</extensions>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
</profile>
</scannerConfigBuildInfo>
</storageModule>
+ <storageModule moduleId="org.eclipse.cdt.core.LanguageSettingsProviders"/>
<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets">
<buildTargets>
- <target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <target name="check" path="test/regress" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
<buildCommand>make</buildCommand>
<buildArguments>-j10</buildArguments>
<buildTarget>check</buildTarget>
<stopOnError>true</stopOnError>
- <useDefaultCommand>false</useDefaultCommand>
+ <useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
</target>
- <target name="all" path="examples" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <target name="all" path="examples/hashsmt" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
<buildCommand>make</buildCommand>
- <buildArguments>-j10</buildArguments>
- <buildTarget>all</buildTarget>
+ <buildArguments>-j3</buildArguments>
+ <buildTarget/>
<stopOnError>true</stopOnError>
<useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
<useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
</target>
- <target name="check" path="test/regress" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <target name="all" path="examples" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
<buildCommand>make</buildCommand>
<buildArguments>-j10</buildArguments>
- <buildTarget>check</buildTarget>
+ <buildTarget>all</buildTarget>
<stopOnError>true</stopOnError>
<useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
<useDefaultCommand>true</useDefaultCommand>
<runAllBuilders>true</runAllBuilders>
</target>
+ <target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+ <buildCommand>make</buildCommand>
+ <buildArguments>-j10</buildArguments>
+ <buildTarget>check</buildTarget>
+ <stopOnError>true</stopOnError>
+ <useDefaultCommand>false</useDefaultCommand>
+ <runAllBuilders>true</runAllBuilders>
+ </target>
</buildTargets>
</storageModule>
- <storageModule moduleId="org.eclipse.cdt.core.LanguageSettingsProviders"/>
</cproject>
AM_CFLAGS = -Wall
noinst_PROGRAMS = \
- sha1smt
+ sha1_inversion \
+ sha1_collision
noinst_DATA =
-sha1smt_SOURCES = \
- sha1smt.cpp \
+sha1_inversion_SOURCES = \
+ sha1_inversion.cpp \
word.h \
word.cpp \
sha1.hpp
-sha1smt_LDADD = \
+sha1_inversion_LDADD = \
@builddir@/../../src/libcvc4.la
+sha1_collision_SOURCES = \
+ sha1_collision.cpp \
+ word.h \
+ word.cpp \
+ sha1.hpp
+sha1_collision_LDADD = \
+ @builddir@/../../src/libcvc4.la
+
+
# for installation
examplesdir = $(docdir)/$(subdir)
examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
public:
typedef cvc4_uint32(&digest_type)[5];
public:
- sha1();
+ sha1(unsigned rounds = 80);
void reset();
std::size_t block_byte_index_;
std::size_t byte_count_;
+
+ unsigned rounds_;
};
-inline sha1::sha1()
+inline sha1::sha1(unsigned rounds)
+: rounds_(rounds)
{
reset();
}
cvc4_uint32 d = h_[3];
cvc4_uint32 e = h_[4];
- for (std::size_t i=0; i<80; ++i) {
+ for (std::size_t i=0; i<rounds_; ++i) {
cvc4_uint32 f;
cvc4_uint32 k;
--- /dev/null
+/********************* */
+/*! \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;
+ }
+}
+
+
+
--- /dev/null
+/********************* */
+/*! \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;
+
+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) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+ output << SetBenchmarkLogicCommand("QF_BV") << endl;
+ output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
+
+ // Make the variables the size of the string
+ hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[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, 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;
+
+ delete cvc4input;
+
+ } catch (CVC4::Exception& e) {
+ cerr << e << endl;
+ }
+}
+
+
+
+++ /dev/null
-/********************* */
-/*! \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;
-
-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) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
- output << SetBenchmarkLogicCommand("QF_BV") << endl;
- output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
-
- // Make the variables the size of the string
- hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[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, 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;
-
- delete cvc4input;
-
- } catch (CVC4::Exception& e) {
- cerr << e << endl;
- }
-}
-
-
-
#include "word.h"
+#include <vector>
+
using namespace std;
using namespace hashsmt;
using namespace CVC4;
return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr());
}
+Word Word::concat(const Word words[], unsigned size) {
+ Expr concat = words[0].d_expr;
+ for(unsigned i = 1; i < size; ++i) {
+ concat = em()->mkExpr(kind::BITVECTOR_CONCAT, concat, words[i].d_expr);
+ }
+ return Word(concat);
+}
+
void Word::print(ostream& out) const {
out << CVC4::Expr::setdepth(-1) << d_expr;
}
/** Returns the comparison expression */
CVC4::Expr operator == (const Word& b) const;
+
+ /** Concatenate the given words */
+ static Word concat(const Word words[], unsigned size);
};
inline std::ostream& operator << (std::ostream& out, const Word& word) {
projects / cvc5.git / commitdiff