aboutsummaryrefslogtreecommitdiffhomepage
path: root/stp/c_interface
diff options
context:
space:
mode:
Diffstat (limited to 'stp/c_interface')
-rw-r--r--stp/c_interface/Makefile19
-rw-r--r--stp/c_interface/c_interface.cpp1548
-rw-r--r--stp/c_interface/c_interface.h401
-rw-r--r--stp/c_interface/fdstream.h186
4 files changed, 0 insertions, 2154 deletions
diff --git a/stp/c_interface/Makefile b/stp/c_interface/Makefile
deleted file mode 100644
index 29b9006b..00000000
--- a/stp/c_interface/Makefile
+++ /dev/null
@@ -1,19 +0,0 @@
-#===-- stp/c_interface/Makefile ----------------------------*- Makefile -*--===#
-#
-# The KLEE Symbolic Virtual Machine
-#
-# This file is distributed under the University of Illinois Open Source
-# License. See LICENSE.TXT for details.
-#
-#===------------------------------------------------------------------------===#
-
-LEVEL=../..
-
-LIBRARYNAME=stp_c_interface
-DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
-
-include $(LEVEL)/Makefile.common
-
-# HACK: Force -Wno-deprecated for ext container use.
-CXX.Flags += -Wno-deprecated
diff --git a/stp/c_interface/c_interface.cpp b/stp/c_interface/c_interface.cpp
deleted file mode 100644
index 52c4df21..00000000
--- a/stp/c_interface/c_interface.cpp
+++ /dev/null
@@ -1,1548 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-#include "c_interface.h"
-
-#include <cstdlib>
-#include <cassert>
-#include <ostream>
-#include <iostream>
-#include "fdstream.h"
-#include "../AST/AST.h"
-
-//These typedefs lower the effort of using the keyboard to type (too
-//many overloaded meanings of the word type)
-typedef BEEV::ASTNode node;
-typedef BEEV::ASTNode* nodestar;
-typedef BEEV::BeevMgr* bmstar;
-typedef BEEV::ASTVec nodelist;
-typedef BEEV::CompleteCounterExample* CompleteCEStar;
-BEEV::ASTVec *decls = NULL;
-//vector<BEEV::ASTNode *> created_exprs;
-bool cinterface_exprdelete_on = false;
-
-void vc_setFlags(char c) {
- std::string helpstring = "Usage: stp [-option] [infile]\n\n";
- helpstring += "-r : switch refinement off (optimizations are ON by default)\n";
- helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n";
- helpstring += "-a : switch optimizations off (optimizations are ON by default)\n";
- helpstring += "-s : print function statistics\n";
- helpstring += "-v : print nodes \n";
- helpstring += "-c : construct counterexample\n";
- helpstring += "-d : check counterexample\n";
- helpstring += "-p : print counterexample\n";
- helpstring += "-h : help\n";
-
- switch(c) {
- case 'a' :
- BEEV::optimize = false;
- BEEV::wordlevel_solve = false;
- break;
- case 'b':
- BEEV::print_STPinput_back = true;
- break;
- case 'c':
- BEEV::construct_counterexample = true;
- break;
- case 'd':
- BEEV::construct_counterexample = true;
- BEEV::check_counterexample = true;
- break;
- case 'e':
- BEEV::variable_activity_optimize = true;
- break;
- case 'f':
- BEEV::smtlib_parser_enable = true;
- break;
- case 'h':
- cout << helpstring;
- BEEV::FatalError("");
- break;
- case 'l' :
- BEEV::linear_search = true;
- break;
- case 'n':
- BEEV::print_output = true;
- break;
- case 'p':
- BEEV::print_counterexample = true;
- break;
- case 'q':
- BEEV::print_arrayval_declaredorder = true;
- break;
- case 'r':
- BEEV::arrayread_refinement = false;
- break;
- case 's' :
- BEEV::stats = true;
- break;
- case 'u':
- BEEV::arraywrite_refinement = true;
- break;
- case 'v' :
- BEEV::print_nodes = true;
- break;
- case 'w':
- BEEV::wordlevel_solve = false;
- break;
- case 'x':
- cinterface_exprdelete_on = true;
- break;
- case 'z':
- BEEV::print_sat_varorder = true;
- break;
- default:
- std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n";
- s += helpstring;
- BEEV::FatalError(s.c_str());
- break;
- }
-}
-
-//Create a validity Checker. This is the global BeevMgr
-VC vc_createValidityChecker(void) {
- vc_setFlags('d');
-#ifdef NATIVE_C_ARITH
-#else
- CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
- if(0 != c) {
- cout << CONSTANTBV::BitVector_Error(c) << endl;
- return 0;
- }
-#endif
- bmstar bm = new BEEV::BeevMgr();
- decls = new BEEV::ASTVec();
- //created_exprs.clear();
- return (VC)bm;
-}
-
-// Expr I/O
-void vc_printExpr(VC vc, Expr e) {
- //do not print in lisp mode
- //bmstar b = (bmstar)vc;
- BEEV::ASTNode q = (*(nodestar)e);
- // b->Begin_RemoveWrites = true;
- // BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false);
- // b->Begin_RemoveWrites = false;
- q.PL_Print(cout);
-}
-
-void vc_printExprFile(VC vc, Expr e, int fd) {
- fdostream os(fd);
- ((nodestar)e)->PL_Print(os);
- //os.flush();
-}
-
-static void vc_printVarDeclsToStream(VC vc, ostream &os) {
- for(BEEV::ASTVec::iterator i = decls->begin(),iend=decls->end();i!=iend;i++) {
- node a = *i;
- switch(a.GetType()) {
- case BEEV::BITVECTOR_TYPE:
- a.PL_Print(os);
- os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;
- break;
- case BEEV::ARRAY_TYPE:
- a.PL_Print(os);
- os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";
- os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;
- break;
- case BEEV::BOOLEAN_TYPE:
- a.PL_Print(os);
- os << " : BOOLEAN;" << endl;
- break;
- default:
- BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a);
- break;
- }
- }
-}
-
-void vc_printVarDecls(VC vc) {
- vc_printVarDeclsToStream(vc, cout);
-}
-
-static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) {
- bmstar b = (bmstar)vc;
- BEEV::ASTVec v = b->GetAsserts();
- for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
- b->Begin_RemoveWrites = true;
- BEEV::ASTNode q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(*i,false) : *i;
- q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(q,false) : q;
- b->Begin_RemoveWrites = false;
- os << "ASSERT( ";
- q.PL_Print(os);
- os << ");" << endl;
- }
-}
-
-void vc_printAsserts(VC vc, int simplify_print) {
- vc_printAssertsToStream(vc, cout, simplify_print);
-}
-
-void vc_printQueryStateToBuffer(VC vc, Expr e, char **buf, unsigned long *len, int simplify_print){
- assert(vc);
- assert(e);
- assert(buf);
- assert(len);
- bmstar b = (bmstar)vc;
-
- // formate the state of the query
- stringstream os;
- vc_printVarDeclsToStream(vc, os);
- os << "%----------------------------------------------------" << endl;
- vc_printAssertsToStream(vc, os, simplify_print);
- os << "%----------------------------------------------------" << endl;
- os << "QUERY( ";
- b->Begin_RemoveWrites = true;
- BEEV::ASTNode q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(*((nodestar)e),false) : *(nodestar)e;
- b->Begin_RemoveWrites = false;
- q.PL_Print(os);
- os << " );" << endl;
-
- // convert to a c buffer
- string s = os.str();
- const char *cstr = s.c_str();
- unsigned long size = s.size() + 1; // number of chars + terminating null
- *buf = (char *)malloc(size);
- if (!(*buf)) {
- fprintf(stderr, "malloc(%lu) failed.", size);
- assert(*buf);
- }
- *len = size;
- memcpy(*buf, cstr, size);
-}
-
-void vc_printCounterExampleToBuffer(VC vc, char **buf, unsigned long *len) {
- assert(vc);
- assert(buf);
- assert(len);
- bmstar b = (bmstar)vc;
-
- // formate the state of the query
- std::ostringstream os;
- BEEV::print_counterexample = true;
- os << "COUNTEREXAMPLE BEGIN: \n";
- b->PrintCounterExample(true,os);
- os << "COUNTEREXAMPLE END: \n";
-
- // convert to a c buffer
- string s = os.str();
- const char *cstr = s.c_str();
- unsigned long size = s.size() + 1; // number of chars + terminating null
- *buf = (char *)malloc(size);
- if (!(*buf)) {
- fprintf(stderr, "malloc(%lu) failed.", size);
- assert(*buf);
- }
- *len = size;
- memcpy(*buf, cstr, size);
-}
-
-void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len) {
- stringstream os;
- //bmstar b = (bmstar)vc;
- BEEV::ASTNode q = *((nodestar)e);
- // b->Begin_RemoveWrites = true;
- // BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false);
- // b->Begin_RemoveWrites = false;
- q.PL_Print(os);
- //((nodestar)e)->PL_Print(os);
- string s = os.str();
- const char * cstr = s.c_str();
- unsigned long size = s.size() + 1; // number of chars + terminating null
- *buf = (char *)malloc(size);
- *len = size;
- memcpy(*buf, cstr, size);
-}
-
-void vc_printQuery(VC vc){
- ostream& os = std::cout;
- bmstar b = (bmstar)vc;
- os << "QUERY(";
- //b->Begin_RemoveWrites = true;
- //BEEV::ASTNode q = b->SimplifyFormula_TopLevel(b->GetQuery(),false);
- BEEV::ASTNode q = b->GetQuery();
- //b->Begin_RemoveWrites = false;
- q.PL_Print(os);
- // b->GetQuery().PL_Print(os);
- os << ");" << endl;
-}
-
-/////////////////////////////////////////////////////////////////////////////
-// Array-related methods //
-/////////////////////////////////////////////////////////////////////////////
-//! Create an array type
-Type vc_arrayType(VC vc, Type typeIndex, Type typeData) {
- bmstar b = (bmstar)vc;
- nodestar ti = (nodestar)typeIndex;
- nodestar td = (nodestar)typeData;
-
- if(!(ti->GetKind() == BEEV::BITVECTOR && (*ti)[0].GetKind() == BEEV::BVCONST))
- BEEV::FatalError("Tyring to build array whose indextype i is not a BITVECTOR, where i = ",*ti);
- if(!(td->GetKind() == BEEV::BITVECTOR && (*td)[0].GetKind() == BEEV::BVCONST))
- BEEV::FatalError("Trying to build an array whose valuetype v is not a BITVECTOR. where a = ",*td);
- nodestar output = new node(b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return (Type)output;
-}
-
-//! Create an expression for the value of array at the given index
-Expr vc_readExpr(VC vc, Expr array, Expr index) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)array;
- nodestar i = (nodestar)index;
-
- b->BVTypeCheck(*a);
- b->BVTypeCheck(*i);
- node o = b->CreateTerm(BEEV::READ,a->GetValueWidth(),*a,*i);
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-// //! Array update; equivalent to "array WITH [index] := newValue"
-Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)array;
- nodestar i = (nodestar)index;
- nodestar n = (nodestar)newValue;
-
- b->BVTypeCheck(*a);
- b->BVTypeCheck(*i);
- b->BVTypeCheck(*n);
- node o = b->CreateTerm(BEEV::WRITE,a->GetValueWidth(),*a,*i,*n);
- o.SetIndexWidth(a->GetIndexWidth());
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-/////////////////////////////////////////////////////////////////////////////
-// Context-related methods //
-/////////////////////////////////////////////////////////////////////////////
-//! Assert a new formula in the current context.
-/*! The formula must have Boolean type. */
-void vc_assertFormula(VC vc, Expr e) {
- nodestar a = (nodestar)e;
- bmstar b = (bmstar)vc;
-
- if(!BEEV::is_Form_kind(a->GetKind()))
- BEEV::FatalError("Trying to assert a NON formula: ",*a);
-
- b->BVTypeCheck(*a);
- b->AddAssert(*a);
-}
-
-//! Check validity of e in the current context.
-/*! If the result is true, then the resulting context is the same as
- * the starting context. If the result is false, then the resulting
- * context is a context in which e is false. e must have Boolean
- * type. */
-int vc_query(VC vc, Expr e) {
- nodestar a = (nodestar)e;
- bmstar b = (bmstar)vc;
-
- if(!BEEV::is_Form_kind(a->GetKind()))
- BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a);
-
- b->BVTypeCheck(*a);
- b->AddQuery(*a);
-
- const BEEV::ASTVec v = b->GetAsserts();
- node o;
- if(!v.empty()) {
- if(v.size()==1)
- return b->TopLevelSAT(v[0],*a);
- else
- return b->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a);
- }
- else
- return b->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a);
-}
-
-void vc_push(VC vc) {
- bmstar b = (bmstar)vc;
- b->ClearAllCaches();
- b->Push();
-}
-
-void vc_pop(VC vc) {
- bmstar b = (bmstar)vc;
- b->Pop();
-}
-
-void vc_printCounterExample(VC vc) {
- bmstar b = (bmstar)vc;
- BEEV::print_counterexample = true;
- cout << "COUNTEREXAMPLE BEGIN: \n";
- b->PrintCounterExample(true);
- cout << "COUNTEREXAMPLE END: \n";
-}
-
-// //! Return the counterexample after a failed query.
-// /*! This method should only be called after a query which returns
-// * false. It will try to return the simplest possible set of
-// * assertions which are sufficient to make the queried expression
-// * false. The caller is responsible for freeing the array when
-// * finished with it.
-// */
-
-Expr vc_getCounterExample(VC vc, Expr e) {
- nodestar a = (nodestar)e;
- bmstar b = (bmstar)vc;
-
- bool t = false;
- if(b->CounterExampleSize())
- t = true;
- nodestar output = new node(b->GetCounterExample(t, *a));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-int vc_counterexample_size(VC vc) {
- bmstar b = (bmstar)vc;
- return b->CounterExampleSize();
-}
-
-WholeCounterExample vc_getWholeCounterExample(VC vc) {
- bmstar b = (bmstar)vc;
- CompleteCEStar c =
- new BEEV::CompleteCounterExample(b->GetCompleteCounterExample(), b);
- return c;
-}
-
-Expr vc_getTermFromCounterExample(VC vc, Expr e, CompleteCEStar cc) {
- //bmstar b = (bmstar)vc;
- nodestar n = (nodestar)e;
- CompleteCEStar c = (CompleteCEStar)cc;
-
- nodestar output = new node(c->GetCounterExample(*n));
- return output;
-}
-
-int vc_getBVLength(VC vc, Expr ex) {
- nodestar e = (nodestar)ex;
-
- if(BEEV::BITVECTOR_TYPE != e->GetType()) {
- BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector");
- }
-
- return e->GetValueWidth();
-} // end of vc_getBVLength
-
-/////////////////////////////////////////////////////////////////////////////
-// Expr Creation methods //
-/////////////////////////////////////////////////////////////////////////////
-//! Create a variable with a given name and type
-/*! The type cannot be a function type. */
-Expr vc_varExpr1(VC vc, char* name,
- int indexwidth, int valuewidth) {
- bmstar b = (bmstar)vc;
-
- node o = b->CreateSymbol(name);
- o.SetIndexWidth(indexwidth);
- o.SetValueWidth(valuewidth);
-
- nodestar output = new node(o);
- ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
- b->BVTypeCheck(*output);
-
- //store the decls in a vector for printing purposes
- decls->push_back(o);
- return output;
-}
-
-Expr vc_varExpr(VC vc, char * name, Type type) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)type;
-
- node o = b->CreateSymbol(name);
- switch(a->GetKind()) {
- case BEEV::BITVECTOR:
- o.SetIndexWidth(0);
- o.SetValueWidth(GetUnsignedConst((*a)[0]));
- break;
- case BEEV::ARRAY:
- o.SetIndexWidth(GetUnsignedConst((*a)[0]));
- o.SetValueWidth(GetUnsignedConst((*a)[1]));
- break;
- case BEEV::BOOLEAN:
- o.SetIndexWidth(0);
- o.SetValueWidth(0);
- break;
- default:
- BEEV::FatalError("CInterface: vc_varExpr: Unsupported type",*a);
- break;
- }
- nodestar output = new node(o);
- ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
- b->BVTypeCheck(*output);
-
- //store the decls in a vector for printing purposes
- decls->push_back(o);
- return output;
-}
-
-//! Create an equality expression. The two children must have the
-//same type.
-Expr vc_eqExpr(VC vc, Expr ccc0, Expr ccc1) {
- bmstar b = (bmstar)vc;
-
- nodestar a = (nodestar)ccc0;
- nodestar aa = (nodestar)ccc1;
- b->BVTypeCheck(*a);
- b->BVTypeCheck(*aa);
- node o = b->CreateNode(BEEV::EQ,*a,*aa);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_boolType(VC vc) {
- bmstar b = (bmstar)vc;
-
- node o = b->CreateNode(BEEV::BOOLEAN);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-/////////////////////////////////////////////////////////////////////////////
-// BOOLEAN EXPR Creation methods //
-/////////////////////////////////////////////////////////////////////////////
-// The following functions create Boolean expressions. The children
-// provided as arguments must be of type Boolean.
-Expr vc_trueExpr(VC vc) {
- bmstar b = (bmstar)vc;
- node c = b->CreateNode(BEEV::TRUE);
-
- nodestar d = new node(c);
- //if(cinterface_exprdelete_on) created_exprs.push_back(d);
- return d;
-}
-
-Expr vc_falseExpr(VC vc) {
- bmstar b = (bmstar)vc;
- node c = b->CreateNode(BEEV::FALSE);
-
- nodestar d = new node(c);
- //if(cinterface_exprdelete_on) created_exprs.push_back(d);
- return d;
-}
-
-Expr vc_notExpr(VC vc, Expr ccc) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
-
- node o = b->CreateNode(BEEV::NOT,*a);
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_andExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- node o = b->CreateNode(BEEV::AND,*l,*r);
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_orExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- node o = b->CreateNode(BEEV::OR,*l,*r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_andExprN(VC vc, Expr* cc, int n) {
- bmstar b = (bmstar)vc;
- nodestar * c = (nodestar *)cc;
- nodelist d;
-
- for(int i =0; i < n; i++)
- d.push_back(*c[i]);
-
- node o = b->CreateNode(BEEV::AND,d);
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-
-Expr vc_orExprN(VC vc, Expr* cc, int n) {
- bmstar b = (bmstar)vc;
- nodestar * c = (nodestar *)cc;
- nodelist d;
-
- for(int i =0; i < n; i++)
- d.push_back(*c[i]);
-
- node o = b->CreateNode(BEEV::OR,d);
- b->BVTypeCheck(o);
-
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){
- bmstar b = (bmstar)vc;
- nodestar c = (nodestar)cond;
- nodestar t = (nodestar)thenpart;
- nodestar e = (nodestar)elsepart;
-
- b->BVTypeCheck(*c);
- b->BVTypeCheck(*t);
- b->BVTypeCheck(*e);
- node o;
- //if the user asks for a formula then produce a formula, else
- //prodcue a term
- if(BEEV::BOOLEAN_TYPE == t->GetType())
- o = b->CreateNode(BEEV::ITE,*c,*t,*e);
- else {
- o = b->CreateTerm(BEEV::ITE,t->GetValueWidth(),*c,*t,*e);
- o.SetIndexWidth(t->GetIndexWidth());
- }
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_impliesExpr(VC vc, Expr antecedent, Expr consequent){
- bmstar b = (bmstar)vc;
- nodestar c = (nodestar)antecedent;
- nodestar t = (nodestar)consequent;
-
- b->BVTypeCheck(*c);
- b->BVTypeCheck(*t);
- node o;
-
- o = b->CreateNode(BEEV::IMPLIES,*c,*t);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_iffExpr(VC vc, Expr e0, Expr e1){
- bmstar b = (bmstar)vc;
- nodestar c = (nodestar)e0;
- nodestar t = (nodestar)e1;
-
- b->BVTypeCheck(*c);
- b->BVTypeCheck(*t);
- node o;
-
- o = b->CreateNode(BEEV::IFF,*c,*t);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_boolToBVExpr(VC vc, Expr form) {
- bmstar b = (bmstar)vc;
- nodestar c = (nodestar)form;
-
- b->BVTypeCheck(*c);
- if(!is_Form_kind(c->GetKind()))
- BEEV::FatalError("CInterface: vc_BoolToBVExpr: You have input a NON formula:",*c);
-
- node o;
- node one = b->CreateOneConst(1);
- node zero = b->CreateZeroConst(1);
- o = b->CreateTerm(BEEV::ITE,1,*c,one,zero);
-
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-/////////////////////////////////////////////////////////////////////////////
-// BITVECTOR EXPR Creation methods //
-/////////////////////////////////////////////////////////////////////////////
-Type vc_bvType(VC vc, int num_bits) {
- bmstar b = (bmstar)vc;
-
- if(!(0 < num_bits))
- BEEV::FatalError("CInterface: number of bits in a bvtype must be a positive integer:",
- b->CreateNode(BEEV::UNDEFINED));
-
- node e = b->CreateBVConst(32, num_bits);
- nodestar output = new node(b->CreateNode(BEEV::BITVECTOR,e));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Type vc_bv32Type(VC vc) {
- return vc_bvType(vc,32);
-}
-
-
-Expr vc_bvConstExprFromStr(VC vc, char* binary_repr) {
- bmstar b = (bmstar)vc;
-
- node n = b->CreateBVConst(binary_repr,2);
- b->BVTypeCheck(n);
- nodestar output = new node(n);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvConstExprFromInt(VC vc,
- int n_bits,
- unsigned int value) {
- bmstar b = (bmstar)vc;
-
- unsigned long long int v = (unsigned long long int)value;
- node n = b->CreateBVConst(n_bits, v);
- b->BVTypeCheck(n);
- nodestar output = new node(n);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvConstExprFromLL(VC vc,
- int n_bits,
- unsigned long long value) {
- bmstar b = (bmstar)vc;
-
- node n = b->CreateBVConst(n_bits, value);
- b->BVTypeCheck(n);
- nodestar output = new node(n);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvConcatExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o =
- b->CreateTerm(BEEV::BVCONCAT,
- l->GetValueWidth()+ r->GetValueWidth(),*l,*r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right){
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVPLUS,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-
-Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right) {
- return vc_bvPlusExpr(vc, 32, left, right);
-}
-
-
-Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVSUB,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-
-Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right) {
- return vc_bvMinusExpr(vc, 32, left, right);
-}
-
-
-Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVMULT,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVDIV,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVMOD,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::SBVDIV,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::SBVMOD,n_bits, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bv32MultExpr(VC vc, Expr left, Expr right) {
- return vc_bvMultExpr(vc, 32, left, right);
-}
-
-
-// unsigned comparators
-Expr vc_bvLtExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVLT, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvLeExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVLE, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvGtExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVGT, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvGeExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVGE, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-// signed comparators
-Expr vc_sbvLtExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVSLT, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_sbvLeExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVSLE, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_sbvGtExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVSGT, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_sbvGeExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateNode(BEEV::BVSGE, *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvUMinusExpr(VC vc, Expr ccc) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
- b->BVTypeCheck(*a);
-
- node o = b->CreateTerm(BEEV::BVUMINUS, a->GetValueWidth(), *a);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-// bitwise operations: these are terms not formulas
-Expr vc_bvAndExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVAND, (*l).GetValueWidth(), *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvOrExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVOR, (*l).GetValueWidth(), *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvXorExpr(VC vc, Expr left, Expr right) {
- bmstar b = (bmstar)vc;
- nodestar l = (nodestar)left;
- nodestar r = (nodestar)right;
-
- b->BVTypeCheck(*l);
- b->BVTypeCheck(*r);
- node o = b->CreateTerm(BEEV::BVXOR, (*l).GetValueWidth(), *l, *r);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvNotExpr(VC vc, Expr ccc) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
-
- b->BVTypeCheck(*a);
- node o = b->CreateTerm(BEEV::BVNEG, a->GetValueWidth(), *a);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
- b->BVTypeCheck(*a);
-
- //convert leftshift to bvconcat
- if(0 != sh_amt) {
- node len = b->CreateBVConst(sh_amt, 0);
- node o = b->CreateTerm(BEEV::BVCONCAT, a->GetValueWidth() + sh_amt, *a, len);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
- }
- else
- return a;
-}
-
-Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
- b->BVTypeCheck(*a);
-
- unsigned int w = a->GetValueWidth();
- //the amount by which you are rightshifting
- //is less-than/equal-to the length of input
- //bitvector
- if(0 < (unsigned)sh_amt && (unsigned)sh_amt <= w) {
- node len = b->CreateBVConst(sh_amt, 0);
- node hi = b->CreateBVConst(32,w-1);
- node low = b->CreateBVConst(32,sh_amt);
- node extract = b->CreateTerm(BEEV::BVEXTRACT,w-sh_amt,*a,hi,low);
-
- node n = b->CreateTerm(BEEV::BVCONCAT, w,len, extract);
- b->BVTypeCheck(n);
- nodestar output = new node(n);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
- }
- else if(sh_amt == 0)
- return a;
- else {
- if(0== w)
- BEEV::FatalError("CInterface: vc_bvRightShiftExpr: cannot have a bitvector of length 0:",*a);
- nodestar output = new node(b->CreateBVConst(w,0));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
- }
-}
-
-/* Same as vc_bvLeftShift only that the answer in 32 bits long */
-Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child) {
- return vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, sh_amt, child), 31, 0);
-}
-
-/* Same as vc_bvRightShift only that the answer in 32 bits long */
-Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child) {
- return vc_bvExtract(vc, vc_bvRightShiftExpr(vc, sh_amt, child), 31, 0);
-}
-
-
-Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child) {
- Expr ifpart;
- Expr thenpart;
- Expr elsepart = vc_trueExpr(vc);
- Expr ite = vc_trueExpr(vc);
-
- for(int count=32; count >= 0; count--){
- if(count != 32) {
- ifpart = vc_eqExpr(vc, sh_amt,
- vc_bvConstExprFromInt(vc, 32, count));
- thenpart = vc_bvExtract(vc,
- vc_bvLeftShiftExpr(vc, count, child),
- 31, 0);
-
- ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
- elsepart = ite;
- }
- else
- elsepart = vc_bvConstExprFromInt(vc,32, 0);
- }
- return ite;
-}
-
-Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) {
- Expr ifpart;
- Expr thenpart;
- Expr elsepart = vc_trueExpr(vc);
- Expr ite = vc_trueExpr(vc);
-
- for(int count=32; count >= 0; count--){
- if(count != 32) {
- ifpart = vc_eqExpr(vc, rhs,
- vc_bvConstExprFromInt(vc, 32, 1 << count));
- thenpart = vc_bvRightShiftExpr(vc, count, child);
- ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
- elsepart = ite;
- } else {
- elsepart = vc_bvConstExprFromInt(vc,32, 0);
- }
- }
- return ite;
-}
-
-Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child) {
- Expr ifpart;
- Expr thenpart;
- Expr elsepart = vc_trueExpr(vc);
- Expr ite = vc_trueExpr(vc);
-
- for(int count=32; count >= 0; count--){
- if(count != 32) {
- ifpart = vc_eqExpr(vc, sh_amt,
- vc_bvConstExprFromInt(vc, 32, count));
- thenpart = vc_bvRightShiftExpr(vc, count, child);
- ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
- elsepart = ite;
- } else {
- elsepart = vc_bvConstExprFromInt(vc,32, 0);
- }
- }
- return ite;
-}
-
-Expr vc_bvExtract(VC vc, Expr ccc, int hi_num, int low_num) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
- b->BVTypeCheck(*a);
-
- node hi = b->CreateBVConst(32,hi_num);
- node low = b->CreateBVConst(32,low_num);
- node o = b->CreateTerm(BEEV::BVEXTRACT,hi_num-low_num+1,*a,hi,low);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvBoolExtract(VC vc, Expr ccc, int bit_num) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
- b->BVTypeCheck(*a);
-
- node bit = b->CreateBVConst(32,bit_num);
- //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
- node zero = b->CreateBVConst(1,0);
- node oo = b->CreateTerm(BEEV::BVEXTRACT,1,*a,bit,bit);
- node o = b->CreateNode(BEEV::EQ,oo,zero);
- b->BVTypeCheck(o);
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-Expr vc_bvSignExtend(VC vc, Expr ccc, int nbits) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)ccc;
-
- //width of the expr which is being sign extended. nbits is the
- //resulting length of the signextended expr
- b->BVTypeCheck(*a);
-
- unsigned exprlen = a->GetValueWidth();
- unsigned outputlen = nbits;
- node n;
- if(exprlen >= outputlen) {
- //extract
- node hi = b->CreateBVConst(32,outputlen-1);
- node low = b->CreateBVConst(32,0);
- n = b->CreateTerm(BEEV::BVEXTRACT,nbits,*a,hi,low);
- b->BVTypeCheck(n);
- }
- else {
- //sign extend
- BEEV::ASTNode width = b->CreateBVConst(32,nbits);
- n = b->CreateTerm(BEEV::BVSX,nbits,*a, width);
- }
-
- b->BVTypeCheck(n);
- nodestar output = new node(n);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
-}
-
-//! Return an int from a constant bitvector expression
-int getBVInt(Expr e) {
- //bmstar b = (bmstar)vc;
- nodestar a = (nodestar)e;
-
- if(BEEV::BVCONST != a->GetKind())
- BEEV::FatalError("CInterface: getBVInt: Attempting to extract int value from a NON-constant BITVECTOR: ",*a);
- return (int)GetUnsignedConst(*a);
-}
-
-//! Return an unsigned int from a constant bitvector expression
-unsigned int getBVUnsigned(Expr e) {
- //bmstar b = (bmstar)vc;
- nodestar a = (nodestar)e;
-
- if(BEEV::BVCONST != a->GetKind())
- BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a);
- return (unsigned int)GetUnsignedConst(*a);
-}
-
-//! Return an unsigned long long int from a constant bitvector expression
-unsigned long long int getBVUnsignedLongLong(Expr e) {
- //bmstar b = (bmstar)vc;
- nodestar a = (nodestar)e;
-
- if(BEEV::BVCONST != a->GetKind())
- BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a);
-#ifdef NATIVE_C_ARITH
- return (unsigned long long int)a->GetBVConst();
-#else
- unsigned* bv = a->GetBVConst();
-
- char * str_bv = (char *)CONSTANTBV::BitVector_to_Bin(bv);
- unsigned long long int tmp = strtoull(str_bv,NULL,2);
- CONSTANTBV::BitVector_Dispose((unsigned char *)str_bv);
- return tmp;
-#endif
-}
-
-
-Expr vc_simplify(VC vc, Expr e) {
- bmstar b = (bmstar)vc;
- nodestar a = (nodestar)e;
-
- if(BEEV::BOOLEAN_TYPE == a->GetType()) {
- nodestar output = new node(b->SimplifyFormula_TopLevel(*a,false));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- b->Begin_RemoveWrites = true;
- output = new node(b->SimplifyFormula_TopLevel(*output,false));
- b->Begin_RemoveWrites = false;
- return output;
- }
- else {
- nodestar output = new node(b->SimplifyTerm(*a));
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- b->Begin_RemoveWrites = true;
- output = new node(b->SimplifyTerm(*output));
- b->Begin_RemoveWrites = false;
- return output;
- }
-}
-
-/* C pointer support: C interface to support C memory arrays in CVCL */
-Expr vc_bvCreateMemoryArray(VC vc, char * arrayName) {
- Type bv8 = vc_bvType(vc,8);
- Type bv32 = vc_bvType(vc,32);
-
- Type malloced_mem0 = vc_arrayType(vc,bv32,bv8);
- return vc_varExpr(vc, arrayName, malloced_mem0);
-}
-
-Expr vc_bvReadMemoryArray(VC vc,
- Expr array,
- Expr byteIndex, int numOfBytes) {
- if(!(numOfBytes > 0))
- BEEV::FatalError("numOfBytes must be greater than 0");
-
- if(numOfBytes == 1)
- return vc_readExpr(vc,array,byteIndex);
- else {
- int count = 1;
- Expr a = vc_readExpr(vc,array,byteIndex);
- while(--numOfBytes > 0) {
- Expr b = vc_readExpr(vc,array,
- /*vc_simplify(vc, */
- vc_bvPlusExpr(vc, 32,
- byteIndex,
- vc_bvConstExprFromInt(vc,32,count)))/*)*/;
- a = vc_bvConcatExpr(vc,b,a);
- count++;
- }
- return a;
- }
-}
-
-Expr vc_bvWriteToMemoryArray(VC vc,
- Expr array, Expr byteIndex,
- Expr element, int numOfBytes) {
- if(!(numOfBytes > 0))
- BEEV::FatalError("numOfBytes must be greater than 0");
-
- int newBitsPerElem = numOfBytes*8;
- if(numOfBytes == 1)
- return vc_writeExpr(vc, array, byteIndex, element);
- else {
- int count = 1;
- int hi = newBitsPerElem - 1;
- int low = newBitsPerElem - 8;
- int low_elem = 0;
- int hi_elem = low_elem + 7;
- Expr c = vc_bvExtract(vc, element, hi_elem, low_elem);
- Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
- while(--numOfBytes > 0) {
- hi = low-1;
- low = low-8;
-
- low_elem = low_elem + 8;
- hi_elem = low_elem + 7;
-
- c = vc_bvExtract(vc, element, hi_elem, low_elem);
- newarray =
- vc_writeExpr(vc, newarray,
- vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)),
- c);
- count++;
- }
- return newarray;
- }
-}
-
-Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value){
- return vc_bvConstExprFromInt(vc, 32, value);
-}
-
-
-#if 0
-static char *val_to_binary_str(unsigned nbits, unsigned long long val) {
- char s[65];
-
- assert(nbits < sizeof s);
- strcpy(s, "");
- while(nbits-- > 0) {
- if((val >> nbits) & 1)
- strcat(s, "1");
- else
- strcat(s, "0");
- }
- return strdup(s);
-}
-#endif
-
-char* exprString(Expr e){
- stringstream ss;
- ((nodestar)e)->PL_Print(ss,0);
- string s = ss.str();
- char *copy = strdup(s.c_str());
- return copy;
-}
-
-char* typeString(Type t){
- stringstream ss;
- ((nodestar)t)->PL_Print(ss,0);
-
- string s = ss.str();
- char *copy = strdup(s.c_str());
- return copy;
-}
-
-Expr getChild(Expr e, int i){
- nodestar a = (nodestar)e;
-
- BEEV::ASTVec c = a->GetChildren();
- if ((unsigned)i < c.size()) {
- BEEV::ASTNode o = c[i];
- nodestar output = new node(o);
- //if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
- }
- else
- BEEV::FatalError("getChild: Error accessing childNode in expression: ",*a);
- return a;
-}
-
-void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg)) {
- BEEV::vc_error_hdlr = error_hdlr;
-}
-
-
-int vc_getHashQueryStateToBuffer(VC vc, Expr query) {
- assert(vc);
- assert(query);
- bmstar b = (bmstar)vc;
- nodestar qry = (nodestar)query;
- BEEV::ASTVec v = b->GetAsserts();
- BEEV::ASTNode out = b->CreateNode(BEEV::AND,b->CreateNode(BEEV::NOT,*qry),v);
- return out.Hash();
-}
-
-Type vc_getType(VC vc, Expr ex) {
- nodestar e = (nodestar)ex;
-
- switch(e->GetType()) {
- case BEEV::BOOLEAN_TYPE:
- return vc_boolType(vc);
- break;
- case BEEV::BITVECTOR_TYPE:
- return vc_bvType(vc,e->GetValueWidth());
- break;
- case BEEV::ARRAY_TYPE: {
- Type typeindex = vc_bvType(vc,e->GetIndexWidth());
- Type typedata = vc_bvType(vc,e->GetValueWidth());
- return vc_arrayType(vc,typeindex,typedata);
- break;
- }
- default:
- BEEV::FatalError("c_interface: vc_GetType: expression with bad typing: please check your expression construction");
- return vc_boolType(vc);
- break;
- }
-}// end of vc_gettype()
-
-//!if e is TRUE then return 1; if e is FALSE then return 0; otherwise
-//return -1
-int vc_isBool(Expr e) {
- nodestar input = (nodestar)e;
- if(BEEV::TRUE == input->GetKind()) {
- return 1;
- }
-
- if(BEEV::FALSE == input->GetKind()) {
- return 0;
- }
-
- return -1;
-}
-
-void vc_Destroy(VC vc) {
- bmstar b = (bmstar)vc;
- // for(std::vector<BEEV::ASTNode *>::iterator it=created_exprs.begin(),
- // itend=created_exprs.end();it!=itend;it++) {
- // BEEV::ASTNode * aaa = *it;
- // delete aaa;
- // }
- delete decls;
- delete b;
-}
-
-void vc_DeleteExpr(Expr e) {
- nodestar input = (nodestar)e;
- //bmstar b = (bmstar)vc;
- delete input;
-}
-
-exprkind_t getExprKind(Expr e) {
- nodestar input = (nodestar)e;
- return (exprkind_t)(input->GetKind());
-}
-
-int getDegree (Expr e) {
- nodestar input = (nodestar)e;
- return input->Degree();
-}
-
-int getBVLength(Expr ex) {
- nodestar e = (nodestar)ex;
-
- if(BEEV::BITVECTOR_TYPE != e->GetType()) {
- BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector");
- }
-
- return e->GetValueWidth();
-}
-
-type_t getType (Expr ex) {
- nodestar e = (nodestar)ex;
-
- return (type_t)(e->GetType());
-}
-
-int getVWidth (Expr ex) {
- nodestar e = (nodestar)ex;
-
- return e->GetValueWidth();
-}
-
-int getIWidth (Expr ex) {
- nodestar e = (nodestar)ex;
-
- return e->GetIndexWidth();
-}
-
-void vc_printCounterExampleFile(VC vc, int fd) {
- fdostream os(fd);
- bmstar b = (bmstar)vc;
- BEEV::print_counterexample = true;
- os << "COUNTEREXAMPLE BEGIN: \n";
- b->PrintCounterExample(true, os);
- os << "COUNTEREXAMPLE END: \n";
-}
-
-const char* exprName(Expr e){
- return ((nodestar)e)->GetName();
-}
-
-int getExprID (Expr ex) {
- BEEV::ASTNode q = (*(nodestar)ex);
-
- return q.GetNodeNum();
-}
diff --git a/stp/c_interface/c_interface.h b/stp/c_interface/c_interface.h
deleted file mode 100644
index a2fa8cd7..00000000
--- a/stp/c_interface/c_interface.h
+++ /dev/null
@@ -1,401 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 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. In particular:
- *
- * - The above copyright notice and this permission notice must appear
- * in all copies of the software and related documentation.
- *
- * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
- * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.
- ********************************************************************/
-// -*- c++ -*-
-#ifndef _cvcl__include__c_interface_h_
-#define _cvcl__include__c_interface_h_
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#ifdef STP_STRONG_TYPING
-#else
- //This gives absolutely no pointer typing at compile-time. Most C
- //users prefer this over stronger typing. User is the king. A
- //stronger typed interface is in the works.
- typedef void* VC;
- typedef void* Expr;
- typedef void* Type;
- typedef void* WholeCounterExample;
-#endif
-
- // o : optimizations
- // c : check counterexample
- // p : print counterexample
- // h : help
- // s : stats
- // v : print nodes
- void vc_setFlags(char c);
-
- //! Flags can be NULL
- VC vc_createValidityChecker(void);
-
- // Basic types
- Type vc_boolType(VC vc);
-
- //! Create an array type
- Type vc_arrayType(VC vc, Type typeIndex, Type typeData);
-
- /////////////////////////////////////////////////////////////////////////////
- // Expr manipulation methods //
- /////////////////////////////////////////////////////////////////////////////
-
- //! Create a variable with a given name and type
- /*! The type cannot be a function type. The var name can contain
- only variables, numerals and underscore. If you use any other
- symbol, you will get a segfault. */
- Expr vc_varExpr(VC vc, char * name, Type type);
-
- //The var name can contain only variables, numerals and
- //underscore. If you use any other symbol, you will get a segfault.
- Expr vc_varExpr1(VC vc, char* name,
- int indexwidth, int valuewidth);
-
- //! Get the expression and type associated with a name.
- /*! If there is no such Expr, a NULL Expr is returned. */
- //Expr vc_lookupVar(VC vc, char* name, Type* type);
-
- //! Get the type of the Expr.
- Type vc_getType(VC vc, Expr e);
-
- int vc_getBVLength(VC vc, Expr e);
-
- //! Create an equality expression. The two children must have the same type.
- Expr vc_eqExpr(VC vc, Expr child0, Expr child1);
-
- // Boolean expressions
-
- // The following functions create Boolean expressions. The children
- // provided as arguments must be of type Boolean (except for the
- // function vc_iteExpr(). In the case of vc_iteExpr() the
- // conditional must always be Boolean, but the ifthenpart
- // (resp. elsepart) can be bit-vector or Boolean type. But, the
- // ifthenpart and elsepart must be both of the same type)
- Expr vc_trueExpr(VC vc);
- Expr vc_falseExpr(VC vc);
- Expr vc_notExpr(VC vc, Expr child);
- Expr vc_andExpr(VC vc, Expr left, Expr right);
- Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes);
- Expr vc_orExpr(VC vc, Expr left, Expr right);
- Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes);
- Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc);
- Expr vc_iffExpr(VC vc, Expr left, Expr right);
- //The output type of vc_iteExpr can be Boolean (formula-level ite)
- //or bit-vector (word-level ite)
- Expr vc_iteExpr(VC vc, Expr conditional, Expr ifthenpart, Expr elsepart);
-
- //Boolean to single bit BV Expression
- Expr vc_boolToBVExpr(VC vc, Expr form);
-
- // Arrays
-
- //! Create an expression for the value of array at the given index
- Expr vc_readExpr(VC vc, Expr array, Expr index);
-
- //! Array update; equivalent to "array WITH [index] := newValue"
- Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue);
-
- // Expr I/O
- //! Expr vc_parseExpr(VC vc, char* s);
-
- //! Prints 'e' to stdout.
- void vc_printExpr(VC vc, Expr e);
-
- //! Prints 'e' into an open file descriptor 'fd'
- void vc_printExprFile(VC vc, Expr e, int fd);
-
- //! Prints state of 'vc' into malloc'd buffer '*buf' and stores the
- // length into '*len'. It is the responsibility of the caller to
- // free the buffer.
- //void vc_printStateToBuffer(VC vc, char **buf, unsigned long *len);
-
- //! Prints 'e' to malloc'd buffer '*buf'. Sets '*len' to the length of
- // the buffer. It is the responsibility of the caller to free the buffer.
- void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len);
-
- //! Prints counterexample to stdout.
- void vc_printCounterExample(VC vc);
-
- //! Prints variable declarations to stdout.
- void vc_printVarDecls(VC vc);
-
- //! Prints asserts to stdout. The flag simplify_print must be set to
- //"1" if you wish simplification to occur dring printing. It must be
- //set to "0" otherwise
- void vc_printAsserts(VC vc, int simplify_print);
-
- //! Prints the state of the query to malloc'd buffer '*buf' and
- //stores ! the length of the buffer to '*len'. It is the
- //responsibility of the caller to free the buffer. The flag
- //simplify_print must be set to "1" if you wish simplification to
- //occur dring printing. It must be set to "0" otherwise
- void vc_printQueryStateToBuffer(VC vc, Expr e,
- char **buf, unsigned long *len, int simplify_print);
-
- //! Similar to vc_printQueryStateToBuffer()
- void vc_printCounterExampleToBuffer(VC vc, char **buf,unsigned long *len);
-
- //! Prints query to stdout.
- void vc_printQuery(VC vc);
-
- /////////////////////////////////////////////////////////////////////////////
- // Context-related methods //
- /////////////////////////////////////////////////////////////////////////////
-
- //! Assert a new formula in the current context.
- /*! The formula must have Boolean type. */
- void vc_assertFormula(VC vc, Expr e);
-
- //! Simplify e with respect to the current context
- Expr vc_simplify(VC vc, Expr e);
-
- //! Check validity of e in the current context. e must be a FORMULA
- //
- //if returned 0 then input is INVALID.
- //
- //if returned 1 then input is VALID
- //
- //if returned 2 then ERROR
- int vc_query(VC vc, Expr e);
-
- //! Return the counterexample after a failed query.
- Expr vc_getCounterExample(VC vc, Expr e);
-
- //! get size of counterexample, i.e. the number of variables/array
- //locations in the counterexample.
- int vc_counterexample_size(VC vc);
-
- //! Checkpoint the current context and increase the scope level
- void vc_push(VC vc);
-
- //! Restore the current context to its state at the last checkpoint
- void vc_pop(VC vc);
-
- //! Return an int from a constant bitvector expression
- int getBVInt(Expr e);
- //! Return an unsigned int from a constant bitvector expression
- unsigned int getBVUnsigned(Expr e);
- //! Return an unsigned long long int from a constant bitvector expressions
- unsigned long long int getBVUnsignedLongLong(Expr e);
-
- /**************************/
- /* BIT VECTOR OPERATIONS */
- /**************************/
- Type vc_bvType(VC vc, int no_bits);
- Type vc_bv32Type(VC vc);
-
- Expr vc_bvConstExprFromStr(VC vc, char* binary_repr);
- Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value);
- Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value);
- Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
-
- Expr vc_bvConcatExpr(VC vc, Expr left, Expr right);
- Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right);
- Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right);
- Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right);
- Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right);
- Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right);
- Expr vc_bv32MultExpr(VC vc, Expr left, Expr right);
- // left divided by right i.e. left/right
- Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right);
- // left modulo right i.e. left%right
- Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right);
- // signed left divided by right i.e. left/right
- Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right);
- // signed left modulo right i.e. left%right
- Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right);
-
- Expr vc_bvLtExpr(VC vc, Expr left, Expr right);
- Expr vc_bvLeExpr(VC vc, Expr left, Expr right);
- Expr vc_bvGtExpr(VC vc, Expr left, Expr right);
- Expr vc_bvGeExpr(VC vc, Expr left, Expr right);
-
- Expr vc_sbvLtExpr(VC vc, Expr left, Expr right);
- Expr vc_sbvLeExpr(VC vc, Expr left, Expr right);
- Expr vc_sbvGtExpr(VC vc, Expr left, Expr right);
- Expr vc_sbvGeExpr(VC vc, Expr left, Expr right);
-
- Expr vc_bvUMinusExpr(VC vc, Expr child);
-
- // bitwise operations: these are terms not formulas
- Expr vc_bvAndExpr(VC vc, Expr left, Expr right);
- Expr vc_bvOrExpr(VC vc, Expr left, Expr right);
- Expr vc_bvXorExpr(VC vc, Expr left, Expr right);
- Expr vc_bvNotExpr(VC vc, Expr child);
-
- Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child);
- Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child);
- /* Same as vc_bvLeftShift only that the answer in 32 bits long */
- Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child);
- /* Same as vc_bvRightShift only that the answer in 32 bits long */
- Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child);
- Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child);
- Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child);
- Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs);
-
- Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no);
-
- //accepts a bitvector and position, and returns a boolean
- //corresponding to that position. More precisely, it return the
- //equation (x[bit_no:bit_no] = 0)
- //FIXME = 1 ?
- Expr vc_bvBoolExtract(VC vc, Expr x, int bit_no);
- Expr vc_bvSignExtend(VC vc, Expr child, int nbits);
-
- /*C pointer support: C interface to support C memory arrays in CVCL */
- Expr vc_bvCreateMemoryArray(VC vc, char * arrayName);
- Expr vc_bvReadMemoryArray(VC vc,
- Expr array, Expr byteIndex, int numOfBytes);
- Expr vc_bvWriteToMemoryArray(VC vc,
- Expr array, Expr byteIndex,
- Expr element, int numOfBytes);
- Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
-
- // return a string representation of the Expr e. The caller is responsible
- // for deallocating the string with free()
- char* exprString(Expr e);
-
- // return a string representation of the Type t. The caller is responsible
- // for deallocating the string with free()
- char* typeString(Type t);
-
- Expr getChild(Expr e, int i);
-
- //1.if input expr is TRUE then the function returns 1;
- //
- //2.if input expr is FALSE then function returns 0;
- //
- //3.otherwise the function returns -1
- int vc_isBool(Expr e);
-
- /* Register the given error handler to be called for each fatal error.*/
- void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg));
-
- int vc_getHashQueryStateToBuffer(VC vc, Expr query);
-
- //destroys the STP instance, and removes all the created expressions
- void vc_Destroy(VC vc);
-
- //deletes the expression e
- void vc_DeleteExpr(Expr e);
-
- //Get the whole counterexample from the current context
- WholeCounterExample vc_getWholeCounterExample(VC vc);
-
- //Get the value of a term expression from the CounterExample
- Expr vc_getTermFromCounterExample(VC vc, Expr e, WholeCounterExample c);
-
- //Kinds of Expr
- enum exprkind_t{
- UNDEFINED,
- SYMBOL,
- BVCONST,
- BVNEG,
- BVCONCAT,
- BVOR,
- BVAND,
- BVXOR,
- BVNAND,
- BVNOR,
- BVXNOR,
- BVEXTRACT,
- BVLEFTSHIFT,
- BVRIGHTSHIFT,
- BVSRSHIFT,
- BVVARSHIFT,
- BVPLUS,
- BVSUB,
- BVUMINUS,
- BVMULTINVERSE,
- BVMULT,
- BVDIV,
- BVMOD,
- SBVDIV,
- SBVMOD,
- BVSX,
- BOOLVEC,
- ITE,
- BVGETBIT,
- BVLT,
- BVLE,
- BVGT,
- BVGE,
- BVSLT,
- BVSLE,
- BVSGT,
- BVSGE,
- EQ,
- NEQ,
- FALSE,
- TRUE,
- NOT,
- AND,
- OR,
- NAND,
- NOR,
- XOR,
- IFF,
- IMPLIES,
- READ,
- WRITE,
- ARRAY,
- BITVECTOR,
- BOOLEAN
- };
-
- // type of expression
- enum type_t {
- BOOLEAN_TYPE = 0,
- BITVECTOR_TYPE,
- ARRAY_TYPE,
- UNKNOWN_TYPE
- };
-
- // get the kind of the expression
- exprkind_t getExprKind (Expr e);
-
- // get the number of children nodes
- int getDegree (Expr e);
-
- // get the bv length
- int getBVLength(Expr e);
-
- // get expression type
- type_t getType (Expr e);
-
- // get value bit width
- int getVWidth (Expr e);
-
- // get index bit width
- int getIWidth (Expr e);
-
- // Prints counterexample to an open file descriptor 'fd'
- void vc_printCounterExampleFile(VC vc, int fd);
-
- // get name of expression. must be a variable.
- const char* exprName(Expr e);
-
- // get the node ID of an Expr.
- int getExprID (Expr ex);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-
diff --git a/stp/c_interface/fdstream.h b/stp/c_interface/fdstream.h
deleted file mode 100644
index 2cff613c..00000000
--- a/stp/c_interface/fdstream.h
+++ /dev/null
@@ -1,186 +0,0 @@
-/*! @brief The following code declares classes to read from and write to
- * file descriptore or file handles.
- *
- * See
- * http://www.josuttis.com/cppcode
- * for details and the latest version.
- *
- * - open:
- * - integrating BUFSIZ on some systems?
- * - optimized reading of multiple characters
- * - stream for reading AND writing
- * - i18n
- *
- * (C) Copyright Nicolai M. Josuttis 2001.
- * Permission to copy, use, modify, sell and distribute this software
- * is granted provided this copyright notice appears in all copies.
- * This software is provided "as is" without express or implied
- * warranty, and with no claim as to its suitability for any purpose.
- *
- * Version: Jul 28, 2002
- * History:
- * Jul 28, 2002: bugfix memcpy() => memmove()
- * fdinbuf::underflow(): cast for return statements
- * Aug 05, 2001: first public version
- */
-#ifndef BOOST_FDSTREAM_HPP
-#define BOOST_FDSTREAM_HPP
-
-#include <istream>
-#include <ostream>
-#include <streambuf>
-
-
-// for EOF:
-#include <cstdio>
-// for memmove():
-#include <cstring>
-
-
-// low-level read and write functions
-#ifdef _MSC_VER
-# include <io.h>
-#else
-# include <unistd.h>
-//extern "C" {
-// int write (int fd, const char* buf, int num);
-// int read (int fd, char* buf, int num);
-//}
-#endif
-
-
-// BEGIN namespace BOOST
-namespace std {
-
-
-/************************************************************
- * fdostream
- * - a stream that writes on a file descriptor
- ************************************************************/
-
-
-class fdoutbuf : public std::streambuf {
- protected:
- int fd; // file descriptor
- public:
- // constructor
- fdoutbuf (int _fd) : fd(_fd) {
- }
- protected:
- // write one character
- virtual int_type overflow (int_type c) {
- if (c != EOF) {
- char z = c;
- if (write (fd, &z, 1) != 1) {
- return EOF;
- }
- }
- return c;
- }
- // write multiple characters
- virtual
- std::streamsize xsputn (const char* s,
- std::streamsize num) {
- return write(fd,s,num);
- }
-};
-
-class fdostream : public std::ostream {
- protected:
- fdoutbuf buf;
- public:
- fdostream (int fd) : std::ostream(0), buf(fd) {
- rdbuf(&buf);
- }
-};
-
-
-/************************************************************
- * fdistream
- * - a stream that reads on a file descriptor
- ************************************************************/
-
-class fdinbuf : public std::streambuf {
- protected:
- int fd; // file descriptor
- protected:
- /* data buffer:
- * - at most, pbSize characters in putback area plus
- * - at most, bufSize characters in ordinary read buffer
- */
- static const int pbSize = 4; // size of putback area
- static const int bufSize = 1024; // size of the data buffer
- char buffer[bufSize+pbSize]; // data buffer
-
- public:
- /* constructor
- * - initialize file descriptor
- * - initialize empty data buffer
- * - no putback area
- * => force underflow()
- */
- fdinbuf (int _fd) : fd(_fd) {
- setg (buffer+pbSize, // beginning of putback area
- buffer+pbSize, // read position
- buffer+pbSize); // end position
- }
-
- protected:
- // insert new characters into the buffer
- virtual int_type underflow () {
-#ifndef _MSC_VER
- using std::memmove;
-#endif
-
- // is read position before end of buffer?
- if (gptr() < egptr()) {
- return traits_type::to_int_type(*gptr());
- }
-
- /* process size of putback area
- * - use number of characters read
- * - but at most size of putback area
- */
- int numPutback;
- numPutback = gptr() - eback();
- if (numPutback > pbSize) {
- numPutback = pbSize;
- }
-
- /* copy up to pbSize characters previously read into
- * the putback area
- */
- memmove (buffer+(pbSize-numPutback), gptr()-numPutback,
- numPutback);
-
- // read at most bufSize new characters
- int num;
- num = read (fd, buffer+pbSize, bufSize);
- if (num <= 0) {
- // ERROR or EOF
- return EOF;
- }
-
- // reset buffer pointers
- setg (buffer+(pbSize-numPutback), // beginning of putback area
- buffer+pbSize, // read position
- buffer+pbSize+num); // end of buffer
-
- // return next character
- return traits_type::to_int_type(*gptr());
- }
-};
-
-class fdistream : public std::istream {
- protected:
- fdinbuf buf;
- public:
- fdistream (int fd) : std::istream(0), buf(fd) {
- rdbuf(&buf);
- }
-};
-
-
-} // END namespace boost
-
-#endif /*BOOST_FDSTREAM_HPP*/
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-23 19:59:02 +0000