add_subdirectory(api)
# TODO(project issue $206): Port example to new API
-# add_subdirectory(hashsmt)
# add_subdirectory(nra-translate)
# add_subdirectory(sets-translate)
+++ /dev/null
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-## Mathias Preiner, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
-##
-if(Boost_FOUND)
- cvc4_add_example(sha1_inversion
- "sha1_inversion.cpp word.cpp" "hashsmt"
- # arguments to binary (for testing)
- "a" "sha1_inversion.outfile")
-endif()
-
-cvc4_add_example(sha1_collision
- "sha1_collision.cpp word.cpp" "hashsmt"
- # arguments to binary (for testing)
- "1" "1" "sha1_collision.outfile")
+++ /dev/null
-/********************* */
-/*! \file sha1.hpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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
- **/
-
-// boost/uuid/sha1.hpp header file ----------------------------------------------//
-
-// Copyright 2007 Andy Tompkins.
-// Distributed under the Boost Software License, Version 1.0. (See
-// accompanying file LICENSE_1_0.txt or copy at
-// http://www.boost.org/LICENSE_1_0.txt)
-
-// Revision History
-// 29 May 2007 - Initial Revision
-// 25 Feb 2008 - moved to namespace boost::uuids::detail
-
-// This is a byte oriented implementation
-// Note: this implementation does not handle message longer than
-// 2^32 bytes.
-
-#ifndef __CVC4__EXAMPLES__HASHSMT__SHA1_H
-#define __CVC4__EXAMPLES__HASHSMT__SHA1_H
-
-#include <cstddef>
-
-#include "word.h"
-
-#ifdef BOOST_NO_STDC_NAMESPACE
-namespace std {
- using ::size_t;
-} // namespace std
-#endif
-
-namespace hashsmt {
-
-static_assert(sizeof(unsigned char)*8 == 8,
- "Unexpected size for unsigned char");
-static_assert(sizeof(unsigned int)*8 == 32,
- "Unexpected size for unsigned int");
-
-inline cvc4_uint32 left_rotate(cvc4_uint32 x, std::size_t n)
-{
- return (x<<n) ^ (x>> (32-n));
-}
-
-class sha1
-{
-public:
- typedef cvc4_uint32(&digest_type)[5];
-public:
- sha1(unsigned rounds = 80);
-
- void reset();
-
- void process_byte(cvc4_uchar8 byte);
- void process_block(void const* bytes_begin, void const* bytes_end);
- void process_bytes(void const* buffer, std::size_t byte_count);
-
- void get_digest(digest_type digest);
-
-private:
- void process_block();
-
-private:
- cvc4_uint32 h_[5];
-
- cvc4_uchar8 block_[64];
-
- std::size_t block_byte_index_;
- std::size_t byte_count_;
-
- unsigned rounds_;
-};
-
-inline sha1::sha1(unsigned rounds)
-: rounds_(rounds)
-{
- reset();
-}
-
-inline void sha1::reset()
-{
- h_[0] = 0x67452301;
- h_[1] = 0xEFCDAB89;
- h_[2] = 0x98BADCFE;
- h_[3] = 0x10325476;
- h_[4] = 0xC3D2E1F0;
-
- block_byte_index_ = 0;
- byte_count_ = 0;
-}
-
-inline void sha1::process_byte(cvc4_uchar8 byte)
-{
- block_[block_byte_index_++] = byte;
- ++byte_count_;
- if (block_byte_index_ == 64) {
- block_byte_index_ = 0;
- process_block();
- }
-}
-
-inline void sha1::process_block(void const* bytes_begin, void const* bytes_end)
-{
- cvc4_uchar8 const* begin = static_cast<cvc4_uchar8 const*>(bytes_begin);
- cvc4_uchar8 const* end = static_cast<cvc4_uchar8 const*>(bytes_end);
- for(; begin != end; ++begin) {
- process_byte(*begin);
- }
-}
-
-inline void sha1::process_bytes(void const* buffer, std::size_t byte_count)
-{
- cvc4_uchar8 const* b = static_cast<cvc4_uchar8 const*>(buffer);
- process_block(b, b+byte_count);
-}
-
-inline void sha1::process_block()
-{
- cvc4_uint32 w[80];
- for (std::size_t i=0; i<16; ++i) {
- w[i] = (block_[i*4 + 0] << 24);
- w[i] |= (block_[i*4 + 1] << 16);
- w[i] |= (block_[i*4 + 2] << 8);
- w[i] |= (block_[i*4 + 3]);
- }
- for (std::size_t i=16; i<80; ++i) {
- w[i] = left_rotate((w[i-3] ^ w[i-8] ^ w[i-14] ^ w[i-16]), 1);
- }
-
- cvc4_uint32 a = h_[0];
- cvc4_uint32 b = h_[1];
- cvc4_uint32 c = h_[2];
- cvc4_uint32 d = h_[3];
- cvc4_uint32 e = h_[4];
-
- for (std::size_t i=0; i<rounds_; ++i) {
- cvc4_uint32 f;
- cvc4_uint32 k;
-
- if (i<20) {
- f = (b & c) | (~b & d);
- k = 0x5A827999;
- } else if (i<40) {
- f = b ^ c ^ d;
- k = 0x6ED9EBA1;
- } else if (i<60) {
- f = (b & c) | (b & d) | (c & d);
- k = 0x8F1BBCDC;
- } else {
- f = b ^ c ^ d;
- k = 0xCA62C1D6;
- }
-
- cvc4_uint32 temp = left_rotate(a, 5) + f + e + k + w[i];
- e = d;
- d = c;
- c = left_rotate(b, 30);
- b = a;
- a = temp;
- }
-
- h_[0] += a;
- h_[1] += b;
- h_[2] += c;
- h_[3] += d;
- h_[4] += e;
-}
-
-inline void sha1::get_digest(digest_type digest)
-{
- std::size_t bit_count = byte_count_*8;
-
- // append the bit '1' to the message
- process_byte(0x80);
-
- // append k bits '0', where k is the minimum number >= 0
- // such that the resulting message length is congruent to 56 (mod 64)
- // check if there is enough space for padding and bit_count
- if (block_byte_index_ > 56) {
- // finish this block
- while (block_byte_index_ != 0) {
- process_byte(0);
- }
-
- // one more block
- while (block_byte_index_ < 56) {
- process_byte(0);
- }
- } else {
- while (block_byte_index_ < 56) {
- process_byte(0);
- }
- }
-
- // append length of message (before pre-processing)
- // as a 64-bit big-endian integer
- process_byte(0);
- process_byte(0);
- process_byte(0);
- process_byte(0);
- process_byte( static_cast<unsigned char>((bit_count>>24) & 0xFF));
- process_byte( static_cast<unsigned char>((bit_count>>16) & 0xFF));
- process_byte( static_cast<unsigned char>((bit_count>>8 ) & 0xFF));
- process_byte( static_cast<unsigned char>((bit_count) & 0xFF));
-
- // get final digest
- digest[0] = h_[0];
- digest[1] = h_[1];
- digest[2] = h_[2];
- digest[3] = h_[3];
- digest[4] = h_[4];
-}
-
-} // namespace hashsmt
-
-#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */
+++ /dev/null
-/********************* */
-/*! \file sha1_collision.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Aina Niemetz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 <fstream>
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-#include "sha1.hpp"
-#include "word.h"
-
-using namespace std;
-using namespace cvc5;
-
-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;
-
- delete[] cvc4input1;
- delete[] cvc4input2;
- }
- catch (cvc5::Exception& e)
- {
- cerr << e << endl;
- }
-}
+++ /dev/null
-/********************* */
-/*! \file sha1_inversion.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
-#include "sha1.hpp"
-#include "word.h"
-
-using namespace std;
-using namespace cvc5;
-
-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 (cvc5::Exception& e)
- {
- cerr << e << endl;
- }
-}
+++ /dev/null
-/********************* */
-/*! \file word.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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
- **/
-
-/*
- * word.cpp
- *
- * Created on: Jul 13, 2012
- * Author: dejan
- */
-
-#include "word.h"
-
-#include <vector>
-
-#include <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/language.h>
-#include <cvc4/options/options.h>
-
-using namespace std;
-using namespace hashsmt;
-using namespace cvc5;
-using namespace cvc5::options;
-
-Expr Word::extendToSize(unsigned newSize) const {
- if (newSize <= size()) {
- return d_expr;
- } else {
- // 0-extend to size
- Expr extendOp = em()->mkConst(BitVectorZeroExtend(newSize - size()));
- return em()->mkExpr(extendOp, d_expr);
- }
-}
-
-ExprManager* Word::s_manager = 0;
-
-ExprManager* Word::em() {
- if (s_manager == 0) {
- cvc5::Options options;
- options.setInputLanguage(language::input::LANG_SMTLIB_V2);
- options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- s_manager = new cvc5::ExprManager(options);
- }
- return s_manager;
-}
-
-Expr Word::operator == (const Word& b) const {
- 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 << cvc5::expr::ExprSetDepth(-1) << d_expr;
-}
-
-Word::Word(unsigned newSize, unsigned value) {
- d_expr = em()->mkConst(BitVector(newSize, value));
-};
-
-Word::Word(unsigned newSize, string name) {
- d_expr = em()->mkVar(name, em()->mkBitVectorType(newSize));
-};
-
-Word& Word::operator = (const Word& b) {
- d_expr = b.d_expr;
- return *this;
-}
-
-Word Word::operator + (const Word& b) const {
- unsigned newSize = std::max(size(), b.size());
- Expr lhs = extendToSize(newSize);
- Expr rhs = b.extendToSize(newSize);
- return em()->mkExpr(kind::BITVECTOR_PLUS, lhs, rhs);
-}
-
-Word& Word::operator += (const Word& b) {
- (*this) = (*this) + b;
- return (*this);
-}
-
-Word Word::operator ~ () const {
- return em()->mkExpr(kind::BITVECTOR_NOT, d_expr);
-}
-
-Word Word::operator & (const Word& b) const {
- unsigned newSize = std::max(size(), b.size());
- Expr lhs = extendToSize(newSize);
- Expr rhs = b.extendToSize(newSize);
- return em()->mkExpr(kind::BITVECTOR_AND, lhs, rhs);
-}
-
-Word Word::operator | (const Word& b) const {
- unsigned newSize = std::max(size(), b.size());
- Expr lhs = extendToSize(newSize);
- Expr rhs = b.extendToSize(newSize);
- return em()->mkExpr(kind::BITVECTOR_OR, lhs, rhs);
-}
-
-Word& Word::operator |= (const Word& b) {
- (*this) = (*this) | b;
- return (*this);
-}
-
-Word Word::operator ^ (const Word& b) const {
- unsigned newSize = std::max(size(), b.size());
- Expr lhs = extendToSize(newSize);
- Expr rhs = b.extendToSize(newSize);
- return em()->mkExpr(kind::BITVECTOR_XOR, lhs, rhs);
-}
-
-Word Word::operator << (unsigned amount) const {
- // Instead of shifting we just add zeroes, to ensure that ((char)x << 24) return 32 bits
- Word padding(amount, 0);
- return em()->mkExpr(kind::BITVECTOR_CONCAT, d_expr, padding.d_expr);
-}
-
-Word Word::operator >> (unsigned amount) const {
- Word shiftAmount(size(), amount);
- return em()->mkExpr(kind::BITVECTOR_LSHR, d_expr, shiftAmount.d_expr);
-}
-
-unsigned Word::size() const {
- BitVectorType type = d_expr.getType();
- return type.getSize();
-}
-
-cvc4_uint32::cvc4_uint32(const Word& b) {
- if (b.size() > 32) {
- // Extract the first 32 bits
- Expr extractOp = em()->mkConst(BitVectorExtract(31, 0));
- d_expr = em()->mkExpr(extractOp, b.getExpr());
- } else if (b.size() < 32) {
- // 0-extend to 32 bits
- Expr extendOp = em()->mkConst(BitVectorZeroExtend(32 - b.size()));
- d_expr = em()->mkExpr(extendOp, b.getExpr());
- } else {
- d_expr = b.getExpr();
- }
-}
-
-cvc4_uchar8::cvc4_uchar8(const Word& b) {
- if (b.size() > 8) {
- // Extract the first 8 bits
- Expr extractOp = em()->mkConst(BitVectorExtract(7, 0));
- d_expr = em()->mkExpr(extractOp, b.getExpr());
- } else if (b.size() < 8) {
- // 0-extend to 8 bits
- Expr extendOp = em()->mkConst(BitVectorZeroExtend(8 - b.size()));
- d_expr = em()->mkExpr(extendOp, b.getExpr());
- } else {
- d_expr = b.getExpr();
- }
-}
+++ /dev/null
-/********************* */
-/*! \file word.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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
- **/
-
-/*
- * word.h
- *
- * Created on: Jul 13, 2012
- * Author: dejan
- */
-
-#ifndef WORD_H_
-#define WORD_H_
-
-#include <string>
-#include <iostream>
-
-#include <cvc4/cvc4.h>
-
-namespace hashsmt {
-
-class Word {
-
- /** Expression managaer we're using for all word expressions */
- static cvc5::ExprManager* s_manager;
-
- protected:
-
- /** The expression of this word */
- cvc5::Expr d_expr;
-
- /** Get the expression manager words are using */
- static cvc5::ExprManager* em();
-
- Word(cvc5::Expr expr = cvc5::Expr()) : d_expr(expr) {}
-
- /** Extend the representing expression to the given size >= size() */
- cvc5::Expr extendToSize(unsigned size) const;
-
- public:
-
- Word(unsigned size, unsigned value = 0);
- Word(unsigned size, std::string name);
-
- Word& operator = (const Word& b);
- Word operator + (const Word& b) const;
- Word& operator += (const Word& b);
- Word operator ~ () const;
- Word operator & (const Word& b) const;
- Word operator | (const Word& b) const;
- Word& operator |= (const Word& b);
- Word operator ^ (const Word& b) const;
- Word operator << (unsigned amount) const;
- Word operator >> (unsigned amount) const;
-
- unsigned size() const;
-
- void print(std::ostream& out) const;
-
- cvc5::Expr getExpr() const { return d_expr; }
-
- /** Returns the comparison expression */
- cvc5::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) {
- word.print(out);
- return out;
-}
-
-/** Symbolic 32-bit unsigned integer as a CVC4 bitvector expression */
-class cvc4_uint32 : public Word {
-public:
-
- /** Construction from constants of the right size */
- cvc4_uint32(unsigned value = 0)
- : Word(32, value) {}
-
- /** Construction of variables of the right size */
- cvc4_uint32(std::string name)
- : Word(32, name) {}
-
- /** Automatic extend/cut to uint32 */
- cvc4_uint32(const Word& word);
-};
-
-/** Symbolic 8-bit unsigned char as a CVC4 bitvector expression */
-class cvc4_uchar8 : public Word {
-public:
-
- /** Construction from constants of the right size */
- cvc4_uchar8(unsigned value = 0)
- : Word(8, value) {}
-
- /** Construction of variables of the right size */
- cvc4_uchar8(std::string name)
- : Word(8, name) {}
-
- /** Automatic extend/cut to uchar8 */
- cvc4_uchar8(const Word& word);
-};
-
-
-}
-
-#endif /* WORD_H_ */
projects / cvc5.git / commitdiff