From ffd0b9133ac4fa0b3939616767854e8ffc54feab Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Mon, 13 Feb 2017 23:13:00 +0000 Subject: Removing unused lib/SMT directory --- lib/SMT/LICENSE.CVC3 | 53 --- lib/SMT/Makefile | 27 -- lib/SMT/SMTParser.cpp | 245 ------------- lib/SMT/SMTParser.h | 92 ----- lib/SMT/main.cpp | 40 --- lib/SMT/smtlib.lex | 263 -------------- lib/SMT/smtlib.y | 974 -------------------------------------------------- 7 files changed, 1694 deletions(-) delete mode 100644 lib/SMT/LICENSE.CVC3 delete mode 100644 lib/SMT/Makefile delete mode 100644 lib/SMT/SMTParser.cpp delete mode 100644 lib/SMT/SMTParser.h delete mode 100644 lib/SMT/main.cpp delete mode 100644 lib/SMT/smtlib.lex delete mode 100644 lib/SMT/smtlib.y diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3 deleted file mode 100644 index a70d12d5..00000000 --- a/lib/SMT/LICENSE.CVC3 +++ /dev/null @@ -1,53 +0,0 @@ -/*!\page LICENSE LICENSE - -Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior -University, New York University, and the University of Iowa, hereafter -designated as the Copyright Owners. - -All rights reserved. - -Redistribution and use in source and binary forms, with or without modification, -are permitted provided that the following conditions are met: - -* Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. -* Redistributions in binary form must reproduce the above copyright notice, -this list of conditions and the following disclaimer in the documentation -and/or other materials provided with the distribution. -* Neither the names of the Copyright Owners nor the names of any contributors -may be used to endorse or promote products derived from this software -without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY -EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY -DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES -(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; -LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON -ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -Note: - -The following files contain code whose copyright does not belong to the -Copyright Owners. However, separate copyright notices in these files give -express permission to copy, use, modify, sell, or distribute the code. Please -see the copyright notices in the individual files for details. - -
-src/include/fdstream.h
-src/include/hash_map.h
-src/include/hash_fun.h
-src/include/hash_set.h
-src/include/hash_table.h
-src/sat/minisat_varorder.h
-src/sat/minisat_solver.cpp
-src/sat/minisat_heap.h
-src/sat/minisat_types.h
-src/sat/minisat_solver.h
-src/sat/minisat_global.h
-
- -*/ diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile deleted file mode 100644 index 92ec8018..00000000 --- a/lib/SMT/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -#===-- lib/SMT/Makefile ------------------------------------*- Makefile -*--===# - -LEVEL=../.. - -LIBRARYNAME=kleaverSMT -DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 - -include $(LEVEL)/Makefile.common - -# Gross, but I don't want to build proper rules for this, and I don't want users -# to have to have bison/flex, so for now require developers to make these -# manually (at least initially). - -smtlib_parser.cpp smtlib_parser.h: smtlib.y - bison -d -o smtlib_parser.cpp -p smtlib smtlib.y - mv smtlib_parser.hpp smtlib_parser.h - perl -pi -e 's/union/struct/g' smtlib_parser.cpp - perl -pi -e 's/union/struct/g' smtlib_parser.h - - -smtlib_lexer.cpp: smtlib.lex smtlib_parser.h - flex -I -Psmtlib -osmtlib_lexer.cpp smtlib.lex - perl -pi -e 's/union/struct/g' smtlib_lexer.cpp - -.PHONY: regen -regen: smtlib_lexer.cpp smtlib_parser.cpp smtlib_parser.h diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp deleted file mode 100644 index 19ce5af7..00000000 --- a/lib/SMT/SMTParser.cpp +++ /dev/null @@ -1,245 +0,0 @@ -//===-- SMTParser.cpp -----------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "SMTParser.h" - -#include "klee/ExprBuilder.h" -#include "klee/Solver.h" -#include "klee/Constraints.h" -#include "expr/Parser.h" - -#include -#include -#include -#include -#include - -//#define DEBUG - -using namespace klee; -using namespace klee::expr; - -extern int smtlibparse(); -extern void *smtlib_createBuffer(int); -extern void smtlib_deleteBuffer(void *); -extern void smtlib_switchToBuffer(void *); -extern int smtlib_bufSize(void); -extern void smtlib_setInteractive(bool); - -SMTParser* SMTParser::parserTemp = NULL; - -SMTParser::SMTParser(const std::string _filename, - ExprBuilder* _builder) : fileName(_filename), - lineNum(1), - done(false), - satQuery(NULL), - bvSize(0), - queryParsed(false), - builder(_builder) { - is = new ifstream(fileName.c_str()); - - // Initial empty environments - varEnvs.push(VarEnv()); - fvarEnvs.push(FVarEnv()); -} - -void SMTParser::Parse() { - SMTParser::parserTemp = this; - - void *buf = smtlib_createBuffer(smtlib_bufSize()); - smtlib_switchToBuffer(buf); - smtlib_setInteractive(false); - smtlibparse(); - //xcout << "Parsed successfully.\n"; -} - -Decl* SMTParser::ParseTopLevelDecl() { - return new QueryCommand(assumptions, builder->Not(satQuery), - std::vector(), - std::vector()); -} - -bool SMTParser::Solve() { - // FIXME: Support choice of solver. - bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true; - Solver *S, *STP = S = - UseDummySolver ? createDummySolver() : new STPSolver(true); - if (UseSTPQueryKQueryLog) - S = createKQueryLoggingSolver(S, "stp-queries.kquery"); - if (UseFastCexSolver) - S = createFastCexSolver(S); - S = createCexCachingSolver(S); - S = createCachingSolver(S); - S = createIndependentSolver(S); - if (0) - S = createValidatingSolver(S, STP); - - Decl *D = this->ParseTopLevelDecl(); - if (QueryCommand *QC = dyn_cast(D)) { - //llvm::cout << "Query " << ":\t"; - - assert("FIXME: Support counterexample query commands!"); - if (QC->Values.empty() && QC->Objects.empty()) { - bool result; - if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query), - result)) { - //std::cout << (result ? "VALID" : "INVALID") << "\n"; - return result; - } - } - } - llvm::cout << "FAIL"; - exit(1); -} - - -// XXX: give more info -int SMTParser::Error(const string& msg) { - llvm::errs() << SMTParser::parserTemp->fileName << ":" - << SMTParser::parserTemp->lineNum << ": " << msg << "\n"; - exit(1); - return 0; -} - - -int SMTParser::StringToInt(const std::string& s) { - std::stringstream str(s); - int x; - str >> x; - assert(str); - return x; -} - - -ExprHandle SMTParser::CreateAnd(std::vector kids) { - unsigned n_kids = kids.size(); - assert(n_kids); - if (n_kids == 1) - return kids[0]; - - ExprHandle r = builder->And(kids[n_kids-2], kids[n_kids-1]); - for (int i=n_kids-3; i>=0; i--) - r = builder->And(kids[i], r); - return r; -} - -ExprHandle SMTParser::CreateOr(std::vector kids) { - unsigned n_kids = kids.size(); - assert(n_kids); - if (n_kids == 1) - return kids[0]; - - ExprHandle r = builder->Or(kids[n_kids-2], kids[n_kids-1]); - for (int i=n_kids-3; i>=0; i--) - r = builder->Or(kids[i], r); - return r; -} - -ExprHandle SMTParser::CreateXor(std::vector kids) { - unsigned n_kids = kids.size(); - assert(n_kids); - if (n_kids == 1) - return kids[0]; - - ExprHandle r = builder->Xor(kids[n_kids-2], kids[n_kids-1]); - for (int i=n_kids-3; i>=0; i--) - r = builder->Xor(kids[i], r); - return r; -} - - -void SMTParser::DeclareExpr(std::string name, Expr::Width w) { - // for now, only allow variables which are multiples of 8 - if (w % 8 != 0) { - cout << "BitVec not multiple of 8 (" << w << "). Need to update code.\n"; - exit(1); - } - -#ifdef DEBUG - std::cout << "Declaring " << name << " of width " << w << "\n"; -#endif - - const Array *arr = Array::CreateArray(name, w / 8); - - ref *kids = new ref[w/8]; - for (unsigned i=0; i < w/8; i++) - kids[i] = builder->Read(UpdateList(arr, NULL), - builder->Constant(i, 32)); - ref var = ConcatExpr::createN(w/8, kids); // XXX: move to builder? - delete [] kids; - - AddVar(name, var); -} - - -ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) { - assert(base == 2 || base == 10 || base == 16); - llvm::APInt ap(w, val.c_str(), val.length(), base); - - return klee::ConstantExpr::alloc(ap); -} - - -void SMTParser::PushVarEnv() { -#ifdef DEBUG - cout << "Pushing new var env\n"; -#endif - varEnvs.push(VarEnv(varEnvs.top())); -} - -void SMTParser::PopVarEnv() { -#ifdef DEBUG - cout << "Popping var env\n"; -#endif - varEnvs.pop(); -} - -void SMTParser::AddVar(std::string name, ExprHandle val) { -#ifdef DEBUG - cout << "Adding (" << name << ", " << val << ") to current var env.\n"; -#endif - varEnvs.top()[name] = val; -} - -ExprHandle SMTParser::GetVar(std::string name) { - VarEnv top = varEnvs.top(); - if (top.find(name) == top.end()) { - llvm::errs() << "Cannot find variable ?" << name << "\n"; - exit(1); - } - return top[name]; -} - - -void SMTParser::PushFVarEnv() { - fvarEnvs.push(FVarEnv(fvarEnvs.top())); -} - -void SMTParser::PopFVarEnv(void) { -#ifdef DEBUG - cout << "Popping fvar env\n"; -#endif - fvarEnvs.pop(); -} - -void SMTParser::AddFVar(std::string name, ExprHandle val) { -#ifdef DEBUG - cout << "Adding (" << name << ", " << val << ") to current fvar env.\n"; -#endif - fvarEnvs.top()[name] = val; -} - -ExprHandle SMTParser::GetFVar(std::string name) { - FVarEnv top = fvarEnvs.top(); - if (top.find(name) == top.end()) { - llvm::errs() << "Cannot find fvar $" << name << "\n"; - exit(1); - } - return top[name]; -} diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h deleted file mode 100644 index ac84e74c..00000000 --- a/lib/SMT/SMTParser.h +++ /dev/null @@ -1,92 +0,0 @@ -//===-- SMTParser.h -------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - - -#ifndef SMT_PARSER_H -#define SMT_PARSER_H - -#include "expr/Parser.h" - -#include -#include -#include - -namespace klee { - class ExprBuilder; - -namespace expr { - -class SMTParser : public klee::expr::Parser { - private: - void *buf; - - public: - /* For interacting w/ the actual parser, should make this nicer */ - static SMTParser* parserTemp; - std::string fileName; - std::istream* is; - int lineNum; - bool done; - bool arraysEnabled; - - std::vector assumptions; - klee::expr::ExprHandle satQuery; - - int bvSize; - bool queryParsed; - - klee::ExprBuilder *builder; - - SMTParser(const std::string filename, ExprBuilder *builder); - - virtual klee::expr::Decl *ParseTopLevelDecl(); - bool Solve(); - - virtual void SetMaxErrors(unsigned N) { } - - virtual unsigned GetNumErrors() const { return 1; } - - virtual ~SMTParser() {} - - void Parse(void); - - int Error(const std::string& s); - - int StringToInt(const std::string& s); - ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w); - - void DeclareExpr(std::string name, Expr::Width w); - - ExprHandle CreateAnd(std::vector); - ExprHandle CreateOr(std::vector); - ExprHandle CreateXor(std::vector); - - - typedef std::map VarEnv; - typedef std::map FVarEnv; - - std::stack varEnvs; - std::stack fvarEnvs; - - void PushVarEnv(void); - void PopVarEnv(void); - void AddVar(std::string name, ExprHandle val); // to current var env - ExprHandle GetVar(std::string name); // from current var env - - void PushFVarEnv(void); - void PopFVarEnv(void); - void AddFVar(std::string name, ExprHandle val); // to current fvar env - ExprHandle GetFVar(std::string name); // from current fvar env -}; - -} -} - -#endif - diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp deleted file mode 100644 index 31fa311d..00000000 --- a/lib/SMT/main.cpp +++ /dev/null @@ -1,40 +0,0 @@ -#include "SMTParser.h" - -#include "klee/ExprBuilder.h" - -using namespace klee; - -int main(int argc, char** argv) { - if (argc != 2) { - cout << "Usage: " << argv[0] << " \n"; - return 1; - } - - enum BuilderKinds { - DefaultBuilder, - ConstantFoldingBuilder, - SimplifyingBuilder - } BuilderKind = SimplifyingBuilder; - - ExprBuilder *Builder = 0; - switch (BuilderKind) { - case DefaultBuilder: - Builder = createDefaultExprBuilder(); - break; - case ConstantFoldingBuilder: - Builder = createDefaultExprBuilder(); - Builder = createConstantFoldingExprBuilder(Builder); - break; - case SimplifyingBuilder: - Builder = createDefaultExprBuilder(); - Builder = createConstantFoldingExprBuilder(Builder); - Builder = createSimplifyingExprBuilder(Builder); - break; - } - - klee::expr::SMTParser smtParser(argv[1], Builder); - smtParser.Parse(); - int result = smtParser.Solve(); - - cout << (result ? "UNSAT":"SAT") << "\n"; -} diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex deleted file mode 100644 index c614c683..00000000 --- a/lib/SMT/smtlib.lex +++ /dev/null @@ -1,263 +0,0 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.lex - * - * Author: Clark Barrett - * - * Created: 2005 - * - *
- * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - *
- * - */ -/*****************************************************************************/ - -#include -#include "SMTParser.h" -#include "smtlib_parser.h" - -using namespace klee; -using namespace klee::expr; - -extern int smtlib_inputLine; -extern char *smtlibtext; - -extern int smtliberror (const char *msg); - -static int smtlibinput(std::istream& is, char* buf, int size) { - int res; - if(is) { - // Set the terminator char to 0 - is.getline(buf, size-1, 0); - // If failbit is set, but eof is not, it means the line simply - // didn't fit; so we clear the state and keep on reading. - bool partialStr = is.fail() && !is.eof(); - if(partialStr) - is.clear(); - - for(res = 0; resis, buf, max_size); - -int smtlib_bufSize() { return YY_BUF_SIZE; } -YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; } - -/* some wrappers for methods that need to refer to a struct. - These are used by SMTParser. */ -void *smtlib_createBuffer(int sz) { - return (void *)smtlib_create_buffer(NULL, sz); -} -void smtlib_deleteBuffer(void *buf_state) { - smtlib_delete_buffer((struct yy_buffer_state *)buf_state); -} -void smtlib_switchToBuffer(void *buf_state) { - smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state); -} -void *smtlib_bufState() { - return (void *)smtlib_buf_state(); -} - -void smtlib_setInteractive(bool is_interactive) { - yy_set_interactive(is_interactive); -} - -// File-static (local to this file) variables and functions -static std::string _string_lit; - - static char escapeChar(char c) { - switch(c) { - case 'n': return '\n'; - case 't': return '\t'; - default: return c; - } - } - -// for now, we don't have subranges. -// -// ".." { return DOTDOT_TOK; } -/*OPCHAR (['!#?\_$&\|\\@])*/ - -%} - -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno - -%x COMMENT -%x STRING_LITERAL -%x USER_VALUE -%s PAT_MODE - -LETTER ([a-zA-Z]) -DIGIT ([0-9]) -OPCHAR (['\.\_]) -IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) -%% - -[\n] { SMTParser::parserTemp->lineNum++; } -[ \t\r\f] { /* skip whitespace */ } - -{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; } - -";" { BEGIN COMMENT; } -"\n" { BEGIN INITIAL; /* return to normal mode */ - SMTParser::parserTemp->lineNum++; } -. { /* stay in comment mode */ } - -"\"" { BEGIN STRING_LITERAL; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -"\\". { /* escape characters (like \n or \") */ - _string_lit.insert(_string_lit.end(), - escapeChar(smtlibtext[1])); } -"\"" { BEGIN INITIAL; /* return to normal mode */ - smtliblval.str = new std::string(_string_lit); - return STRING_TOK; } -. { _string_lit.insert(_string_lit.end(),*smtlibtext); } - -":pat" { BEGIN PAT_MODE; - return PAT_TOK;} -"}" { BEGIN INITIAL; - return RCURBRACK_TOK; } -"{" { BEGIN USER_VALUE; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -"\\"[{}] { /* escape characters */ - _string_lit.insert(_string_lit.end(),smtlibtext[1]); } - -"}" { BEGIN INITIAL; /* return to normal mode */ - smtliblval.str = new std::string(_string_lit); - return USER_VAL_TOK; } - -"\n" { _string_lit.insert(_string_lit.end(),'\n'); - SMTParser::parserTemp->lineNum++; } -. { _string_lit.insert(_string_lit.end(),*smtlibtext); } - -"BitVec" { return BITVEC_TOK; } - -"true" { return TRUE_TOK; } -"false" { return FALSE_TOK; } -"ite" { return ITE_TOK; } -"not" { return NOT_TOK; } -"implies" { return IMPLIES_TOK; } -"if_then_else" { return IF_THEN_ELSE_TOK; } -"and" { return AND_TOK; } -"or" { return OR_TOK; } -"xor" { return XOR_TOK; } -"iff" { return IFF_TOK; } -"exists" { return EXISTS_TOK; } -"forall" { return FORALL_TOK; } -"let" { return LET_TOK; } -"flet" { return FLET_TOK; } -"notes" { return NOTES_TOK; } -"cvc_command" { return CVC_COMMAND_TOK; } -"sorts" { return SORTS_TOK; } -"funs" { return FUNS_TOK; } -"preds" { return PREDS_TOK; } -"extensions" { return EXTENSIONS_TOK; } -"definition" { return DEFINITION_TOK; } -"axioms" { return AXIOMS_TOK; } -"logic" { return LOGIC_TOK; } -"sat" { return SAT_TOK; } -"unsat" { return UNSAT_TOK; } -"unknown" { return UNKNOWN_TOK; } -"assumption" { return ASSUMPTION_TOK; } -"formula" { return FORMULA_TOK; } -"status" { return STATUS_TOK; } -"benchmark" { return BENCHMARK_TOK; } -"extrasorts" { return EXTRASORTS_TOK; } -"extrafuns" { return EXTRAFUNS_TOK; } -"extrapreds" { return EXTRAPREDS_TOK; } -"language" { return LANGUAGE_TOK; } -"distinct" { return DISTINCT_TOK; } -":pattern" { return PAT_TOK; } -":" { return COLON_TOK; } -"\[" { return LBRACKET_TOK; } -"\]" { return RBRACKET_TOK; } -"{" { return LCURBRACK_TOK;} -"}" { return RCURBRACK_TOK;} -"(" { return LPAREN_TOK; } -")" { return RPAREN_TOK; } -"$" { return DOLLAR_TOK; } -"?" { return QUESTION_TOK; } - - -"bit0" { return BIT0_TOK; } -"bit1" { return BIT1_TOK; } - -"concat" { return BVCONCAT_TOK; } -"extract" { return BVEXTRACT_TOK; } - -"bvnot" { return BVNOT_TOK; } -"bvand" { return BVAND_TOK; } -"bvor" { return BVOR_TOK; } -"bvneg" { return BVNEG_TOK; } -"bvnand" { return BVNAND_TOK; } -"bvnor" { return BVNOR_TOK; } -"bvxor" { return BVXOR_TOK; } -"bvxnor" { return BVXNOR_TOK; } - -"=" { return EQ_TOK; } -"bvcomp" { return BVCOMP_TOK; } -"bvult" { return BVULT_TOK; } -"bvule" { return BVULE_TOK; } -"bvugt" { return BVUGT_TOK; } -"bvuge" { return BVUGE_TOK; } -"bvslt" { return BVSLT_TOK; } -"bvsle" { return BVSLE_TOK; } -"bvsgt" { return BVSGT_TOK; } -"bvsge" { return BVSGE_TOK; } - -"bvadd" { return BVADD_TOK; } -"bvsub" { return BVSUB_TOK; } -"bvmul" { return BVMUL_TOK; } -"bvudiv" { return BVUDIV_TOK; } -"bvurem" { return BVUREM_TOK; } -"bvsdiv" { return BVSDIV_TOK; } -"bvsrem" { return BVSREM_TOK; } -"bvsmod" { return BVSMOD_TOK; } - -"bvshl" { return BVSHL_TOK; } -"bvlshr" { return BVLSHR_TOK; } -"bvashr" { return BVASHR_TOK; } - -"repeat" { return REPEAT_TOK; } -"zero_extend" { return ZEXT_TOK; } -"sign_extend" { return SEXT_TOK; } -"rotate_left" { return ROL_TOK; } -"rotate_right" { return ROR_TOK; } - - -"bv"[0-9]+ { smtliblval.str = new std::string(smtlibtext); return BV_TOK; } -"bvbin"[0-1]+ { smtliblval.str = new std::string(smtlibtext); return BVBIN_TOK; } -"bvhex"[0-9,A-F,a-f]+ { smtliblval.str = new std::string(smtlibtext); return BVHEX_TOK; } - - -({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; } - -<> { return EOF_TOK; } - -. { smtliberror("Illegal input character."); } -%% - diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y deleted file mode 100644 index eb3b3890..00000000 --- a/lib/SMT/smtlib.y +++ /dev/null @@ -1,974 +0,0 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.y - * - * Author: Clark Barrett - * - * Created: Apr 30 2005 - * - *
- * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - *
- * - */ -/*****************************************************************************/ -/* - This file contains the bison code for the parser that reads in CVC - commands in SMT-LIB language. -*/ - -#include "SMTParser.h" -#include "klee/Expr.h" -#include "klee/ExprBuilder.h" - -#include - -using namespace klee; -using namespace klee::expr; - -// Define shortcuts for various things -#define PARSER SMTParser::parserTemp -#define BUILDER SMTParser::parserTemp->builder -#define DONE SMTParser::parserTemp->done -#define ASSUMPTIONS SMTParser::parserTemp->assumptions -#define QUERY SMTParser::parserTemp->satQuery - -#define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled) -#define BVSIZE (SMTParser::parserTemp->bvSize) -#define QUERYPARSED SMTParser::parserTemp->queryParsed - -// Suppress the bogus warning suppression in bison (it generates -// compile error) -#undef __GNUC_MINOR__ - -/* stuff that lives in smtlib.lex */ -extern int smtliblex(void); - -int smtliberror(const char *s) -{ - return SMTParser::parserTemp->Error(s); -} - - -#define YYLTYPE_IS_TRIVIAL 1 -#define YYMAXDEPTH 10485760 - -%} - -/* -%union { - std::string *str; - std::vector *strvec; - CVC3::Expr *node; - std::vector *vec; - std::pair, std::vector > *pat_ann; -}; -*/ - -%union { - std::string *str; - klee::expr::ExprHandle node; - std::vector *vec; -}; - - -%start cmd - -/* strings are for better error messages. - "_TOK" is so macros don't conflict with kind names */ -/* -%type bench_attributes sort_symbs fun_symb_decls pred_symb_decls -%type an_formulas quant_vars an_terms fun_symb patterns -%type pattern -%type benchmark bench_name bench_attribute -%type status fun_symb_decl fun_sig pred_symb_decl pred_sig -%type an_formula quant_var an_atom prop_atom -%type an_term basic_term sort_symb pred_symb -%type var fvar -%type logic_name quant_symb connective user_value attribute annotation -%type annotations -%type patterns_annotations -*/ - -%type an_formula an_logical_formula an_atom prop_atom -%type an_formulas -%type an_term basic_term constant -%type an_fun an_arithmetic_fun an_bitwise_fun -%type an_pred -%type logic_name status attribute user_value annotation annotations -%type var fvar symb - -%token NUMERAL_TOK -%token SYM_TOK -%token STRING_TOK -%token AR_SYMB -%token USER_VAL_TOK - -%token BV_TOK -%token BVBIN_TOK -%token BVHEX_TOK - -%token BITVEC_TOK - -%token TRUE_TOK -%token FALSE_TOK -%token ITE_TOK -%token NOT_TOK -%token IMPLIES_TOK -%token IF_THEN_ELSE_TOK -%token AND_TOK -%token OR_TOK -%token XOR_TOK -%token IFF_TOK -%token EXISTS_TOK -%token FORALL_TOK -%token LET_TOK -%token FLET_TOK -%token NOTES_TOK -%token CVC_COMMAND_TOK -%token SORTS_TOK -%token FUNS_TOK -%token PREDS_TOK -%token EXTENSIONS_TOK -%token DEFINITION_TOK -%token AXIOMS_TOK -%token LOGIC_TOK -%token COLON_TOK -%token LBRACKET_TOK -%token RBRACKET_TOK -%token LCURBRACK_TOK -%token RCURBRACK_TOK -%token LPAREN_TOK -%token RPAREN_TOK -%token SAT_TOK -%token UNSAT_TOK -%token UNKNOWN_TOK -%token ASSUMPTION_TOK -%token FORMULA_TOK -%token STATUS_TOK -%token BENCHMARK_TOK -%token EXTRASORTS_TOK -%token EXTRAFUNS_TOK -%token EXTRAPREDS_TOK -%token LANGUAGE_TOK -%token DOLLAR_TOK -%token QUESTION_TOK -%token DISTINCT_TOK -%token SEMICOLON_TOK -%token EOF_TOK -%token PAT_TOK - - -%token BIT0_TOK -%token BIT1_TOK - -%token BVCONCAT_TOK -%token BVEXTRACT_TOK - -%token BVNOT_TOK -%token BVAND_TOK -%token BVOR_TOK -%token BVNEG_TOK -%token BVNAND_TOK -%token BVNOR_TOK -%token BVXOR_TOK -%token BVXNOR_TOK - -%token EQ_TOK -%token BVCOMP_TOK -%token BVULT_TOK -%token BVULE_TOK -%token BVUGT_TOK -%token BVUGE_TOK -%token BVSLT_TOK -%token BVSLE_TOK -%token BVSGT_TOK -%token BVSGE_TOK - -%token BVADD_TOK -%token BVSUB_TOK -%token BVMUL_TOK -%token BVUDIV_TOK -%token BVUREM_TOK -%token BVSDIV_TOK -%token BVSREM_TOK -%token BVSMOD_TOK -%token BVSHL_TOK -%token BVLSHR_TOK -%token BVASHR_TOK - -%token REPEAT_TOK -%token ZEXT_TOK -%token SEXT_TOK -%token ROL_TOK -%token ROR_TOK - -%% - -cmd: - benchmark - { - YYACCEPT; - } -; - -benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { } - - | EOF_TOK - { - DONE = true; - } -; - -bench_name: - SYM_TOK { } -; - -bench_attributes: - bench_attribute { } - - | bench_attributes bench_attribute { } -; - -bench_attribute: - COLON_TOK ASSUMPTION_TOK an_formula - { - ASSUMPTIONS.push_back($3); - } - - | COLON_TOK FORMULA_TOK an_formula - { - QUERYPARSED = true; - QUERY = $3; - } - - | COLON_TOK STATUS_TOK status { } - - | COLON_TOK LOGIC_TOK logic_name - { - if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") { - llvm::errs() << "ERROR: Logic " << *$3 << " not supported."; - exit(1); - } - - if (*$3 == "QF_AUFBV") - ARRAYSENABLED = true; - } -/* - | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK - { - // XXX? - } -*/ - - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK - { - PARSER->DeclareExpr(*$5, atoi($8->c_str())); - } -/* - | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK - { - //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); - //delete $4; - } -*/ - | COLON_TOK NOTES_TOK STRING_TOK - { } - - | COLON_TOK CVC_COMMAND_TOK STRING_TOK - { } - - | annotation - { } -; - - -logic_name : - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - BVSIZE = atoi($3->c_str()); - delete $3; - $$ = $1; - } - | SYM_TOK - { - $$ = $1; - } -; - -status: - SAT_TOK { } - | UNSAT_TOK { } - | UNKNOWN_TOK { } -; - -/* -sort_symbs: - sort_symb - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | sort_symbs sort_symb - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -fun_symb_decls: - fun_symb_decl - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - fun_symb_decls fun_symb_decl - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -fun_symb_decl: - LPAREN_TOK fun_sig annotations - { - $$ = $2; - delete $3; - } - | LPAREN_TOK fun_sig RPAREN_TOK - { - $$ = $2; - } -; - -fun_sig: - fun_symb sort_symbs - { - if ($2->size() == 1) { - $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0])); - } - else { - CVC3::Expr tmp(VC->listExpr("_ARROW", *$2)); - $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp)); - } - delete $1; - delete $2; - } -; - -pred_symb_decls: - pred_symb_decl - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - pred_symb_decls pred_symb_decl - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -pred_symb_decl: - LPAREN_TOK pred_sig annotations - { - $$ = $2; - delete $3; - } - | LPAREN_TOK pred_sig RPAREN_TOK - { - $$ = $2; - } -; - -pred_sig: - pred_symb sort_symbs - { - std::vector tmp(*$2); - tmp.push_back(VC->idExpr("_BOOLEAN")); - CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp)); - $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2)); - delete $1; - delete $2; - } - | pred_symb - { - $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), - VC->idExpr("_BOOLEAN"))); - delete $1; - } -; -*/ - - -an_formulas: - an_formula - { - $$ = new std::vector; - $$->push_back($1); - } - | - an_formulas an_formula - { - $1->push_back($2); - $$ = $1; - } -; - - -an_logical_formula: - - LPAREN_TOK NOT_TOK an_formula annotations - { - $$ = BUILDER->Not($3); - } - - | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations - { - $$ = Expr::createImplies($3, $4); // XXX: move to builder? - } - - | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations - { - $$ = BUILDER->Select($3, $4, $5); - } - - | LPAREN_TOK AND_TOK an_formulas annotations - { - $$ = PARSER->CreateAnd(*$3); - } - - | LPAREN_TOK OR_TOK an_formulas annotations - { - $$ = PARSER->CreateOr(*$3); - } - - | LPAREN_TOK XOR_TOK an_formulas annotations - { - $$ = PARSER->CreateXor(*$3); - } - - | LPAREN_TOK IFF_TOK an_formula an_formula annotations - { - $$ = BUILDER->Eq($3, $4); - } -; - - -an_formula: - an_atom - { - $$ = $1; - } - - | an_logical_formula - { - $$ = $1; - } - - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK - { - PARSER->PushVarEnv(); - PARSER->AddVar(*$4, $5); - } - an_formula annotations - { - $$ = $8; - PARSER->PopVarEnv(); - } - - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK - { - PARSER->PushFVarEnv(); - PARSER->AddFVar(*$4, $5); - } - an_formula annotations - { - $$ = $8; - PARSER->PopFVarEnv(); - } -; - - - -an_atom: - prop_atom - { - $$ = $1; - } - | LPAREN_TOK prop_atom annotations - { - $$ = $2; - } - - | an_pred - { - $$ = $1; - } - -/* - | LPAREN_TOK DISTINCT_TOK an_terms annotations - { - $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); - -// std::vector tmp; -// tmp.push_back(*$2); -// tmp.insert(tmp.end(), $3->begin(), $3->end()); -// $$ = new CVC3::Expr(VC->listExpr(tmp)); -// for (unsigned i = 0; i < (*$3).size(); ++i) { -// tmp.push_back(($3)[i]) -// for (unsigned j = i+1; j < (*$3).size(); ++j) { -// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); -// } -// } -// $$ = new CVC3::Expr(VC->listExpr("_AND", tmp)); - delete $3; - delete $4; - } - | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK - { - $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); -// std::vector tmp; -// for (unsigned i = 0; i < (*$3).size(); ++i) { -// for (unsigned j = i+1; j < (*$3).size(); ++j) { -// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); -// } -// } -// $$ = new CVC3::Expr(VC->listExpr("_AND", tmp)); - delete $3; - } -*/ -; - -prop_atom: - TRUE_TOK - { - $$ = BUILDER->Constant(1, 1); - } - - | FALSE_TOK - { - $$ = BUILDER->Constant(0, 1);; - } - - | fvar - { - $$ = PARSER->GetFVar(*$1); - } -; - - -an_pred: - LPAREN_TOK EQ_TOK an_term an_term annotations - { - $$ = BUILDER->Eq($3, $4); - } - - | LPAREN_TOK BVULT_TOK an_term an_term annotations - { - $$ = BUILDER->Ult($3, $4); - } - - | LPAREN_TOK BVULE_TOK an_term an_term annotations - { - $$ = BUILDER->Ule($3, $4); - } - - | LPAREN_TOK BVUGT_TOK an_term an_term annotations - { - $$ = BUILDER->Ugt($3, $4); - } - - | LPAREN_TOK BVUGE_TOK an_term an_term annotations - { - $$ = BUILDER->Uge($3, $4); - } - - | LPAREN_TOK BVSLT_TOK an_term an_term annotations - { - $$ = BUILDER->Slt($3, $4); - } - - | LPAREN_TOK BVSLE_TOK an_term an_term annotations - { - $$ = BUILDER->Sle($3, $4); - } - - | LPAREN_TOK BVSGT_TOK an_term an_term annotations - { - $$ = BUILDER->Sgt($3, $4); - } - - | LPAREN_TOK BVSGE_TOK an_term an_term annotations - { - $$ = BUILDER->Sge($3, $4); - } -; - - -an_arithmetic_fun: - - LPAREN_TOK BVNEG_TOK an_term annotations - { - smtliberror("bvneg not supported yet"); - $$ = NULL; // TODO - } - - | LPAREN_TOK BVADD_TOK an_term an_term annotations - { - $$ = BUILDER->Add($3, $4); - } - - | LPAREN_TOK BVSUB_TOK an_term an_term annotations - { - $$ = BUILDER->Sub($3, $4); - } - - | LPAREN_TOK BVMUL_TOK an_term an_term annotations - { - $$ = BUILDER->Mul($3, $4); - } - - | LPAREN_TOK BVUDIV_TOK an_term an_term annotations - { - $$ = BUILDER->UDiv($3, $4); - } - - | LPAREN_TOK BVUREM_TOK an_term an_term annotations - { - $$ = BUILDER->URem($3, $4); - } - - | LPAREN_TOK BVSDIV_TOK an_term an_term annotations - { - $$ = BUILDER->SDiv($3, $4); - } - - | LPAREN_TOK BVSREM_TOK an_term an_term annotations - { - $$ = BUILDER->SRem($3, $4); - } - - | LPAREN_TOK BVSMOD_TOK an_term an_term annotations - { - smtliberror("bvsmod not supported yet"); - $$ = NULL; // TODO - } -; - - -an_bitwise_fun: - LPAREN_TOK BVNOT_TOK an_term annotations - { - $$ = BUILDER->Not($3); - } - - | LPAREN_TOK BVAND_TOK an_term an_term annotations - { - $$ = BUILDER->And($3, $4); - } - - | LPAREN_TOK BVOR_TOK an_term an_term annotations - { - $$ = BUILDER->Or($3, $4); - } - - | LPAREN_TOK BVXOR_TOK an_term an_term annotations - { - $$ = BUILDER->Xor($3, $4); - } - - | LPAREN_TOK BVXNOR_TOK an_term an_term annotations - { - smtliberror("bvxnor not supported yet"); - $$ = NULL; // TODO - } - - | LPAREN_TOK BVSHL_TOK an_term an_term annotations - { - $$ = BUILDER->Shl($3, $4); - } - - | LPAREN_TOK BVLSHR_TOK an_term an_term annotations - { - $$ = BUILDER->LShr($3, $4); - } - - | LPAREN_TOK BVASHR_TOK an_term an_term annotations - { - $$ = BUILDER->AShr($3, $4); - } - - | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - smtliberror("rotate_left not supported yet"); - $$ = NULL; // TODO - } - - | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - smtliberror("rotate_right not supported yet"); - $$ = NULL; // TODO - } - - | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - $$ = BUILDER->ZExt($6, $6->getWidth() + PARSER->StringToInt(*$4)); - } - - | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - $$ = BUILDER->SExt($6, $6->getWidth() + PARSER->StringToInt(*$4)); - } - - | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations - { - $$ = BUILDER->Concat($3, $4); - } - - | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - smtliberror("repeat not supported yet"); - $$ = NULL; // TODO - } - - | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations - { - int off = PARSER->StringToInt(*$6); - $$ = BUILDER->Extract($8, off, PARSER->StringToInt(*$4) - off + 1); - } -; - - -an_fun: - an_logical_formula - { - $$ = $1; - } - - | an_pred - { - $$ = $1; - } - - | LPAREN_TOK BVCOMP_TOK an_term an_term annotations - { - $$ = BUILDER->Eq($3, $4); - } - - | an_arithmetic_fun - { - $$ = $1; - } - - | an_bitwise_fun - { - $$ = $1; - } - -/* - else if (ARRAYSENABLED && *$1 == "select") { - $$->push_back(VC->idExpr("_READ")); - } - else if (ARRAYSENABLED && *$1 == "store") { - $$->push_back(VC->idExpr("_WRITE")); - } -*/ -; - -constant: - BIT0_TOK - { - $$ = PARSER->GetConstExpr("0", 2, 1); - } - - | BIT1_TOK - { - $$ = PARSER->GetConstExpr("1", 2, 1); - } - - | BVBIN_TOK - { - $$ = PARSER->GetConstExpr($1->substr(5), 2, $1->length()-5); - } - | BVHEX_TOK - { - $$ = PARSER->GetConstExpr($1->substr(5), 16, ($1->length()-5)*4); - } - | BV_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = PARSER->GetConstExpr($1->substr(2), 10, PARSER->StringToInt(*$3)); - } -; - - -an_term: - basic_term - { - $$ = $1; - } - | LPAREN_TOK basic_term annotations - { - $$ = $2; - delete $3; - } - - | an_fun - { - $$ = $1; - } - - | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations - { - $$ = BUILDER->Select($3, $4, $5); - } -; - - -basic_term: - constant - { - $$ = $1; - } - - | var - { - $$ = PARSER->GetVar(*$1); - } - | symb - { - $$ = PARSER->GetVar(*$1); - } -; - - - -annotations: - RPAREN_TOK { } - | annotation annotations { } -; - -annotation: - attribute { } - - | attribute user_value { } -; - -user_value: - USER_VAL_TOK - { - delete $1; - } -; - -/* -sort_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - if (BVENABLED && *$1 == "BitVec") { - $$ = new CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3))); - } - else { - $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3))); - } - delete $1; - delete $3; - } - | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - if (BVENABLED && ARRAYSENABLED && *$1 == "Array") { - $$ = new CVC3::Expr(VC->listExpr("_ARRAY", - VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)), - VC->listExpr("_BITVECTOR", VC->ratExpr(*$5)))); - } - else { - $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5))); - } - delete $1; - delete $3; - delete $5; - } - | SYM_TOK - { - if (*$1 == "Real") { - $$ = new CVC3::Expr(VC->idExpr("_REAL")); - } else if (*$1 == "Int") { - $$ = new CVC3::Expr(VC->idExpr("_INT")); - } else { - $$ = new CVC3::Expr(VC->idExpr(*$1)); - } - delete $1; - } -; - -*/ - -/* -fun_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - else if (BVENABLED && - $1->size() > 2 && - (*$1)[0] == 'b' && - (*$1)[1] == 'v') { - int i = 2; - while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(2), 10)); - } - else $$->push_back(VC->idExpr(*$1)); - } - else $$->push_back(VC->idExpr(*$1)); - $$->push_back(VC->ratExpr(*$3)); - delete $1; - delete $3; - } -; -*/ - -attribute: - COLON_TOK SYM_TOK - { - $$ = $2; - } -; - - -var: - QUESTION_TOK SYM_TOK - { - $$ = $2; - } -; - - -fvar: - DOLLAR_TOK SYM_TOK - { - $$ = $2; - } -; - -symb: - SYM_TOK - { - $$ = $1; - } - -%% -- cgit 1.4.1