1 /********************************************************************
2 * AUTHORS: Vijay Ganesh, Andrew V. Jones
3 *
4 * BEGIN DATE: November, 2005
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24 #include "stp/c_interface.h"
25
26 #include <cassert>
27 #include <cstdio>
28 #include <cstdlib>
29
30 #include "stp/Interface/fdstream.h"
31 #include "stp/Parser/parser.h"
32 #include "stp/Printer/printers.h"
33 #include "stp/cpp_interface.h"
34 #include "stp/Util/GitSHA1.h"
35 // FIXME: External library
36 #include "extlib-abc/cnf_short.h"
37
38 using std::cout;
39 using std::ostream;
40 using std::stringstream;
41 using std::string;
42 using std::fdostream;
43 using std::endl;
44
45 // GLOBAL FUNCTION: parser
46 extern int cvcparse(void*);
47 extern int smtparse(void*);
48
49 /* wraps get_git_version_sha in stp namespace */
get_git_version_sha(void)50 const char* get_git_version_sha(void)
51 {
52 return stp::get_git_version_sha();
53 }
54
55 /* wraps get_git_version_tag in stp namespace */
get_git_version_tag(void)56 const char* get_git_version_tag(void)
57 {
58 return stp::get_git_version_tag();
59 }
60
61 /* wraps get_compilation_env in stp namespace */
get_compilation_env(void)62 const char* get_compilation_env(void)
63 {
64 return stp::get_compilation_env();
65 }
66
67 // TODO remove this, it's really ugly
vc_setFlags(VC vc,char c,int)68 void vc_setFlags(VC vc, char c, int /*param_value*/)
69 {
70 process_argument(c, vc);
71 }
72
73 // TODO remove this, it's really ugly
vc_setFlag(VC vc,char c)74 void vc_setFlag(VC vc, char c)
75 {
76 process_argument(c, vc);
77 }
78
vc_setInterfaceFlags(VC vc,enum ifaceflag_t f,int param_value)79 void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value)
80 {
81 stp::STP* stp_i = (stp::STP*)vc;
82 stp::STPMgr* b = stp_i->bm;
83 switch (f)
84 {
85 case EXPRDELETE:
86 b->UserFlags.cinterface_exprdelete_on_flag = param_value != 0;
87 break;
88 case MS:
89 b->UserFlags.solver_to_use = stp::UserDefinedFlags::MINISAT_SOLVER;
90 break;
91 case SMS:
92 b->UserFlags.solver_to_use =
93 stp::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER;
94 break;
95 case CMS4:
96 b->UserFlags.solver_to_use = stp::UserDefinedFlags::CRYPTOMINISAT5_SOLVER;
97 break;
98 case RISS:
99 b->UserFlags.solver_to_use = stp::UserDefinedFlags::RISS_SOLVER;
100 break;
101 case MSP:
102 //Array-based Minisat has been replaced with normal MiniSat
103 b->UserFlags.solver_to_use = stp::UserDefinedFlags::MINISAT_SOLVER;
104 break;
105 default:
106 stp::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized flag\n");
107 break;
108 }
109 }
110
111 // Division is now always total
make_division_total(VC)112 void make_division_total(VC /*vc*/)
113 {
114 }
115
116 // Create a validity Checker.
vc_createValidityChecker(void)117 VC vc_createValidityChecker(void)
118 {
119 CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
120 if (0 != c)
121 {
122 cout << CONSTANTBV::BitVector_Error(c) << endl;
123 return 0;
124 }
125
126 stp::STPMgr* bm = new stp::STPMgr();
127
128 bm->defaultNodeFactory =
129 new SimplifyingNodeFactory(*(bm->hashingNodeFactory), *bm);
130
131 stp::Simplifier* simp = new stp::Simplifier(bm);
132 stp::BVSolver* bvsolver = new stp::BVSolver(bm, simp);
133 stp::ToSAT* tosat = new stp::ToSAT(bm);
134 stp::ArrayTransformer* arrayTransformer = new stp::ArrayTransformer(bm, simp);
135 stp::AbsRefine_CounterExample* Ctr_Example =
136 new stp::AbsRefine_CounterExample(bm, simp, arrayTransformer);
137
138 stp::STP* stpObj =
139 new stp::STP(bm, simp, bvsolver, arrayTransformer, tosat, Ctr_Example);
140
141 // created_exprs.clear();
142 vc_setFlags(stpObj, 'd');
143 return (VC)stpObj;
144 }
145
146 // Expr I/O
vc_printExpr(VC vc,Expr e)147 void vc_printExpr(VC vc, Expr e)
148 {
149 // do not print in lisp mode
150 stp::STP* stp_i = (stp::STP*)vc;
151 stp::ASTNode q = (*(stp::ASTNode*)e);
152 stp::STPMgr* b = stp_i->bm;
153 q.PL_Print(cout, b);
154 }
155
vc_printSMTLIB(VC vc,Expr e)156 char* vc_printSMTLIB(VC vc, Expr e)
157 {
158 stp::STP* stp_i = (stp::STP*)vc;
159 stp::STPMgr* b = stp_i->bm;
160
161 stringstream ss;
162 printer::SMTLIB1_PrintBack(ss, *((stp::ASTNode*)e), b);
163 string s = ss.str();
164 char* copy = strdup(s.c_str());
165 return copy;
166 }
167
168 // prints Expr 'e' to stdout as C code
vc_printExprCCode(VC vc,Expr e)169 void vc_printExprCCode(VC vc, Expr e)
170 {
171 stp::STP* stp_i = (stp::STP*)vc;
172 stp::STPMgr* b = stp_i->bm;
173 stp::ASTNode q = (*(stp::ASTNode*)e);
174
175 // print variable declarations
176 stp::ASTVec declsFromParser = (stp::ASTVec)b->decls;
177
178 for (stp::ASTVec::iterator it = declsFromParser.begin(),
179 itend = declsFromParser.end();
180 it != itend; it++)
181 {
182 if (stp::BITVECTOR_TYPE == it->GetType())
183 {
184 const char* name = it->GetName();
185 unsigned int bitWidth = it->GetValueWidth();
186 assert(bitWidth % 8 == 0);
187 unsigned int byteWidth = bitWidth / 8;
188 cout << "unsigned char " << name << "[" << byteWidth << "];" << endl;
189 }
190 else
191 {
192 // vc_printExprCCode: unsupported decl. type
193 assert(0);
194 }
195 }
196
197 cout << endl;
198
199 // print constraints and assert
200 printer::C_Print(cout, q, b);
201 }
202
vc_printExprFile(VC vc,Expr e,int fd)203 void vc_printExprFile(VC vc, Expr e, int fd)
204 {
205 stp::STP* stp_i = (stp::STP*)vc;
206 stp::STPMgr* b = stp_i->bm;
207
208 fdostream os(fd);
209
210 ((stp::ASTNode*)e)->PL_Print(os, b);
211 // os.flush();
212 }
213
vc_printVarDeclsToStream(VC vc,ostream & os)214 static void vc_printVarDeclsToStream(VC vc, ostream& os)
215 {
216 stp::STP* stp_i = (stp::STP*)vc;
217 stp::STPMgr* b = stp_i->bm;
218
219 for (stp::ASTVec::iterator i = b->decls.begin(), iend = b->decls.end();
220 i != iend; i++)
221 {
222 stp::ASTNode a = *i;
223 switch (a.GetType())
224 {
225 case stp::BITVECTOR_TYPE:
226 a.PL_Print(os, b);
227 os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;
228 break;
229 case stp::ARRAY_TYPE:
230 a.PL_Print(os, b);
231 os << " : ARRAY "
232 << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";
233 os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;
234 break;
235 case stp::BOOLEAN_TYPE:
236 a.PL_Print(os, b);
237 os << " : BOOLEAN;" << endl;
238 break;
239 default:
240 stp::FatalError("vc_printDeclsToStream: Unsupported type", a);
241 break;
242 }
243 }
244 }
245
vc_printVarDecls(VC vc)246 void vc_printVarDecls(VC vc)
247 {
248 vc_printVarDeclsToStream(vc, cout);
249 }
250
vc_clearDecls(VC vc)251 void vc_clearDecls(VC vc)
252 {
253 stp::STP* stp_i = (stp::STP*)vc;
254 stp::STPMgr* b = stp_i->bm;
255 b->decls.clear();
256 }
257
vc_printAssertsToStream(VC vc,ostream & os,int simplify_print)258 static void vc_printAssertsToStream(VC vc, ostream& os, int simplify_print)
259 {
260 stp::STP* stp_i = (stp::STP*)vc;
261 stp::STPMgr* b = stp_i->bm;
262 stp::ASTVec v = b->GetAsserts();
263 stp::Simplifier* simp = new stp::Simplifier(b);
264 for (stp::ASTVec::iterator i = v.begin(), iend = v.end(); i != iend; i++)
265 {
266 stp::ASTNode q =
267 (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(*i, false) : *i;
268 q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(q, false) : q;
269 os << "ASSERT( ";
270 q.PL_Print(os, b);
271 os << ");" << endl;
272 }
273 delete simp;
274 simp = NULL;
275 }
276
vc_printAsserts(VC vc,int simplify_print)277 void vc_printAsserts(VC vc, int simplify_print)
278 {
279 vc_printAssertsToStream(vc, cout, simplify_print);
280 }
281
vc_printQueryStateToBuffer(VC vc,Expr e,char ** buf,unsigned long * len,int simplify_print)282 void vc_printQueryStateToBuffer(VC vc, Expr e, char** buf, unsigned long* len,
283 int simplify_print)
284 {
285 stp::STP* stp_i = (stp::STP*)vc;
286 stp::STPMgr* b = stp_i->bm;
287 assert(vc);
288 assert(e);
289 assert(buf);
290 assert(len);
291
292 stp::Simplifier* simp = new stp::Simplifier(b);
293
294 // formate the state of the query
295 stringstream os;
296 vc_printVarDeclsToStream(vc, os);
297 os << "%----------------------------------------------------" << endl;
298 vc_printAssertsToStream(vc, os, simplify_print);
299 os << "%----------------------------------------------------" << endl;
300 os << "QUERY( ";
301 stp::ASTNode q =
302 (simplify_print == 1)
303 ? simp->SimplifyFormula_TopLevel(*((stp::ASTNode*)e), false)
304 : *(stp::ASTNode*)e;
305 q.PL_Print(os, b);
306 os << " );" << endl;
307
308 delete simp;
309 simp = NULL;
310
311 // convert to a c buffer
312 string s = os.str();
313 const char* cstr = s.c_str();
314 unsigned long size = s.size() + 1; // number of chars + terminating null
315 *buf = (char*)malloc(size);
316 if (!(*buf))
317 {
318 fprintf(stderr, "malloc(%lu) failed.", size);
319 assert(*buf);
320 }
321 *len = size;
322 memcpy(*buf, cstr, size);
323 }
324
vc_printCounterExampleToBuffer(VC vc,char ** buf,unsigned long * len)325 void vc_printCounterExampleToBuffer(VC vc, char** buf, unsigned long* len)
326 {
327 assert(vc);
328 assert(buf);
329 assert(len);
330
331 stp::STP* stp_i = (stp::STP*)vc;
332 stp::STPMgr* b = stp_i->bm;
333 stp::AbsRefine_CounterExample* ce =
334 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
335
336 // formate the state of the query
337 std::ostringstream os;
338 bool currentPrint = b->UserFlags.print_counterexample_flag;
339 b->UserFlags.print_counterexample_flag = true;
340 os << "COUNTEREXAMPLE BEGIN: \n";
341 ce->PrintCounterExample(true, os);
342 os << "COUNTEREXAMPLE END: \n";
343 b->UserFlags.print_counterexample_flag = currentPrint;
344
345 // convert to a c buffer
346 string s = os.str();
347 const char* cstr = s.c_str();
348 unsigned long size = s.size() + 1; // number of chars + terminating null
349 *buf = (char*)malloc(size);
350 if (!(*buf))
351 {
352 fprintf(stderr, "malloc(%lu) failed.", size);
353 assert(*buf);
354 }
355 *len = size;
356 memcpy(*buf, cstr, size);
357 }
358
vc_printExprToBuffer(VC vc,Expr e,char ** buf,unsigned long * len)359 void vc_printExprToBuffer(VC vc, Expr e, char** buf, unsigned long* len)
360 {
361 stp::STP* stp_i = (stp::STP*)vc;
362 stp::STPMgr* b = stp_i->bm;
363 stp::ASTNode q = *((stp::ASTNode*)e);
364
365 stringstream os;
366 q.PL_Print(os, b);
367 string s = os.str();
368 const char* cstr = s.c_str();
369 unsigned long size = s.size() + 1; // number of chars + terminating null
370 *buf = (char*)malloc(size);
371 *len = size;
372 memcpy(*buf, cstr, size);
373 }
374
vc_printQuery(VC vc)375 void vc_printQuery(VC vc)
376 {
377 stp::STP* stp_i = (stp::STP*)vc;
378 stp::STPMgr* b = stp_i->bm;
379
380 ostream& os = std::cout;
381 os << "QUERY(";
382 stp::ASTNode q = b->GetQuery();
383 q.PL_Print(os, b);
384 os << ");" << endl;
385 }
386
persistNode(VC vc,stp::ASTNode n)387 stp::ASTNode* persistNode(VC vc, stp::ASTNode n)
388 {
389 stp::STP* stp_i = (stp::STP*)vc;
390 stp::STPMgr* b = stp_i->bm;
391
392 stp::ASTNode* np = new stp::ASTNode(n);
393 if (b->UserFlags.cinterface_exprdelete_on_flag)
394 b->persist.push_back(np);
395 return np;
396 }
397
398 /////////////////////////////////////////////////////////////////////////////
399 // Array-related methods //
400 /////////////////////////////////////////////////////////////////////////////
401 //! Create an array type
vc_arrayType(VC vc,Type typeIndex,Type typeData)402 Type vc_arrayType(VC vc, Type typeIndex, Type typeData)
403 {
404 stp::STP* stp_i = (stp::STP*)vc;
405 stp::STPMgr* b = stp_i->bm;
406 stp::ASTNode* ti = (stp::ASTNode*)typeIndex;
407 stp::ASTNode* td = (stp::ASTNode*)typeData;
408
409 if (!(ti->GetKind() == stp::BITVECTOR && (*ti)[0].GetKind() == stp::BVCONST))
410 {
411 stp::FatalError("Tyring to build array whose"
412 "indextype i is not a BITVECTOR, where i = ",
413 *ti);
414 }
415 if (!(td->GetKind() == stp::BITVECTOR && (*td)[0].GetKind() == stp::BVCONST))
416 {
417 stp::FatalError("Trying to build an array whose"
418 "valuetype v is not a BITVECTOR. where a = ",
419 *td);
420 }
421 stp::ASTNode output = b->CreateNode(stp::ARRAY, (*ti)[0], (*td)[0]);
422
423 return persistNode(vc, output);
424 }
425
426 //! Create an expression for the value of array at the given index
vc_readExpr(VC vc,Expr array,Expr index)427 Expr vc_readExpr(VC vc, Expr array, Expr index)
428 {
429 stp::STP* stp_i = (stp::STP*)vc;
430 stp::STPMgr* b = stp_i->bm;
431 stp::ASTNode* a = (stp::ASTNode*)array;
432 stp::ASTNode* i = (stp::ASTNode*)index;
433
434 assert(BVTypeCheck(*a));
435 assert(BVTypeCheck(*i));
436 stp::ASTNode o = b->CreateTerm(stp::READ, a->GetValueWidth(), *a, *i);
437 assert(BVTypeCheck(o));
438
439 stp::ASTNode* output = new stp::ASTNode(o);
440 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
441 return output;
442 }
443
444 // //! Array update; equivalent to "array WITH [index] := newValue"
vc_writeExpr(VC vc,Expr array,Expr index,Expr newValue)445 Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue)
446 {
447 stp::STP* stp_i = (stp::STP*)vc;
448 stp::STPMgr* b = stp_i->bm;
449 stp::ASTNode* a = (stp::ASTNode*)array;
450 stp::ASTNode* i = (stp::ASTNode*)index;
451 stp::ASTNode* n = (stp::ASTNode*)newValue;
452
453 assert(BVTypeCheck(*a));
454 assert(BVTypeCheck(*i));
455 assert(BVTypeCheck(*n));
456 stp::ASTNode o = b->CreateTerm(stp::WRITE, a->GetValueWidth(), *a, *i, *n);
457 o.SetIndexWidth(a->GetIndexWidth());
458 assert(BVTypeCheck(o));
459
460 stp::ASTNode* output = new stp::ASTNode(o);
461 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
462 return output;
463 }
464
465 /////////////////////////////////////////////////////////////////////////////
466 // Context-related methods //
467 /////////////////////////////////////////////////////////////////////////////
468 //! Assert a new formula in the current context.
469 /*! The formula must have Boolean type. */
vc_assertFormula(VC vc,Expr e)470 void vc_assertFormula(VC vc, Expr e)
471 {
472 stp::STP* stp_i = (stp::STP*)vc;
473 stp::STPMgr* b = stp_i->bm;
474 stp::ASTNode* a = (stp::ASTNode*)e;
475
476 if (!stp::is_Form_kind(a->GetKind()))
477 stp::FatalError("Trying to assert a NON formula: ", *a);
478
479 assert(BVTypeCheck(*a));
480 b->AddAssert(*a);
481 }
482
483 //! Check validity of e in the current context. e must be a FORMULA
484 //
485 // if returned 0 then input is INVALID.
486 //
487 // if returned 1 then input is VALID
488 //
489 // if returned 2 then ERROR
490 //
491 //! Check validity of e in the current context.
492 /*! If the result is true, then the resulting context is the same as
493 * the starting context. If the result is false, then the resulting
494 * context is a context in which e is false. e must have Boolean
495 * type. */
vc_query(VC vc,Expr e)496 int vc_query(VC vc, Expr e)
497 {
498 return vc_query_with_timeout(vc, e, -1);
499 }
500
vc_query_with_timeout(VC vc,Expr e,int timeout_ms)501 int vc_query_with_timeout(VC vc, Expr e, int timeout_ms)
502 {
503 stp::STP* stp_i = (stp::STP*)vc;
504 stp::ASTNode* a = (stp::ASTNode*)e;
505 stp::STPMgr* b = stp_i->bm;
506
507 if (!stp::is_Form_kind(a->GetKind()))
508 {
509 stp::FatalError("CInterface: Trying to QUERY a NON formula: ", *a);
510 }
511
512 assert(BVTypeCheck(*a));
513 // Cached in case someone runs PrintQuery()
514 b->SetQuery(*a);
515
516 stp_i->ClearAllTables();
517
518 const stp::ASTVec v = b->GetAsserts();
519 stp::ASTNode o;
520 int output;
521 stp_i->bm->UserFlags.timeout_max_conflicts = timeout_ms;
522 if (!v.empty())
523 {
524 if (v.size() == 1)
525 {
526 output = stp_i->TopLevelSTP(v[0], *a);
527 }
528 else
529 {
530 output = stp_i->TopLevelSTP(b->CreateNode(stp::AND, v), *a);
531 }
532 }
533 else
534 {
535 output = stp_i->TopLevelSTP(b->CreateNode(stp::TRUE), *a);
536 }
537
538 return output;
539 }
540
541 // int vc_absRefineQuery(VC vc, Expr e) {
542 // stp::STP* stp_i = (stp::STP*)vc;
543 // stp::ASTNode* a = (stp::ASTNode*)e;
544 // stp::STPMgr* b = stp_i->bm;
545
546 // if(!stp::is_Form_kind(a->GetKind()))
547 // stp::FatalError("CInterface: Trying to QUERY a NON formula: ",*a);
548
549 // //a->LispPrint(cout, 0);
550 // //printf("##################################################\n");
551 // BVTypeCheck(*a);
552 // b->AddQuery(*a);
553
554 // const stp::ASTVec v = b->GetAsserts();
555 // stp::ASTNode o;
556 // if(!v.empty()) {
557 // if(v.size()==1)
558 // return b->TopLevelSTP(v[0],*a);
559 // else
560 // return b->TopLevelSTP(b->CreateNode(stp::AND,v),*a);
561 // }
562 // else
563 // return b->TopLevelSTP(b->CreateNode(stp::TRUE),*a);
564 // }
565
vc_push(VC vc)566 void vc_push(VC vc)
567 {
568 stp::STP* stp_i = (stp::STP*)vc;
569 stp::STPMgr* b = stp_i->bm;
570 stp_i->ClearAllTables();
571 b->Push();
572 }
573
574 //NB, doesn't remove symbols from decls, so they will be kept alive.
vc_pop(VC vc)575 void vc_pop(VC vc)
576 {
577 stp::STP* stp_i = (stp::STP*)vc;
578 stp::STPMgr* b = stp_i->bm;
579 b->Pop();
580 }
581
vc_printCounterExample(VC vc)582 void vc_printCounterExample(VC vc)
583 {
584 stp::STP* stp_i = (stp::STP*)vc;
585 stp::STPMgr* b = stp_i->bm;
586 stp::AbsRefine_CounterExample* ce =
587 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
588
589 bool currentPrint = b->UserFlags.print_counterexample_flag;
590 b->UserFlags.print_counterexample_flag = true;
591 cout << "COUNTEREXAMPLE BEGIN: \n";
592 ce->PrintCounterExample(true);
593 cout << "COUNTEREXAMPLE END: \n";
594 b->UserFlags.print_counterexample_flag = currentPrint;
595 }
596
597 // //! Return the counterexample after a failed query.
598 // /*! This method should only be called after a query which returns
599 // * false. It will try to return the simplest possible set of
600 // * assertions which are sufficient to make the queried expression
601 // * false. The caller is responsible for freeing the array when
602 // * finished with it.
603 // */
604
vc_getCounterExample(VC vc,Expr e)605 Expr vc_getCounterExample(VC vc, Expr e)
606 {
607 stp::STP* stp_i = (stp::STP*)vc;
608 stp::ASTNode* a = (stp::ASTNode*)e;
609
610 stp::AbsRefine_CounterExample* ce =
611 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
612 stp::ASTNode* output = new stp::ASTNode(ce->GetCounterExample(*a));
613 return output;
614 }
615
vc_getCounterExampleArray(VC vc,Expr e,Expr ** indices,Expr ** values,int * size)616 void vc_getCounterExampleArray(VC vc, Expr e, Expr** indices, Expr** values,
617 int* size)
618 {
619 stp::STP* stp_i = (stp::STP*)vc;
620 stp::ASTNode* a = (stp::ASTNode*)e;
621 stp::AbsRefine_CounterExample* ce =
622 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
623
624 bool t = false;
625 if (ce->CounterExampleSize())
626 t = true;
627
628 vector<std::pair<ASTNode, ASTNode>> entries =
629 ce->GetCounterExampleArray(t, *a);
630 *size = entries.size();
631 if (*size != 0)
632 {
633 *indices = (Expr*)malloc(*size * sizeof(Expr*));
634 assert(*indices);
635 *values = (Expr*)malloc(*size * sizeof(Expr*));
636 assert(*values);
637
638 for (int i = 0; i < *size; ++i)
639 {
640 (*indices)[i] = new stp::ASTNode(entries[i].first);
641 (*values)[i] = new stp::ASTNode(entries[i].second);
642 }
643 }
644 }
645
vc_counterexample_size(VC vc)646 int vc_counterexample_size(VC vc)
647 {
648 stp::STP* stp_i = (stp::STP*)vc;
649 stp::AbsRefine_CounterExample* ce =
650 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
651 return ce->CounterExampleSize();
652 }
653
vc_getWholeCounterExample(VC vc)654 WholeCounterExample vc_getWholeCounterExample(VC vc)
655 {
656 stp::STP* stp_i = (stp::STP*)vc;
657 stp::STPMgr* b = stp_i->bm;
658 stp::AbsRefine_CounterExample* ce =
659 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
660
661 stp::CompleteCounterExample* c =
662 new stp::CompleteCounterExample(ce->GetCompleteCounterExample(), b);
663 return c;
664 }
665
vc_getTermFromCounterExample(VC,Expr e,WholeCounterExample cc)666 Expr vc_getTermFromCounterExample(VC /*vc*/, Expr e, WholeCounterExample cc)
667 {
668 stp::ASTNode* n = (stp::ASTNode*)e;
669 stp::CompleteCounterExample* c = (stp::CompleteCounterExample*)cc;
670
671 stp::ASTNode* output = new stp::ASTNode(c->GetCounterExample(*n));
672 return output;
673 }
674
vc_deleteWholeCounterExample(WholeCounterExample cc)675 void vc_deleteWholeCounterExample(WholeCounterExample cc)
676 {
677 stp::CompleteCounterExample* c = (stp::CompleteCounterExample*)cc;
678
679 delete c;
680 }
681
vc_getBVLength(VC,Expr ex)682 int vc_getBVLength(VC /*vc*/, Expr ex)
683 {
684 stp::ASTNode* e = (stp::ASTNode*)ex;
685
686 if (stp::BITVECTOR_TYPE != e->GetType())
687 {
688 stp::FatalError("c_interface: vc_GetBVLength: "
689 "Input expression must be a bit-vector");
690 }
691 return e->GetValueWidth();
692 }
693
694 /////////////////////////////////////////////////////////////////////////////
695 // Expr Creation methods //
696 /////////////////////////////////////////////////////////////////////////////
697 //! Create a variable with a given name and type
698 /*! The type cannot be a function type. */
vc_varExpr1(VC vc,const char * name,int indexwidth,int valuewidth)699 Expr vc_varExpr1(VC vc, const char* name, int indexwidth, int valuewidth)
700 {
701 stp::STP* stp_i = (stp::STP*)vc;
702 stp::STPMgr* b = stp_i->bm;
703
704 stp::ASTNode o = b->CreateSymbol(name, indexwidth, valuewidth);
705
706 stp::ASTNode* output = new stp::ASTNode(o);
707 ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
708 assert(BVTypeCheck(*output));
709
710 // store the decls in a vector for printing purposes
711 b->decls.push_back(o);
712 return output;
713 }
714
vc_varExpr(VC vc,const char * name,Type type)715 Expr vc_varExpr(VC vc, const char* name, Type type)
716 {
717 stp::STP* stp_i = (stp::STP*)vc;
718 stp::STPMgr* b = stp_i->bm;
719 stp::ASTNode* a = (stp::ASTNode*)type;
720
721 unsigned indexWidth;
722 unsigned valueWidth;
723
724 switch (a->GetKind())
725 {
726 case stp::BITVECTOR:
727 indexWidth = 0;
728 valueWidth = (*a)[0].GetUnsignedConst();
729 break;
730 case stp::ARRAY:
731 indexWidth = (*a)[0].GetUnsignedConst();
732 valueWidth = (*a)[1].GetUnsignedConst();
733 break;
734 case stp::BOOLEAN:
735 indexWidth = 0;
736 valueWidth = 0;
737 break;
738 default:
739 stp::FatalError("CInterface: vc_varExpr: Unsupported type", *a);
740 assert(false);
741 exit(-1);
742 break;
743 }
744 stp::ASTNode o = b->CreateSymbol(name, indexWidth, valueWidth);
745
746 stp::ASTNode* output = new stp::ASTNode(o);
747 ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
748 assert(BVTypeCheck(*output));
749
750 // store the decls in a vector for printing purposes
751 b->decls.push_back(o);
752 return output;
753 }
754
755 //! Create an equality expression. The two children must have the
756 // same type.
vc_eqExpr(VC vc,Expr ccc0,Expr ccc1)757 Expr vc_eqExpr(VC vc, Expr ccc0, Expr ccc1)
758 {
759 stp::STP* stp_i = (stp::STP*)vc;
760 stp::STPMgr* b = stp_i->bm;
761
762 stp::ASTNode* a = (stp::ASTNode*)ccc0;
763 stp::ASTNode* aa = (stp::ASTNode*)ccc1;
764 assert(BVTypeCheck(*a));
765 assert(BVTypeCheck(*aa));
766 stp::ASTNode o = b->CreateNode(stp::EQ, *a, *aa);
767
768 stp::ASTNode* output = new stp::ASTNode(o);
769 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
770 return output;
771 }
772
vc_boolType(VC vc)773 Expr vc_boolType(VC vc)
774 {
775 stp::STP* stp_i = (stp::STP*)vc;
776 stp::STPMgr* b = stp_i->bm;
777
778 stp::ASTNode output = b->CreateNode(stp::BOOLEAN);
779 return persistNode(vc, output);
780 }
781
782 /////////////////////////////////////////////////////////////////////////////
783 // BOOLEAN EXPR Creation methods //
784 /////////////////////////////////////////////////////////////////////////////
785 // The following functions create Boolean expressions. The children
786 // provided as arguments must be of type Boolean.
vc_trueExpr(VC vc)787 Expr vc_trueExpr(VC vc)
788 {
789 stp::STP* stp_i = (stp::STP*)vc;
790 stp::STPMgr* b = stp_i->bm;
791 stp::ASTNode c = b->CreateNode(stp::TRUE);
792
793 stp::ASTNode* d = new stp::ASTNode(c);
794 // if(cinterface_exprdelete_on) created_exprs.push_back(d);
795 return d;
796 }
797
vc_falseExpr(VC vc)798 Expr vc_falseExpr(VC vc)
799 {
800 stp::STP* stp_i = (stp::STP*)vc;
801 stp::STPMgr* b = stp_i->bm;
802 stp::ASTNode c = b->CreateNode(stp::FALSE);
803
804 stp::ASTNode* d = new stp::ASTNode(c);
805 // if(cinterface_exprdelete_on) created_exprs.push_back(d);
806 return d;
807 }
808
vc_notExpr(VC vc,Expr ccc)809 Expr vc_notExpr(VC vc, Expr ccc)
810 {
811 stp::STP* stp_i = (stp::STP*)vc;
812 stp::STPMgr* b = stp_i->bm;
813 stp::ASTNode* a = (stp::ASTNode*)ccc;
814
815 stp::ASTNode o = b->CreateNode(stp::NOT, *a);
816 assert(BVTypeCheck(o));
817
818 stp::ASTNode* output = new stp::ASTNode(o);
819 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
820 return output;
821 }
822
vc_andExpr(VC vc,Expr left,Expr right)823 Expr vc_andExpr(VC vc, Expr left, Expr right)
824 {
825 stp::STP* stp_i = (stp::STP*)vc;
826 stp::STPMgr* b = stp_i->bm;
827 stp::ASTNode* l = (stp::ASTNode*)left;
828 stp::ASTNode* r = (stp::ASTNode*)right;
829
830 stp::ASTNode o = b->CreateNode(stp::AND, *l, *r);
831 assert(BVTypeCheck(o));
832
833 stp::ASTNode* output = new stp::ASTNode(o);
834 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
835 return output;
836 }
837
vc_orExpr(VC vc,Expr left,Expr right)838 Expr vc_orExpr(VC vc, Expr left, Expr right)
839 {
840 stp::STP* stp_i = (stp::STP*)vc;
841 stp::STPMgr* b = stp_i->bm;
842 stp::ASTNode* l = (stp::ASTNode*)left;
843 stp::ASTNode* r = (stp::ASTNode*)right;
844
845 stp::ASTNode o = b->CreateNode(stp::OR, *l, *r);
846 assert(BVTypeCheck(o));
847 stp::ASTNode* output = new stp::ASTNode(o);
848 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
849 return output;
850 }
851
vc_xorExpr(VC vc,Expr left,Expr right)852 Expr vc_xorExpr(VC vc, Expr left, Expr right)
853 {
854 stp::STP* stp_i = (stp::STP*)vc;
855 stp::STPMgr* b = stp_i->bm;
856 stp::ASTNode* l = (stp::ASTNode*)left;
857 stp::ASTNode* r = (stp::ASTNode*)right;
858
859 stp::ASTNode o = b->CreateNode(stp::XOR, *l, *r);
860 assert(BVTypeCheck(o));
861 stp::ASTNode* output = new stp::ASTNode(o);
862 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
863 return output;
864 }
865
vc_andExprN(VC vc,Expr * cc,int n)866 Expr vc_andExprN(VC vc, Expr* cc, int n)
867 {
868 stp::STP* stp_i = (stp::STP*)vc;
869 stp::STPMgr* b = stp_i->bm;
870 stp::ASTNode** c = (stp::ASTNode**)cc;
871 assert(n > 0);
872
873 stp::ASTVec d;
874 for (int i = 0; i < n; i++)
875 {
876 d.push_back(*c[i]);
877 }
878
879 stp::ASTNode o = b->CreateNode(stp::AND, d);
880 assert(BVTypeCheck(o));
881 stp::ASTNode* output = new stp::ASTNode(o);
882
883 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
884 return output;
885 }
886
vc_orExprN(VC vc,Expr * cc,int n)887 Expr vc_orExprN(VC vc, Expr* cc, int n)
888 {
889 stp::STP* stp_i = (stp::STP*)vc;
890 stp::STPMgr* b = stp_i->bm;
891 stp::ASTNode** c = (stp::ASTNode**)cc;
892 stp::ASTVec d;
893
894 for (int i = 0; i < n; i++)
895 d.push_back(*c[i]);
896
897 stp::ASTNode o = b->CreateNode(stp::OR, d);
898 assert(BVTypeCheck(o));
899
900 stp::ASTNode* output = new stp::ASTNode(o);
901 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
902 return output;
903 }
904
vc_bvPlusExprN(VC vc,int n_bits,Expr * cc,int n)905 Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* cc, int n)
906 {
907 stp::STP* stp_i = (stp::STP*)vc;
908 stp::STPMgr* b = stp_i->bm;
909 stp::ASTNode** c = (stp::ASTNode**)cc;
910 stp::ASTVec d;
911
912 for (int i = 0; i < n; i++)
913 d.push_back(*c[i]);
914
915 stp::ASTNode o = b->CreateTerm(stp::BVPLUS, n_bits, d);
916 assert(BVTypeCheck(o));
917
918 stp::ASTNode* output = new stp::ASTNode(o);
919 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
920 return output;
921 }
922
vc_iteExpr(VC vc,Expr cond,Expr thenpart,Expr elsepart)923 Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart)
924 {
925 stp::STP* stp_i = (stp::STP*)vc;
926 stp::STPMgr* b = stp_i->bm;
927 stp::ASTNode* c = (stp::ASTNode*)cond;
928 stp::ASTNode* t = (stp::ASTNode*)thenpart;
929 stp::ASTNode* e = (stp::ASTNode*)elsepart;
930
931 assert(BVTypeCheck(*c));
932 assert(BVTypeCheck(*t));
933 assert(BVTypeCheck(*e));
934 stp::ASTNode o;
935 // if the user asks for a formula then produce a formula, else
936 // prodcue a term
937 if (stp::BOOLEAN_TYPE == t->GetType())
938 o = b->CreateNode(stp::ITE, *c, *t, *e);
939 else
940 {
941 o = b->CreateTerm(stp::ITE, t->GetValueWidth(), *c, *t, *e);
942 o.SetIndexWidth(t->GetIndexWidth());
943 }
944 assert(BVTypeCheck(o));
945 stp::ASTNode* output = new stp::ASTNode(o);
946 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
947 return output;
948 }
949
vc_impliesExpr(VC vc,Expr antecedent,Expr consequent)950 Expr vc_impliesExpr(VC vc, Expr antecedent, Expr consequent)
951 {
952 stp::STP* stp_i = (stp::STP*)vc;
953 stp::STPMgr* b = stp_i->bm;
954 stp::ASTNode* c = (stp::ASTNode*)antecedent;
955 stp::ASTNode* t = (stp::ASTNode*)consequent;
956
957 assert(BVTypeCheck(*c));
958 assert(BVTypeCheck(*t));
959 stp::ASTNode o;
960
961 o = b->CreateNode(stp::IMPLIES, *c, *t);
962 assert(BVTypeCheck(o));
963 stp::ASTNode* output = new stp::ASTNode(o);
964 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
965 return output;
966 }
967
vc_iffExpr(VC vc,Expr e0,Expr e1)968 Expr vc_iffExpr(VC vc, Expr e0, Expr e1)
969 {
970 stp::STP* stp_i = (stp::STP*)vc;
971 stp::STPMgr* b = stp_i->bm;
972 stp::ASTNode* c = (stp::ASTNode*)e0;
973 stp::ASTNode* t = (stp::ASTNode*)e1;
974
975 assert(BVTypeCheck(*c));
976 assert(BVTypeCheck(*t));
977 stp::ASTNode o;
978
979 o = b->CreateNode(stp::IFF, *c, *t);
980 assert(BVTypeCheck(o));
981 stp::ASTNode* output = new stp::ASTNode(o);
982 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
983 return output;
984 }
985
vc_boolToBVExpr(VC vc,Expr form)986 Expr vc_boolToBVExpr(VC vc, Expr form)
987 {
988 stp::STP* stp_i = (stp::STP*)vc;
989 stp::STPMgr* b = stp_i->bm;
990 stp::ASTNode* c = (stp::ASTNode*)form;
991
992 assert(BVTypeCheck(*c));
993 if (!is_Form_kind(c->GetKind()))
994 {
995 stp::FatalError("CInterface: vc_BoolToBVExpr: "
996 "You have input a NON formula:",
997 *c);
998 }
999
1000 stp::ASTNode o;
1001 stp::ASTNode one = b->CreateOneConst(1);
1002 stp::ASTNode zero = b->CreateZeroConst(1);
1003 o = b->CreateTerm(stp::ITE, 1, *c, one, zero);
1004
1005 assert(BVTypeCheck(o));
1006 stp::ASTNode* output = new stp::ASTNode(o);
1007 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1008 return output;
1009 }
1010
vc_paramBoolExpr(VC vc,Expr boolvar,Expr parameter)1011 Expr vc_paramBoolExpr(VC vc, Expr boolvar, Expr parameter)
1012 {
1013 stp::STP* stp_i = (stp::STP*)vc;
1014 stp::STPMgr* b = stp_i->bm;
1015 stp::ASTNode* c = (stp::ASTNode*)boolvar;
1016 stp::ASTNode* t = (stp::ASTNode*)parameter;
1017
1018 assert(BVTypeCheck(*c));
1019 assert(BVTypeCheck(*t));
1020 stp::ASTNode o;
1021
1022 o = b->CreateNode(stp::PARAMBOOL, *c, *t);
1023 // BVTypeCheck(o);
1024 stp::ASTNode* output = new stp::ASTNode(o);
1025 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1026 return output;
1027 }
1028
1029 /////////////////////////////////////////////////////////////////////////////
1030 // BITVECTOR EXPR Creation methods //
1031 /////////////////////////////////////////////////////////////////////////////
vc_bvType(VC vc,int num_bits)1032 Type vc_bvType(VC vc, int num_bits)
1033 {
1034 stp::STP* stp_i = (stp::STP*)vc;
1035 stp::STPMgr* b = stp_i->bm;
1036
1037 if (!(0 < num_bits))
1038 {
1039 stp::FatalError("CInterface: number of bits in a bvtype"
1040 " must be a positive integer:",
1041 b->CreateNode(stp::UNDEFINED));
1042 }
1043
1044 stp::ASTNode e = b->CreateBVConst(32, num_bits);
1045 stp::ASTNode output = (b->CreateNode(stp::BITVECTOR, e));
1046 return persistNode(vc, output);
1047 }
1048
vc_bv32Type(VC vc)1049 Type vc_bv32Type(VC vc)
1050 {
1051 return vc_bvType(vc, 32);
1052 }
1053
vc_bvConstExprFromDecStr(VC vc,int width,const char * decimalInput)1054 Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput)
1055 {
1056 stp::STP* stp_i = (stp::STP*)vc;
1057 stp::STPMgr* b = stp_i->bm;
1058
1059 std::string str(decimalInput);
1060 stp::ASTNode n = b->CreateBVConst(str, 10, width);
1061 assert(BVTypeCheck(n));
1062 stp::ASTNode* output = new stp::ASTNode(n);
1063 return output;
1064 }
1065
vc_bvConstExprFromStr(VC vc,const char * binary_repr)1066 Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr)
1067 {
1068 stp::STP* stp_i = (stp::STP*)vc;
1069 stp::STPMgr* b = stp_i->bm;
1070
1071 stp::ASTNode n = b->CreateBVConst(binary_repr, 2);
1072 assert(BVTypeCheck(n));
1073 stp::ASTNode* output = new stp::ASTNode(n);
1074 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1075 return output;
1076 }
1077
vc_bvConstExprFromInt(VC vc,int n_bits,unsigned int value)1078 Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value)
1079 {
1080 stp::STP* stp_i = (stp::STP*)vc;
1081 stp::STPMgr* b = stp_i->bm;
1082
1083 unsigned long long int v = (unsigned long long int)value;
1084 unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64 - n_bits);
1085 // printf("%ull", max_n_bits);
1086 if (v > max_n_bits)
1087 {
1088 printf("CInterface: vc_bvConstExprFromInt: "
1089 "Cannot construct a constant %llu >= %llu,\n",
1090 v, max_n_bits);
1091 stp::FatalError("FatalError");
1092 }
1093 stp::ASTNode n = b->CreateBVConst(n_bits, v);
1094 assert(BVTypeCheck(n));
1095 return persistNode(vc, n);
1096 }
1097
vc_bvConstExprFromLL(VC vc,int n_bits,unsigned long long value)1098 Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value)
1099 {
1100 stp::STP* stp_i = (stp::STP*)vc;
1101 stp::STPMgr* b = stp_i->bm;
1102
1103 stp::ASTNode n = b->CreateBVConst(n_bits, value);
1104 assert(BVTypeCheck(n));
1105 stp::ASTNode* output = new stp::ASTNode(n);
1106 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1107 return output;
1108 }
1109
vc_bvConcatExpr(VC vc,Expr left,Expr right)1110 Expr vc_bvConcatExpr(VC vc, Expr left, Expr right)
1111 {
1112 stp::STP* stp_i = (stp::STP*)vc;
1113 stp::STPMgr* b = stp_i->bm;
1114 stp::ASTNode* l = (stp::ASTNode*)left;
1115 stp::ASTNode* r = (stp::ASTNode*)right;
1116
1117 assert(BVTypeCheck(*l));
1118 assert(BVTypeCheck(*r));
1119 stp::ASTNode o = b->CreateTerm(
1120 stp::BVCONCAT, l->GetValueWidth() + r->GetValueWidth(), *l, *r);
1121 assert(BVTypeCheck(o));
1122 stp::ASTNode* output = new stp::ASTNode(o);
1123 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1124 return output;
1125 }
1126
createBinaryTerm(VC vc,int n_bits,Kind k,Expr left,Expr right)1127 Expr createBinaryTerm(VC vc, int n_bits, Kind k, Expr left, Expr right)
1128 {
1129 stp::STP* stp_i = (stp::STP*)vc;
1130 stp::STPMgr* b = stp_i->bm;
1131 stp::ASTNode* l = (stp::ASTNode*)left;
1132 stp::ASTNode* r = (stp::ASTNode*)right;
1133
1134 assert(BVTypeCheck(*l));
1135 assert(BVTypeCheck(*r));
1136 stp::ASTNode o = b->CreateTerm(k, n_bits, *l, *r);
1137 assert(BVTypeCheck(o));
1138 stp::ASTNode* output = new stp::ASTNode(o);
1139 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1140 return output;
1141 }
1142
vc_bvPlusExpr(VC vc,int n_bits,Expr left,Expr right)1143 Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right)
1144 {
1145 return createBinaryTerm(vc, n_bits, stp::BVPLUS, left, right);
1146 }
1147
vc_bv32PlusExpr(VC vc,Expr left,Expr right)1148 Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right)
1149 {
1150 return vc_bvPlusExpr(vc, 32, left, right);
1151 }
1152
vc_bvMinusExpr(VC vc,int n_bits,Expr left,Expr right)1153 Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right)
1154 {
1155 return createBinaryTerm(vc, n_bits, stp::BVSUB, left, right);
1156 }
1157
vc_bv32MinusExpr(VC vc,Expr left,Expr right)1158 Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right)
1159 {
1160 return vc_bvMinusExpr(vc, 32, left, right);
1161 }
1162
vc_bvMultExpr(VC vc,int n_bits,Expr left,Expr right)1163 Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right)
1164 {
1165 return createBinaryTerm(vc, n_bits, stp::BVMULT, left, right);
1166 }
1167
vc_bvDivExpr(VC vc,int n_bits,Expr left,Expr right)1168 Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right)
1169 {
1170 return createBinaryTerm(vc, n_bits, stp::BVDIV, left, right);
1171 }
1172
vc_bvModExpr(VC vc,int n_bits,Expr left,Expr right)1173 Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right)
1174 {
1175 return createBinaryTerm(vc, n_bits, stp::BVMOD, left, right);
1176 }
1177
vc_sbvDivExpr(VC vc,int n_bits,Expr left,Expr right)1178 Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right)
1179 {
1180 return createBinaryTerm(vc, n_bits, stp::SBVDIV, left, right);
1181 }
1182
vc_sbvModExpr(VC vc,int n_bits,Expr left,Expr right)1183 Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right)
1184 {
1185 return createBinaryTerm(vc, n_bits, stp::SBVMOD, left, right);
1186 }
1187
vc_sbvRemExpr(VC vc,int n_bits,Expr left,Expr right)1188 Expr vc_sbvRemExpr(VC vc, int n_bits, Expr left, Expr right)
1189 {
1190 return createBinaryTerm(vc, n_bits, stp::SBVREM, left, right);
1191 }
1192
vc_bv32MultExpr(VC vc,Expr left,Expr right)1193 Expr vc_bv32MultExpr(VC vc, Expr left, Expr right)
1194 {
1195 return vc_bvMultExpr(vc, 32, left, right);
1196 }
1197
createBinaryNode(VC vc,Kind k,Expr left,Expr right)1198 Expr createBinaryNode(VC vc, Kind k, Expr left, Expr right)
1199 {
1200 stp::STP* stp_i = (stp::STP*)vc;
1201 stp::STPMgr* b = stp_i->bm;
1202 stp::ASTNode* l = (stp::ASTNode*)left;
1203 stp::ASTNode* r = (stp::ASTNode*)right;
1204 assert(BVTypeCheck(*l));
1205 assert(BVTypeCheck(*r));
1206 stp::ASTNode o = b->CreateNode(k, *l, *r);
1207 assert(BVTypeCheck(o));
1208 stp::ASTNode* output = new stp::ASTNode(o);
1209 // if(cinterface_exprdelete_on)
1210 // created_exprs.push_back(output);
1211 return output;
1212 }
1213
1214 // unsigned comparators
vc_bvLtExpr(VC vc,Expr left,Expr right)1215 Expr vc_bvLtExpr(VC vc, Expr left, Expr right)
1216 {
1217 return createBinaryNode(vc, stp::BVLT, left, right);
1218 }
vc_bvLeExpr(VC vc,Expr left,Expr right)1219 Expr vc_bvLeExpr(VC vc, Expr left, Expr right)
1220 {
1221 return createBinaryNode(vc, stp::BVLE, left, right);
1222 }
vc_bvGtExpr(VC vc,Expr left,Expr right)1223 Expr vc_bvGtExpr(VC vc, Expr left, Expr right)
1224 {
1225 return createBinaryNode(vc, stp::BVGT, left, right);
1226 }
vc_bvGeExpr(VC vc,Expr left,Expr right)1227 Expr vc_bvGeExpr(VC vc, Expr left, Expr right)
1228 {
1229 return createBinaryNode(vc, stp::BVGE, left, right);
1230 }
1231 // signed comparators
vc_sbvLtExpr(VC vc,Expr left,Expr right)1232 Expr vc_sbvLtExpr(VC vc, Expr left, Expr right)
1233 {
1234 return createBinaryNode(vc, stp::BVSLT, left, right);
1235 }
vc_sbvLeExpr(VC vc,Expr left,Expr right)1236 Expr vc_sbvLeExpr(VC vc, Expr left, Expr right)
1237 {
1238 return createBinaryNode(vc, stp::BVSLE, left, right);
1239 }
vc_sbvGtExpr(VC vc,Expr left,Expr right)1240 Expr vc_sbvGtExpr(VC vc, Expr left, Expr right)
1241 {
1242 return createBinaryNode(vc, stp::BVSGT, left, right);
1243 }
vc_sbvGeExpr(VC vc,Expr left,Expr right)1244 Expr vc_sbvGeExpr(VC vc, Expr left, Expr right)
1245 {
1246 return createBinaryNode(vc, stp::BVSGE, left, right);
1247 }
1248
vc_bvLeftShiftExprExpr(VC vc,int n_bits,Expr left,Expr right)1249 Expr vc_bvLeftShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)
1250 {
1251 return createBinaryTerm(vc, n_bits, stp::BVLEFTSHIFT, left, right);
1252 }
1253
vc_bvRightShiftExprExpr(VC vc,int n_bits,Expr left,Expr right)1254 Expr vc_bvRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)
1255 {
1256 return createBinaryTerm(vc, n_bits, stp::BVRIGHTSHIFT, left, right);
1257 }
1258
vc_bvSignedRightShiftExprExpr(VC vc,int n_bits,Expr left,Expr right)1259 Expr vc_bvSignedRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)
1260 {
1261 return createBinaryTerm(vc, n_bits, stp::BVSRSHIFT, left, right);
1262 }
1263
vc_bvUMinusExpr(VC vc,Expr ccc)1264 Expr vc_bvUMinusExpr(VC vc, Expr ccc)
1265 {
1266 stp::STP* stp_i = (stp::STP*)vc;
1267 stp::STPMgr* b = stp_i->bm;
1268
1269 stp::ASTNode* a = (stp::ASTNode*)ccc;
1270 assert(BVTypeCheck(*a));
1271
1272 stp::ASTNode o = b->CreateTerm(stp::BVUMINUS, a->GetValueWidth(), *a);
1273 assert(BVTypeCheck(o));
1274 stp::ASTNode* output = new stp::ASTNode(o);
1275 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1276 return output;
1277 }
1278
1279 // Expr createBinaryTerm(VC vc, int n_bits, Kind k, Expr left, Expr right){
1280
1281 // bitwise operations: these are terms not formulas
vc_bvAndExpr(VC vc,Expr left,Expr right)1282 Expr vc_bvAndExpr(VC vc, Expr left, Expr right)
1283 {
1284 return createBinaryTerm(vc, (*((stp::ASTNode*)left)).GetValueWidth(),
1285 stp::BVAND, left, right);
1286 }
1287
vc_bvOrExpr(VC vc,Expr left,Expr right)1288 Expr vc_bvOrExpr(VC vc, Expr left, Expr right)
1289 {
1290 return createBinaryTerm(vc, (*((stp::ASTNode*)left)).GetValueWidth(),
1291 stp::BVOR, left, right);
1292 }
1293
vc_bvXorExpr(VC vc,Expr left,Expr right)1294 Expr vc_bvXorExpr(VC vc, Expr left, Expr right)
1295 {
1296 return createBinaryTerm(vc, (*((stp::ASTNode*)left)).GetValueWidth(),
1297 stp::BVXOR, left, right);
1298 }
1299
vc_bvNotExpr(VC vc,Expr ccc)1300 Expr vc_bvNotExpr(VC vc, Expr ccc)
1301 {
1302 stp::STP* stp_i = (stp::STP*)vc;
1303 stp::STPMgr* b = stp_i->bm;
1304 stp::ASTNode* a = (stp::ASTNode*)ccc;
1305
1306 assert(BVTypeCheck(*a));
1307 stp::ASTNode o = b->CreateTerm(stp::BVNOT, a->GetValueWidth(), *a);
1308 assert(BVTypeCheck(o));
1309 stp::ASTNode* output = new stp::ASTNode(o);
1310 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1311 return output;
1312 }
1313
vc_bvLeftShiftExpr(VC vc,int sh_amt,Expr ccc)1314 Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc)
1315 {
1316 stp::STP* stp_i = (stp::STP*)vc;
1317 stp::STPMgr* b = stp_i->bm;
1318 stp::ASTNode* a = (stp::ASTNode*)ccc;
1319 assert(BVTypeCheck(*a));
1320
1321 // convert leftshift to bvconcat
1322 if (0 != sh_amt)
1323 {
1324 stp::ASTNode len = b->CreateBVConst(sh_amt, 0);
1325 stp::ASTNode o =
1326 b->CreateTerm(stp::BVCONCAT, a->GetValueWidth() + sh_amt, *a, len);
1327 assert(BVTypeCheck(o));
1328 stp::ASTNode* output = new stp::ASTNode(o);
1329 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1330 return output;
1331 }
1332 else
1333 return a;
1334 }
1335
vc_bvRightShiftExpr(VC vc,int sh_amt,Expr ccc)1336 Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc)
1337 {
1338 stp::STP* stp_i = (stp::STP*)vc;
1339 stp::STPMgr* b = stp_i->bm;
1340 stp::ASTNode* a = (stp::ASTNode*)ccc;
1341 assert(BVTypeCheck(*a));
1342
1343 unsigned int w = a->GetValueWidth();
1344 // the amount by which you are rightshifting
1345 // is less-than/equal-to the length of input
1346 // bitvector
1347 if (0 < (unsigned)sh_amt && (unsigned)sh_amt < w)
1348 {
1349 stp::ASTNode len = b->CreateBVConst(sh_amt, 0);
1350 stp::ASTNode hi = b->CreateBVConst(32, w - 1);
1351 stp::ASTNode low = b->CreateBVConst(32, sh_amt);
1352 stp::ASTNode extract =
1353 b->CreateTerm(stp::BVEXTRACT, w - sh_amt, *a, hi, low);
1354
1355 stp::ASTNode n = b->CreateTerm(stp::BVCONCAT, w, len, extract);
1356 BVTypeCheck(n);
1357 stp::ASTNode* output = new stp::ASTNode(n);
1358 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1359 return output;
1360 }
1361 else if ((unsigned)sh_amt == w)
1362 {
1363 stp::ASTNode* output = new stp::ASTNode(b->CreateBVConst(w, 0));
1364 return output;
1365 }
1366 else if (sh_amt == 0)
1367 return a;
1368 else
1369 {
1370 if (0 == w)
1371 {
1372 stp::FatalError("CInterface: vc_bvRightShiftExpr: "
1373 "cannot have a bitvector of length 0:",
1374 *a);
1375 }
1376 stp::ASTNode* output = new stp::ASTNode(b->CreateBVConst(w, 0));
1377 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1378 return output;
1379 }
1380 }
1381
1382 /* Same as vc_bvLeftShift only that the answer in 32 bits long */
vc_bv32LeftShiftExpr(VC vc,int sh_amt,Expr child)1383 Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child)
1384 {
1385 return vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, sh_amt, child), 31, 0);
1386 }
1387
1388 /* Same as vc_bvRightShift only that the answer in 32 bits long */
vc_bv32RightShiftExpr(VC vc,int sh_amt,Expr child)1389 Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child)
1390 {
1391 return vc_bvExtract(vc, vc_bvRightShiftExpr(vc, sh_amt, child), 31, 0);
1392 }
1393
vc_bvVar32LeftShiftExpr(VC vc,Expr sh_amt,Expr child)1394 Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child)
1395 {
1396 Expr ifpart;
1397 Expr thenpart;
1398 Expr elsepart = vc_trueExpr(vc);
1399 Expr ite = vc_trueExpr(vc);
1400 int child_width = vc_getBVLength(vc, child);
1401 int shift_width = vc_getBVLength(vc, sh_amt);
1402
1403 assert(child_width > 0);
1404
1405 for (int count = 32; count >= 0; count--)
1406 {
1407 if (count != 32)
1408 {
1409 ifpart =
1410 vc_eqExpr(vc, sh_amt, vc_bvConstExprFromInt(vc, shift_width, count));
1411 thenpart = vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, count, child),
1412 child_width - 1, 0);
1413
1414 ite = vc_iteExpr(vc, ifpart, thenpart, elsepart);
1415 elsepart = ite;
1416 }
1417 else
1418 {
1419 elsepart = vc_bvConstExprFromInt(vc, child_width, 0);
1420 }
1421 }
1422 return ite;
1423 }
1424
vc_bvVar32DivByPowOfTwoExpr(VC vc,Expr child,Expr rhs)1425 Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs)
1426 {
1427 Expr ifpart;
1428 Expr thenpart;
1429 Expr elsepart = vc_trueExpr(vc);
1430 Expr ite = vc_trueExpr(vc);
1431
1432 for (int count = 32; count >= 0; count--)
1433 {
1434 if (count != 32)
1435 {
1436 ifpart = vc_eqExpr(vc, rhs, vc_bvConstExprFromInt(vc, 32, 1 << count));
1437 thenpart = vc_bvRightShiftExpr(vc, count, child);
1438 ite = vc_iteExpr(vc, ifpart, thenpart, elsepart);
1439 elsepart = ite;
1440 }
1441 else
1442 {
1443 elsepart = vc_bvConstExprFromInt(vc, 32, 0);
1444 }
1445 }
1446 return ite;
1447 }
1448
vc_bvVar32RightShiftExpr(VC vc,Expr sh_amt,Expr child)1449 Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child)
1450 {
1451 Expr ifpart;
1452 Expr thenpart;
1453 Expr elsepart = vc_trueExpr(vc);
1454 Expr ite = vc_trueExpr(vc);
1455
1456 int child_width = vc_getBVLength(vc, child);
1457 int shift_width = vc_getBVLength(vc, sh_amt);
1458
1459 assert(child_width > 0);
1460
1461 for (int count = 32; count >= 0; count--)
1462 {
1463 if (count != 32)
1464 {
1465 ifpart =
1466 vc_eqExpr(vc, sh_amt, vc_bvConstExprFromInt(vc, shift_width, count));
1467 thenpart = vc_bvRightShiftExpr(vc, count, child);
1468 ite = vc_iteExpr(vc, ifpart, thenpart, elsepart);
1469 elsepart = ite;
1470 }
1471 else
1472 {
1473 elsepart = vc_bvConstExprFromInt(vc, child_width, 0);
1474 }
1475 }
1476 return ite;
1477 }
1478
vc_bvExtract(VC vc,Expr ccc,int hi_num,int low_num)1479 Expr vc_bvExtract(VC vc, Expr ccc, int hi_num, int low_num)
1480 {
1481 stp::STP* stp_i = (stp::STP*)vc;
1482 stp::STPMgr* b = stp_i->bm;
1483 stp::ASTNode* a = (stp::ASTNode*)ccc;
1484 BVTypeCheck(*a);
1485
1486 stp::ASTNode hi = b->CreateBVConst(32, hi_num);
1487 stp::ASTNode low = b->CreateBVConst(32, low_num);
1488 stp::ASTNode o =
1489 b->CreateTerm(stp::BVEXTRACT, hi_num - low_num + 1, *a, hi, low);
1490 BVTypeCheck(o);
1491 stp::ASTNode* output = new stp::ASTNode(o);
1492 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1493 return output;
1494 }
1495
vc_bvBoolExtract(VC vc,Expr ccc,int bit_num)1496 Expr vc_bvBoolExtract(VC vc, Expr ccc, int bit_num)
1497 {
1498 stp::STP* stp_i = (stp::STP*)vc;
1499 stp::STPMgr* b = stp_i->bm;
1500 stp::ASTNode* a = (stp::ASTNode*)ccc;
1501 BVTypeCheck(*a);
1502
1503 stp::ASTNode bit = b->CreateBVConst(32, bit_num);
1504 // stp::ASTNode o = b->CreateNode(stp::BVGETBIT,*a,bit);
1505 stp::ASTNode zero = b->CreateBVConst(1, 0);
1506 stp::ASTNode oo = b->CreateTerm(stp::BVEXTRACT, 1, *a, bit, bit);
1507 stp::ASTNode o = b->CreateNode(stp::EQ, oo, zero);
1508 BVTypeCheck(o);
1509 stp::ASTNode* output = new stp::ASTNode(o);
1510 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1511 return output;
1512 }
1513
vc_bvBoolExtract_Zero(VC vc,Expr ccc,int bit_num)1514 Expr vc_bvBoolExtract_Zero(VC vc, Expr ccc, int bit_num)
1515 {
1516 stp::STP* stp_i = (stp::STP*)vc;
1517 stp::STPMgr* b = stp_i->bm;
1518 stp::ASTNode* a = (stp::ASTNode*)ccc;
1519 BVTypeCheck(*a);
1520
1521 stp::ASTNode bit = b->CreateBVConst(32, bit_num);
1522 // stp::ASTNode o = b->CreateNode(stp::BVGETBIT,*a,bit);
1523 stp::ASTNode zero = b->CreateBVConst(1, 0);
1524 stp::ASTNode oo = b->CreateTerm(stp::BVEXTRACT, 1, *a, bit, bit);
1525 stp::ASTNode o = b->CreateNode(stp::EQ, oo, zero);
1526 BVTypeCheck(o);
1527 stp::ASTNode* output = new stp::ASTNode(o);
1528 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1529 return output;
1530 }
1531
vc_bvBoolExtract_One(VC vc,Expr ccc,int bit_num)1532 Expr vc_bvBoolExtract_One(VC vc, Expr ccc, int bit_num)
1533 {
1534 stp::STP* stp_i = (stp::STP*)vc;
1535 stp::STPMgr* b = stp_i->bm;
1536 stp::ASTNode* a = (stp::ASTNode*)ccc;
1537 BVTypeCheck(*a);
1538
1539 stp::ASTNode bit = b->CreateBVConst(32, bit_num);
1540 // stp::ASTNode o = b->CreateNode(stp::BVGETBIT,*a,bit);
1541 stp::ASTNode one = b->CreateBVConst(1, 1);
1542 stp::ASTNode oo = b->CreateTerm(stp::BVEXTRACT, 1, *a, bit, bit);
1543 stp::ASTNode o = b->CreateNode(stp::EQ, oo, one);
1544 BVTypeCheck(o);
1545 stp::ASTNode* output = new stp::ASTNode(o);
1546 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1547 return output;
1548 }
1549
vc_bvSignExtend(VC vc,Expr ccc,int nbits)1550 Expr vc_bvSignExtend(VC vc, Expr ccc, int nbits)
1551 {
1552 stp::STP* stp_i = (stp::STP*)vc;
1553 stp::STPMgr* b = stp_i->bm;
1554 stp::ASTNode* a = (stp::ASTNode*)ccc;
1555
1556 // width of the expr which is being sign extended. nbits is the
1557 // resulting length of the signextended expr
1558 BVTypeCheck(*a);
1559
1560 unsigned exprlen = a->GetValueWidth();
1561 unsigned outputlen = nbits;
1562 stp::ASTNode n;
1563 if (exprlen >= outputlen)
1564 {
1565 // extract
1566 stp::ASTNode hi = b->CreateBVConst(32, outputlen - 1);
1567 stp::ASTNode low = b->CreateBVConst(32, 0);
1568 n = b->CreateTerm(stp::BVEXTRACT, nbits, *a, hi, low);
1569 BVTypeCheck(n);
1570 }
1571 else
1572 {
1573 // sign extend
1574 stp::ASTNode width = b->CreateBVConst(32, nbits);
1575 n = b->CreateTerm(stp::BVSX, nbits, *a, width);
1576 }
1577
1578 BVTypeCheck(n);
1579 stp::ASTNode* output = new stp::ASTNode(n);
1580 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1581 return output;
1582 }
1583
1584 //! Return an int from a constant bitvector expression
getBVInt(Expr e)1585 int getBVInt(Expr e)
1586 {
1587 stp::ASTNode* a = (stp::ASTNode*)e;
1588
1589 if (stp::BVCONST != a->GetKind())
1590 {
1591 stp::FatalError("CInterface: getBVInt: Attempting to "
1592 "extract int value from a NON-constant BITVECTOR: ",
1593 *a);
1594 }
1595 return (int)a->GetUnsignedConst();
1596 }
1597
1598 //! Return an unsigned int from a constant bitvector expression
getBVUnsigned(Expr e)1599 unsigned int getBVUnsigned(Expr e)
1600 {
1601 stp::ASTNode* a = (stp::ASTNode*)e;
1602
1603 if (stp::BVCONST != a->GetKind())
1604 {
1605 stp::FatalError("getBVUnsigned: Attempting to extract int "
1606 "value from a NON-constant BITVECTOR: ",
1607 *a);
1608 }
1609 return (unsigned int)a->GetUnsignedConst();
1610 }
1611
1612 //! Return an unsigned long long int from a constant bitvector expression
getBVUnsignedLongLong(Expr e)1613 unsigned long long int getBVUnsignedLongLong(Expr e)
1614 {
1615 stp::ASTNode* a = (stp::ASTNode*)e;
1616
1617 if (stp::BVCONST != a->GetKind())
1618 stp::FatalError("getBVUnsigned: Attempting to extract int value"
1619 "from a NON-constant BITVECTOR: ",
1620 *a);
1621 unsigned* bv = a->GetBVConst();
1622
1623 char* str_bv = (char*)CONSTANTBV::BitVector_to_Bin(bv);
1624 unsigned long long int tmp = std::strtoull(str_bv, NULL, 2);
1625 CONSTANTBV::BitVector_Dispose((unsigned char*)str_bv);
1626 return tmp;
1627 }
1628
vc_simplify(VC vc,Expr e)1629 Expr vc_simplify(VC vc, Expr e)
1630 {
1631 stp::STP* stp_i = (stp::STP*)vc;
1632 stp::Simplifier* simp = (stp::Simplifier*)(stp_i->simp);
1633 stp::ASTNode* a = (stp::ASTNode*)e;
1634
1635 if (stp::BOOLEAN_TYPE == a->GetType())
1636 {
1637 stp::ASTNode* round1 =
1638 new stp::ASTNode(simp->SimplifyFormula_TopLevel(*a, false));
1639 stp::ASTNode* output =
1640 new stp::ASTNode(simp->SimplifyFormula_TopLevel(*round1, false));
1641 delete round1;
1642 return output;
1643 }
1644 else
1645 {
1646 stp::ASTNode* round1 = new stp::ASTNode(simp->SimplifyTerm(*a));
1647 stp::ASTNode* output = new stp::ASTNode(simp->SimplifyTerm(*round1));
1648 delete round1;
1649 return output;
1650 }
1651 }
1652
1653 /* C pointer support: C interface to support C memory arrays in CVCL */
vc_bvCreateMemoryArray(VC vc,const char * arrayName)1654 Expr vc_bvCreateMemoryArray(VC vc, const char* arrayName)
1655 {
1656 Type bv8 = vc_bvType(vc, 8);
1657 Type bv32 = vc_bvType(vc, 32);
1658
1659 Type malloced_mem0 = vc_arrayType(vc, bv32, bv8);
1660 return vc_varExpr(vc, arrayName, malloced_mem0);
1661 }
1662
vc_bvReadMemoryArray(VC vc,Expr array,Expr byteIndex,int numOfBytes)1663 Expr vc_bvReadMemoryArray(VC vc, Expr array, Expr byteIndex, int numOfBytes)
1664 {
1665 if (!(numOfBytes > 0))
1666 stp::FatalError("numOfBytes must be greater than 0");
1667
1668 if (numOfBytes == 1)
1669 return vc_readExpr(vc, array, byteIndex);
1670 else
1671 {
1672 int count = 1;
1673 Expr a = vc_readExpr(vc, array, byteIndex);
1674 while (--numOfBytes > 0)
1675 {
1676 Expr b = vc_readExpr(vc, array,
1677 /*vc_simplify(vc, */
1678 vc_bvPlusExpr(vc, 32, byteIndex,
1679 vc_bvConstExprFromInt(vc, 32, count)));
1680 a = vc_bvConcatExpr(vc, b, a);
1681 count++;
1682 }
1683 return a;
1684 }
1685 }
1686
vc_bvWriteToMemoryArray(VC vc,Expr array,Expr byteIndex,Expr element,int numOfBytes)1687 Expr vc_bvWriteToMemoryArray(VC vc, Expr array, Expr byteIndex, Expr element,
1688 int numOfBytes)
1689 {
1690 if (!(numOfBytes > 0))
1691 stp::FatalError("numOfBytes must be greater than 0");
1692
1693 int newBitsPerElem = numOfBytes * 8;
1694 if (numOfBytes == 1)
1695 return vc_writeExpr(vc, array, byteIndex, element);
1696 else
1697 {
1698 int count = 1;
1699 int low_elem = 0;
1700 int hi_elem = low_elem + 7;
1701 Expr c = vc_bvExtract(vc, element, hi_elem, low_elem);
1702 Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
1703 while (--numOfBytes > 0)
1704 {
1705 low_elem = low_elem + 8;
1706 hi_elem = low_elem + 7;
1707
1708 c = vc_bvExtract(vc, element, hi_elem, low_elem);
1709 newarray = vc_writeExpr(
1710 vc, newarray, vc_bvPlusExpr(vc, 32, byteIndex,
1711 vc_bvConstExprFromInt(vc, 32, count)),
1712 c);
1713 count++;
1714 }
1715 return newarray;
1716 }
1717 }
1718
vc_bv32ConstExprFromInt(VC vc,unsigned int value)1719 Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value)
1720 {
1721 return vc_bvConstExprFromInt(vc, 32, value);
1722 }
1723
1724 #if 0
1725 static char *val_to_binary_str(unsigned nbits, unsigned long long val) {
1726 char s[65];
1727
1728 assert(nbits < sizeof s);
1729 strcpy(s, "");
1730 while(nbits-- > 0) {
1731 if((val >> nbits) & 1)
1732 strcat(s, "1");
1733 else
1734 strcat(s, "0");
1735 }
1736 return strdup(s);
1737 }
1738 #endif
1739
vc_parseExpr(VC vc,const char * infile)1740 Expr vc_parseExpr(VC vc, const char* infile)
1741 {
1742 stp::STP* stp_i = (stp::STP*)vc;
1743 stp::STPMgr* b = stp_i->bm;
1744
1745 extern FILE *cvcin, *smtin;
1746 cvcin = fopen(infile, "r");
1747 if (cvcin == NULL)
1748 {
1749 fprintf(stderr, "STP: Error: cannot open %s\n", infile);
1750 stp::FatalError("Cannot open file");
1751 return 0;
1752 }
1753
1754 CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
1755 if (0 != c)
1756 {
1757 cout << CONSTANTBV::BitVector_Error(c) << endl;
1758 return 0;
1759 }
1760
1761 stp::Cpp_interface cpp_inter(*b, b->defaultNodeFactory);
1762 stp::GlobalParserInterface = &cpp_inter;
1763
1764 stp::ASTVec* AssertsQuery = new stp::ASTVec;
1765 if (b->UserFlags.smtlib1_parser_flag)
1766 {
1767 smtin = cvcin;
1768 cvcin = NULL;
1769 stp::GlobalSTP = stp_i;
1770 stp::GlobalParserBM = b;
1771 smtparse((void*)AssertsQuery);
1772 stp::GlobalSTP = NULL;
1773 stp::GlobalParserBM = NULL;
1774 }
1775 else
1776 {
1777 stp::GlobalSTP = stp_i;
1778 stp::GlobalParserBM = b;
1779 cvcparse((void*)AssertsQuery);
1780 stp::GlobalSTP = NULL;
1781 stp::GlobalParserBM = NULL;
1782 }
1783
1784 stp::ASTNode asserts = (*(stp::ASTVec*)AssertsQuery)[0];
1785 stp::ASTNode query = (*(stp::ASTVec*)AssertsQuery)[1];
1786
1787 stp::ASTNode oo = b->CreateNode(stp::NOT, query);
1788 stp::ASTNode o = b->CreateNode(stp::AND, asserts, oo);
1789 stp::ASTNode* output = new stp::ASTNode(o);
1790 delete AssertsQuery;
1791 return output;
1792 }
1793
exprString(Expr e)1794 char* exprString(Expr e)
1795 {
1796 stringstream ss;
1797 ((stp::ASTNode*)e)->PL_Print(ss, 0);
1798 string s = ss.str();
1799 char* copy = strdup(s.c_str());
1800 return copy;
1801 }
1802
typeString(Type t)1803 char* typeString(Type t)
1804 {
1805 stringstream ss;
1806 ((stp::ASTNode*)t)->PL_Print(ss, 0);
1807
1808 string s = ss.str();
1809 char* copy = strdup(s.c_str());
1810 return copy;
1811 }
1812
getChild(Expr e,int i)1813 Expr getChild(Expr e, int i)
1814 {
1815 stp::ASTNode* a = (stp::ASTNode*)e;
1816
1817 stp::ASTVec c = a->GetChildren();
1818 if (0 <= i && (unsigned)i < c.size())
1819 {
1820 stp::ASTNode o = c[i];
1821 stp::ASTNode* output = new stp::ASTNode(o);
1822 // if(cinterface_exprdelete_on) created_exprs.push_back(output);
1823 return output;
1824 }
1825 else
1826 {
1827 stp::FatalError("getChild: Error accessing childNode "
1828 "in expression: ",
1829 *a);
1830 }
1831 return a;
1832 }
1833
vc_registerErrorHandler(void (* error_hdlr)(const char * err_msg))1834 void vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg))
1835 {
1836 stp::vc_error_hdlr = error_hdlr;
1837 }
1838
vc_getHashQueryStateToBuffer(VC vc,Expr query)1839 int vc_getHashQueryStateToBuffer(VC vc, Expr query)
1840 {
1841 stp::STP* stp_i = (stp::STP*)vc;
1842 stp::STPMgr* b = stp_i->bm;
1843 stp::ASTNode* qry = (stp::ASTNode*)query;
1844 assert(vc);
1845 assert(query);
1846
1847 stp::ASTVec v = b->GetAsserts();
1848 stp::ASTNode out = b->CreateNode(stp::AND, b->CreateNode(stp::NOT, *qry), v);
1849 return out.Hash();
1850 }
1851
vc_getType(VC vc,Expr ex)1852 Type vc_getType(VC vc, Expr ex)
1853 {
1854 stp::ASTNode* e = (stp::ASTNode*)ex;
1855
1856 switch (e->GetType())
1857 {
1858 case stp::BOOLEAN_TYPE:
1859 return vc_boolType(vc);
1860 break;
1861 case stp::BITVECTOR_TYPE:
1862 return vc_bvType(vc, e->GetValueWidth());
1863 break;
1864 case stp::ARRAY_TYPE:
1865 {
1866 Type typeindex = vc_bvType(vc, e->GetIndexWidth());
1867 Type typedata = vc_bvType(vc, e->GetValueWidth());
1868 return vc_arrayType(vc, typeindex, typedata);
1869 break;
1870 }
1871 default:
1872 stp::FatalError("c_interface: vc_GetType: "
1873 "expression with bad typing: "
1874 "please check your expression construction");
1875 return vc_boolType(vc);
1876 break;
1877 }
1878 }
1879
1880 //!if e is TRUE then return 1; if e is FALSE then return 0; otherwise
1881 // return -1
vc_isBool(Expr e)1882 int vc_isBool(Expr e)
1883 {
1884 stp::ASTNode* input = (stp::ASTNode*)e;
1885 if (stp::TRUE == input->GetKind())
1886 {
1887 return 1;
1888 }
1889
1890 if (stp::FALSE == input->GetKind())
1891 {
1892 return 0;
1893 }
1894
1895 return -1;
1896 }
1897
vc_Destroy(VC vc)1898 void vc_Destroy(VC vc)
1899 {
1900 stp::STP* stp_i = (stp::STP*)vc;
1901 stp::STPMgr* b = stp_i->bm;
1902
1903 if (b->UserFlags.cinterface_exprdelete_on_flag)
1904 {
1905 for (vector<stp::ASTNode*>::iterator it = b->persist.begin();
1906 it != b->persist.end(); it++)
1907 delete *it;
1908 b->persist.clear();
1909 }
1910
1911 Cnf_ClearMemory();
1912 vc_clearDecls(vc);
1913 stp_i->deleteObjects();
1914
1915 delete stp_i;
1916 delete b->defaultNodeFactory;
1917 delete b;
1918 }
1919
vc_DeleteExpr(Expr e)1920 void vc_DeleteExpr(Expr e)
1921 {
1922 stp::ASTNode* input = (stp::ASTNode*)e;
1923 delete input;
1924 }
1925
getExprKind(Expr e)1926 exprkind_t getExprKind(Expr e)
1927 {
1928 stp::ASTNode* input = (stp::ASTNode*)e;
1929 return (exprkind_t)(input->GetKind());
1930 }
1931
getDegree(Expr e)1932 int getDegree(Expr e)
1933 {
1934 stp::ASTNode* input = (stp::ASTNode*)e;
1935 return input->Degree();
1936 }
1937
getBVLength(Expr ex)1938 int getBVLength(Expr ex)
1939 {
1940 stp::ASTNode* e = (stp::ASTNode*)ex;
1941
1942 if (stp::BITVECTOR_TYPE != e->GetType())
1943 {
1944 stp::FatalError("c_interface: vc_GetBVLength: "
1945 "Input expression must be a bit-vector");
1946 }
1947
1948 return e->GetValueWidth();
1949 }
1950
getType(Expr ex)1951 type_t getType(Expr ex)
1952 {
1953 stp::ASTNode* e = (stp::ASTNode*)ex;
1954 return (type_t)(e->GetType());
1955 }
1956
getVWidth(Expr ex)1957 int getVWidth(Expr ex)
1958 {
1959 stp::ASTNode* e = (stp::ASTNode*)ex;
1960 return e->GetValueWidth();
1961 }
1962
getIWidth(Expr ex)1963 int getIWidth(Expr ex)
1964 {
1965 stp::ASTNode* e = (stp::ASTNode*)ex;
1966 return e->GetIndexWidth();
1967 }
1968
vc_printCounterExampleFile(VC vc,int fd)1969 void vc_printCounterExampleFile(VC vc, int fd)
1970 {
1971 stp::STP* stp_i = (stp::STP*)vc;
1972 stp::STPMgr* b = stp_i->bm;
1973
1974 fdostream os(fd);
1975 stp::AbsRefine_CounterExample* ce =
1976 (stp::AbsRefine_CounterExample*)(stp_i->Ctr_Example);
1977
1978 bool currentPrint = b->UserFlags.print_counterexample_flag;
1979 b->UserFlags.print_counterexample_flag = true;
1980 os << "COUNTEREXAMPLE BEGIN: \n";
1981 ce->PrintCounterExample(true, os);
1982 os << "COUNTEREXAMPLE END: \n";
1983 b->UserFlags.print_counterexample_flag = currentPrint;
1984 }
1985
exprName(Expr e)1986 const char* exprName(Expr e)
1987 {
1988 return ((stp::ASTNode*)e)->GetName();
1989 }
1990
getExprID(Expr ex)1991 int getExprID(Expr ex)
1992 {
1993 stp::ASTNode q = (*(stp::ASTNode*)ex);
1994 return q.GetNodeNum();
1995 }
1996
process_argument(const char ch,VC vc)1997 void process_argument(const char ch, VC vc)
1998 {
1999 stp::STP* stp_i = (stp::STP*)vc;
2000 stp::STPMgr* bm = stp_i->bm;
2001
2002 switch (ch)
2003 {
2004 case 'a':
2005 bm->UserFlags.optimize_flag = false;
2006 break;
2007 case 'c':
2008 bm->UserFlags.construct_counterexample_flag = true;
2009 break;
2010 case 'd':
2011 bm->UserFlags.construct_counterexample_flag = true;
2012 bm->UserFlags.check_counterexample_flag = true;
2013 break;
2014
2015 case 'h':
2016 assert(0 && "This API is dumb, don't use it!");
2017 exit(-1);
2018 break;
2019 case 'm':
2020 bm->UserFlags.smtlib1_parser_flag = true;
2021 if (bm->UserFlags.smtlib2_parser_flag)
2022 stp::FatalError("Can't use both the smtlib and smtlib2 parsers");
2023 break;
2024 case 'n':
2025 bm->UserFlags.print_output_flag = true;
2026 break;
2027 case 'p':
2028 bm->UserFlags.print_counterexample_flag = true;
2029 break;
2030 case 'q':
2031 bm->UserFlags.print_arrayval_declaredorder_flag = true;
2032 break;
2033 case 'r':
2034 bm->UserFlags.ackermannisation = true;
2035 break;
2036 case 's':
2037 bm->UserFlags.stats_flag = true;
2038 break;
2039 case 't':
2040 bm->UserFlags.quick_statistics_flag = true;
2041 break;
2042 case 'v':
2043 bm->UserFlags.print_nodes_flag = true;
2044 break;
2045 case 'w':
2046 bm->UserFlags.wordlevel_solve_flag = false;
2047 break;
2048 case 'y':
2049 bm->UserFlags.print_binary_flag = true;
2050 break;
2051 default:
2052 // fprintf(stderr,usage,prog);
2053 // cout << helpstring;
2054 assert(0 && "Unrecognised option");
2055 exit(-1);
2056 break;
2057 }
2058 }
2059
2060 //////////////////////////////////////////////////////////////////////////
2061 // extended version
2062
vc_parseMemExpr(VC vc,const char * s,Expr * oquery,Expr * oasserts)2063 int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts)
2064 {
2065 stp::STP* stp_i = (stp::STP*)vc;
2066 stp::STPMgr* b = stp_i->bm;
2067
2068 #if 0
2069 stp::GlobalSTP = (stp::STP*)vc;
2070 CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
2071 if(0 != c) {
2072 cout << CONSTANTBV::BitVector_Error(c) << endl;
2073 return 0;
2074 }
2075 #endif
2076
2077 stp::Cpp_interface pi(*b, b->defaultNodeFactory);
2078 stp::GlobalParserInterface = π
2079
2080 stp::ASTVec AssertsQuery;
2081 if (b->UserFlags.smtlib1_parser_flag)
2082 {
2083 // YY_BUFFER_STATE bstat = smt_scan_string(s);
2084 // smt_switch_to_buffer(bstat);
2085 stp::GlobalSTP = stp_i;
2086 stp::GlobalParserBM = b;
2087 stp::SMTScanString(s);
2088 smtparse((void*)&AssertsQuery);
2089 // smt_delete_buffer(bstat);
2090 stp::GlobalSTP = NULL;
2091 stp::GlobalParserBM = NULL;
2092 }
2093 else
2094 {
2095 // YY_BUFFER_STATE bstat = cvc_scan_string(s);
2096 // cvc_switch_to_buffer(bstat);
2097 stp::GlobalSTP = stp_i;
2098 stp::GlobalParserBM = b;
2099 stp::CVCScanString(s);
2100 cvcparse((void*)&AssertsQuery);
2101 // cvc_delete_buffer(bstat);
2102 stp::GlobalSTP = NULL;
2103 stp::GlobalParserBM = NULL;
2104 }
2105
2106 if (oquery)
2107 {
2108 *(stp::ASTNode**)oquery = new stp::ASTNode(AssertsQuery[1]);
2109 }
2110 if (oasserts)
2111 {
2112 *(stp::ASTNode**)oasserts = new stp::ASTNode(AssertsQuery[0]);
2113 }
2114 return 1;
2115 }
2116
_vc_useSolver(VC vc,stp::UserDefinedFlags::SATSolvers solver)2117 void _vc_useSolver(VC vc, stp::UserDefinedFlags::SATSolvers solver)
2118 {
2119 /* Helper method to encapsulate setting a solver */
2120 stp::STP* stp_i = (stp::STP*)vc;
2121 stp::STPMgr* b = stp_i->bm;
2122 b->UserFlags.solver_to_use = solver;
2123 }
2124
_vc_isUsingSolver(VC vc,stp::UserDefinedFlags::SATSolvers solver)2125 bool _vc_isUsingSolver(VC vc, stp::UserDefinedFlags::SATSolvers solver)
2126 {
2127 /* Helper method to encapsulate getting a solver */
2128 stp::STP* stp_i = (stp::STP*)vc;
2129 stp::STPMgr* b = stp_i->bm;
2130 return b->UserFlags.solver_to_use == solver;
2131 }
2132
vc_supportsMinisat(VC vc)2133 bool vc_supportsMinisat(VC vc)
2134 {
2135 return true;
2136 }
2137
vc_useMinisat(VC vc)2138 bool vc_useMinisat(VC vc)
2139 {
2140 _vc_useSolver(vc, stp::UserDefinedFlags::MINISAT_SOLVER);
2141 return true;
2142 }
2143
vc_isUsingMinisat(VC vc)2144 bool vc_isUsingMinisat(VC vc)
2145 {
2146 return _vc_isUsingSolver(vc, stp::UserDefinedFlags::MINISAT_SOLVER);
2147 }
2148
vc_supportsSimplifyingMinisat(VC vc)2149 bool vc_supportsSimplifyingMinisat(VC vc )
2150 {
2151 return true;
2152 }
2153
vc_useSimplifyingMinisat(VC vc)2154 bool vc_useSimplifyingMinisat(VC vc)
2155 {
2156 _vc_useSolver(vc, stp::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER);
2157 return true;
2158 }
2159
vc_isUsingSimplifyingMinisat(VC vc)2160 bool vc_isUsingSimplifyingMinisat(VC vc)
2161 {
2162 return _vc_isUsingSolver(vc, stp::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER);
2163 }
2164
vc_supportsCryptominisat(VC vc)2165 bool vc_supportsCryptominisat(VC vc )
2166 {
2167 #ifdef USE_CRYPTOMINISAT
2168 return true;
2169 #else
2170 return false;
2171 #endif
2172 }
2173
vc_useCryptominisat(VC vc)2174 bool vc_useCryptominisat(VC vc
2175 #ifndef USE_CRYPTOMINISAT
2176
2177 #endif
2178 )
2179 {
2180 #ifdef USE_CRYPTOMINISAT
2181 _vc_useSolver(vc, stp::UserDefinedFlags::CRYPTOMINISAT5_SOLVER);
2182 return true;
2183 #else
2184 return false;
2185 #endif
2186 }
2187
vc_isUsingCryptominisat(VC vc)2188 bool vc_isUsingCryptominisat(VC vc
2189 #ifndef USE_CRYPTOMINISAT
2190
2191 #endif
2192 )
2193 {
2194 #ifdef USE_CRYPTOMINISAT
2195 return _vc_isUsingSolver(vc, stp::UserDefinedFlags::CRYPTOMINISAT5_SOLVER);
2196 #else
2197 return false;
2198 #endif
2199 }
2200
vc_supportsRiss(VC vc)2201 bool vc_supportsRiss(VC vc )
2202 {
2203 #ifdef USE_RISS
2204 return true;
2205 #else
2206 return false;
2207 #endif
2208 }
2209
vc_useRiss(VC vc)2210 bool vc_useRiss(VC vc
2211 #ifndef USE_RISS
2212
2213 #endif
2214 )
2215 {
2216 #ifdef USE_RISS
2217 _vc_useSolver(vc, stp::UserDefinedFlags::RISS_SOLVER);
2218 return true;
2219 #else
2220 return false;
2221 #endif
2222 }
2223
vc_isUsingRiss(VC vc)2224 bool vc_isUsingRiss(VC vc
2225 #ifndef USE_RISS
2226
2227 #endif
2228 )
2229 {
2230 #ifdef USE_RISS
2231 return _vc_isUsingSolver(vc, stp::UserDefinedFlags::RISS_SOLVER);
2232 #else
2233 return false;
2234 #endif
2235 }
2236
2237