diff options
Diffstat (limited to 'stp/c_interface/c_interface.h')
| -rw-r--r-- | stp/c_interface/c_interface.h | 401 |
1 files changed, 0 insertions, 401 deletions
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 - - |