Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 401 insertions, 0 deletions

diff --git a/stp/c_interface/c_interface.h b/stp/c_interface/c_interface.h
new file mode 100644
index 00000000..a2fa8cd7
--- /dev/null
+++ b/stp/c_interface/c_interface.h
@@ -0,0 +1,401 @@
+/********************************************************************
+ * 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
+
+