From 104d5d3a6620e2999a018349ebb8313b9406e507 Mon Sep 17 00:00:00 2001 From: Rajdeep Mukherjee Date: Wed, 20 Dec 2017 11:44:40 +0000 Subject: [PATCH] optimizations in deduction phase --- regression/acdl/FIFO/main.c | 153 ----- regression/acdl/FIFO/test.desc | 6 - regression/acdl/Makefile | 8 +- regression/acdl/branch4/main.c | 1 - regression/acdl/bug0/debug | 114 ---- regression/acdl/bug0/run.sh | 1 - regression/acdl/bug1/run.sh | 1 - regression/acdl/bug2/run.sh | 1 - regression/acdl/bug3/debug | 5 - regression/acdl/bug3/run.sh | 1 - regression/acdl/loop2/main.c | 2 +- regression/acdl/run-acdls-interval.sh | 19 + regression/acdl/run-acdls-octagon.sh | 19 + regression/acdl/statistics.py | 90 +++ regression/acdl/statistics.sh | 1 + regression/acdl/switch6/main.c | 18 - regression/acdl/switch6/test.desc | 6 - src/2ls/summary_checker_acdl.cpp | 7 +- src/acdl/acdl_domain.cpp | 673 +++++++++++++++++++- src/acdl/acdl_domain.h | 20 + src/acdl/acdl_solver.cpp | 637 ++++++++++++++++-- src/acdl/acdl_solver.h | 4 +- src/acdl/acdl_worklist_base.cpp | 16 + src/acdl/acdl_worklist_base.h | 2 + src/acdl/acdl_worklist_forward_strategy.cpp | 2 +- src/domains/tpolyhedra_domain.cpp | 2 +- 26 files changed, 1421 insertions(+), 388 deletions(-) delete mode 100644 regression/acdl/FIFO/main.c delete mode 100644 regression/acdl/FIFO/test.desc delete mode 100644 regression/acdl/bug0/debug delete mode 100755 regression/acdl/bug0/run.sh delete mode 100755 regression/acdl/bug1/run.sh delete mode 100755 regression/acdl/bug2/run.sh delete mode 100644 regression/acdl/bug3/debug delete mode 100755 regression/acdl/bug3/run.sh create mode 100755 regression/acdl/run-acdls-interval.sh create mode 100755 regression/acdl/run-acdls-octagon.sh create mode 100644 regression/acdl/statistics.py create mode 100755 regression/acdl/statistics.sh delete mode 100644 regression/acdl/switch6/main.c delete mode 100644 regression/acdl/switch6/test.desc diff --git a/regression/acdl/FIFO/main.c b/regression/acdl/FIFO/main.c deleted file mode 100644 index f29c81af4..000000000 --- a/regression/acdl/FIFO/main.c +++ /dev/null @@ -1,153 +0,0 @@ -#include -#include - -_Bool nondet_bool(); -unsigned char nondet_uchar(); - -int MSBD = 3; -int LAST = 1; -int MSBA = 3; - -struct state_elements_srFIFO { - _Bool empty; - unsigned char mem[16]; - unsigned char tail; -}; -struct state_elements_srFIFO ssrFIFO; - -void initial_srFIFO() { - int i; - //for(i = 0; i <= LAST; i = i + 1) - ssrFIFO.mem[0] = 0; - ssrFIFO.tail = 0; - ssrFIFO.empty = 1; -} - -void srFIFO(_Bool clock, unsigned char dataIn, _Bool push, _Bool pop, unsigned char *dataOut, _Bool *full, _Bool *empty) -{ - int i; - unsigned char tmp1; - // clocked block - if(push && !*full) - { - //for(i = LAST; i > 0; i = i - 1) - ssrFIFO.mem[0] = (ssrFIFO.mem[i - 1] & 0xF); - ssrFIFO.mem[0] = dataIn & 0xF; - - if(!ssrFIFO.empty) - ssrFIFO.tail = (ssrFIFO.tail + 1) & 0xF; - ssrFIFO.empty = 0; - *empty = 0; - } - - else - if(pop && !ssrFIFO.empty) - { - if(ssrFIFO.tail == 0) - { - ssrFIFO.empty = 1; - *empty = 1; - } - else - ssrFIFO.tail = ((ssrFIFO.tail & 0xF) - 1) & 0xF; - } - - tmp1 = ssrFIFO.tail & 0xF; - *dataOut = (ssrFIFO.mem[tmp1]) & 0xF; - *full = ((ssrFIFO.tail & 0xF) == LAST); -} - -struct state_elements_rbFIFO{ - _Bool empty; - unsigned char mem[16]; - unsigned char head; - unsigned char tail; -}; -struct state_elements_rbFIFO srbFIFO; - -void initial_rbFIFO() -{ - int i; - //for(i = 0;i <= LAST; i = i + 1) - srbFIFO.mem[0] = 0; - srbFIFO.head = 0; - srbFIFO.tail = 0; - srbFIFO.empty = 1; -} - -void rbFIFO(_Bool clock, unsigned char dataIn, _Bool push, _Bool pop, unsigned char *dataOut, _Bool *full, _Bool *empty) -{ - unsigned char tmp1, tmp2; - - if(push && !*full) - { - tmp1 = srbFIFO.head & 0xF; - srbFIFO.mem[tmp1] = dataIn & 0xF; - srbFIFO.head = ((srbFIFO.head & 0xF) + 1) & 0xF; - srbFIFO.empty = 0; - *empty = 0; - } - - else - if(pop && !srbFIFO.empty) - { - srbFIFO.tail = ((srbFIFO.tail & 0xf) + 1) & 0xF; - if((srbFIFO.tail & 0xF) == (srbFIFO.head & 0xF)) { - srbFIFO.empty = 1; - *empty = 1; - } - } - tmp2 = srbFIFO.tail & 0xF; - *dataOut = (srbFIFO.mem[tmp2]) & 0xF; - *full = ((srbFIFO.tail & 0xF) == (srbFIFO.head & 0xF)) & (!srbFIFO.empty ); -} - -/* -struct state_elements_main{ - struct state_elements_srFIFO sr; - struct state_elements_rbFIFO rb; -}; -struct state_elements_main smain; -*/ - -unsigned char srDataOut; -_Bool srFull; -_Bool srEmpty; -unsigned char rbDataOut; -_Bool rbFull; -_Bool rbEmpty; - -_Bool design(_Bool clock, unsigned char dataIn, _Bool push, _Bool pop, _Bool *equal) -{ - - srFIFO(clock, dataIn, push, pop, &srDataOut, &srFull, &srEmpty); - rbFIFO(clock, dataIn, push, pop, &rbDataOut, &rbFull, &rbEmpty); - // the below should fail - //*equal = ((srFull == rbFull) && (smain.sr.empty == smain.rb.empty) && (smain.sr.empty | (srDataOut == rbDataOut))); - *equal = ((srFull == rbFull) && (ssrFIFO.empty == srbFIFO.empty) && (ssrFIFO.empty || (srDataOut == rbDataOut))); - //assert(srFull == rbFull); - //assert(srEmpty == rbEmpty); - //assert(srDataOut == rbDataOut); - - assert(*equal != 1); -} - - -void main() { - _Bool clock; - unsigned char dataIn; - _Bool push; - _Bool pop; - _Bool equal; - - initial_rbFIFO(); - initial_srFIFO(); - - //while(1) { - push = nondet_bool(); - pop = nondet_bool(); - dataIn = nondet_uchar(); - design(clock, dataIn, push, pop, &equal); - //assert(equal == 1); - //} -} diff --git a/regression/acdl/FIFO/test.desc b/regression/acdl/FIFO/test.desc deleted file mode 100644 index 2aa99167b..000000000 --- a/regression/acdl/FIFO/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -THOROUGH -main.c ---inline -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ diff --git a/regression/acdl/Makefile b/regression/acdl/Makefile index 75b85f1c1..69d94aa03 100644 --- a/regression/acdl/Makefile +++ b/regression/acdl/Makefile @@ -1,12 +1,12 @@ default: tests.log -FLAGS = --verbosity 10 --acdl --decision equality --learning first-uip --propagate chaotic --inline +FLAGS = --verbosity 10 --acdl --decision ordered --learning first-uip --propagate chaotic --inline test: - @../test.pl -c "/usr/bin/time ../../../src/2ls/2ls $(FLAGS)" + @../test.pl -c "/usr/bin/time ../../src/2ls/2ls $(FLAGS)" tests.log: ../test.pl - @../test.pl -c "../../../src/2ls/2ls $(FLAGS)" + @../test.pl -c "../../src/2ls/2ls $(FLAGS)" show: @for dir in *; do \ @@ -17,4 +17,4 @@ show: clean: @rm -f *.log - @for dir in *; do rm -f $$dir/*.out; done; + @for dir in *; do rm -f $$dir/*.{sv,dat,log,out,cnf,smt2,aag,aig,v,git,svn,nfs}; rm -f $$dir/*.nfs*; done; diff --git a/regression/acdl/branch4/main.c b/regression/acdl/branch4/main.c index a450f6e71..15fea75c3 100644 --- a/regression/acdl/branch4/main.c +++ b/regression/acdl/branch4/main.c @@ -1,6 +1,5 @@ int main() { int x, y; -_Bool c; if(y<0) x=0; else diff --git a/regression/acdl/bug0/debug b/regression/acdl/bug0/debug deleted file mode 100644 index 61842e390..000000000 --- a/regression/acdl/bug0/debug +++ /dev/null @@ -1,114 +0,0 @@ - -Pop: i#phi21%1 == i#23%2 -prop_trail size is: 28 -control_trail is empty -Computing old abstract value of implication graph: -$guard#22%0 -!(-((signed __CPROVER_bitvector[33])i#phi21%0) >= 0) -!$guard#ls24%2 -!(i#20 >= 1) -!(-((signed __CPROVER_bitvector[33])i#20) >= 1) -$guard#0 -$cond#24%1 -$cond#24%2 -!$cond#21%0 -$guard#21%0 -$guard#ls24%0 -!(-((signed __CPROVER_bitvector[33])i#lb24%0) >= 0) -!(i#phi21%0 >= 4) -!(i#phi21 >= 4) -!(-((signed __CPROVER_bitvector[33])i#phi21) >= 0) -!(i#23%1 >= 4) -!(-((signed __CPROVER_bitvector[33])i#23%1) >= 0) -!$cond#21 -$guard#21 -$guard#22%1 -!(i#phi21%2 >= 1) -!(-((signed __CPROVER_bitvector[33])i#phi21%2) >= 1) -!(i#phi21%1 >= 3) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 1) -!$cond#21%1 -$guard#21%1 -!(i#23%2 >= 2) -!(-((signed __CPROVER_bitvector[33])i#23%2) >= 0) -Popped Statement for live variables: i#phi21%1 == i#23%2 -Variables in Popped Statement: i#23%2 i#phi21%1 -Live variables list are as follows: $cond#21$cond#21%1$cond#21%2$cond#24%2$guard#0$guard#21$guard#21%1$guard#21%2$guard#22%2$guard#25i#23%2i#phi21%1i#phi21%2 -Deleted live variables are: i#23%2 -The content of the updated worklist is as follows: -Updated Worklist Element::$cond#21%1 == i#phi21%1 >= 4 -Updated Worklist Element::$guard#21%1 == ($guard#22%2 && $cond#24%2) -Updated Worklist Element::$cond#21%2 == i#phi21%2 >= 4 -Updated Worklist Element::$guard#21%2 == $guard#0 -Updated Worklist Element::$guard#25 == ($cond#21 && $guard#21) -The updated live variables after removal are as follows: $cond#21$cond#21%1$cond#21%2$cond#24%2$guard#0$guard#21$guard#21%1$guard#21%2$guard#22%2$guard#25i#phi21%1i#phi21%2 -New: !(i#phi21%1 >= 2) && !(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 0) -prop_trail size is: 30 -control_trail is empty -Computing new abstract value of implication graph: -!(i#phi21%1 >= 2) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 0) -$guard#22%0 -!(-((signed __CPROVER_bitvector[33])i#phi21%0) >= 0) -!$guard#ls24%2 -!(i#20 >= 1) -!(-((signed __CPROVER_bitvector[33])i#20) >= 1) -$guard#0 -$cond#24%1 -$cond#24%2 -!$cond#21%0 -$guard#21%0 -$guard#ls24%0 -!(-((signed __CPROVER_bitvector[33])i#lb24%0) >= 0) -!(i#phi21%0 >= 4) -!(i#phi21 >= 4) -!(-((signed __CPROVER_bitvector[33])i#phi21) >= 0) -!(i#23%1 >= 4) -!(-((signed __CPROVER_bitvector[33])i#23%1) >= 0) -!$cond#21 -$guard#21 -$guard#22%1 -!(i#phi21%2 >= 1) -!(-((signed __CPROVER_bitvector[33])i#phi21%2) >= 1) -!(i#phi21%1 >= 3) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 1) -!$cond#21%1 -$guard#21%1 -!(i#23%2 >= 2) -!(-((signed __CPROVER_bitvector[33])i#23%2) >= 0) -!(i#phi21%1 >= 2) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 0) -Pop: $cond#21%1 == i#phi21%1 >= 4 -prop_trail size is: 30 -control_trail is empty -Computing old abstract value of implication graph: -$guard#22%0 -!(-((signed __CPROVER_bitvector[33])i#phi21%0) >= 0) -!$guard#ls24%2 -!(i#20 >= 1) -!(-((signed __CPROVER_bitvector[33])i#20) >= 1) -$guard#0 -$cond#24%1 -$cond#24%2 -!$cond#21%0 -$guard#21%0 -$guard#ls24%0 -!(-((signed __CPROVER_bitvector[33])i#lb24%0) >= 0) -!(i#phi21%0 >= 4) -!(i#phi21 >= 4) -!(-((signed __CPROVER_bitvector[33])i#phi21) >= 0) -!(i#23%1 >= 4) -!(-((signed __CPROVER_bitvector[33])i#23%1) >= 0) -!$cond#21 -$guard#21 -$guard#22%1 -!(i#phi21%2 >= 1) -!(-((signed __CPROVER_bitvector[33])i#phi21%2) >= 1) -!(i#phi21%1 >= 3) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 1) -!$cond#21%1 -$guard#21%1 -!(i#23%2 >= 2) -!(-((signed __CPROVER_bitvector[33])i#23%2) >= 0) -!(i#phi21%1 >= 2) -!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 0) diff --git a/regression/acdl/bug0/run.sh b/regression/acdl/bug0/run.sh deleted file mode 100755 index d7c3098b6..000000000 --- a/regression/acdl/bug0/run.sh +++ /dev/null @@ -1 +0,0 @@ -2ls main.c --acdl --acdl-decision ordered --acdl-conflict first-uip --unwind 3 diff --git a/regression/acdl/bug1/run.sh b/regression/acdl/bug1/run.sh deleted file mode 100755 index 5ca90fefd..000000000 --- a/regression/acdl/bug1/run.sh +++ /dev/null @@ -1 +0,0 @@ -2ls main.c --acdl --acdl-decision ordered --acdl-conflict first-uip --unwind 2 diff --git a/regression/acdl/bug2/run.sh b/regression/acdl/bug2/run.sh deleted file mode 100755 index 5ca90fefd..000000000 --- a/regression/acdl/bug2/run.sh +++ /dev/null @@ -1 +0,0 @@ -2ls main.c --acdl --acdl-decision ordered --acdl-conflict first-uip --unwind 2 diff --git a/regression/acdl/bug3/debug b/regression/acdl/bug3/debug deleted file mode 100644 index abb23f3f7..000000000 --- a/regression/acdl/bug3/debug +++ /dev/null @@ -1,5 +0,0 @@ -search for "FALSE <==", how can the following deduce to FALSE. -[ACDL-DOMAIN] deductions: FALSE <== !(y#phi64%2 >= 10) && !(-((signed -__CPROVER_bitvector[33])y#phi64%2) >= -4) && !(-((signed -__CPROVER_bitvector[33])y#phi46%1) >= -4) && !(-((signed -__CPROVER_bitvector[33])y#phi46%1) >= -8) && !(y#phi64%2 >= 9) diff --git a/regression/acdl/bug3/run.sh b/regression/acdl/bug3/run.sh deleted file mode 100755 index abaf3d2f5..000000000 --- a/regression/acdl/bug3/run.sh +++ /dev/null @@ -1 +0,0 @@ -2ls main.c --acdl --acdl-decision ordered --acdl-conflict first-uip --unwind 1 diff --git a/regression/acdl/loop2/main.c b/regression/acdl/loop2/main.c index 31eca0e89..27233d833 100644 --- a/regression/acdl/loop2/main.c +++ b/regression/acdl/loop2/main.c @@ -1,7 +1,7 @@ int main() { int x=0,i; for(i=0;i<10;i++) - x = x+i; + x = x+i; assert(x<10); } diff --git a/regression/acdl/run-acdls-interval.sh b/regression/acdl/run-acdls-interval.sh new file mode 100755 index 000000000..0f37aee7e --- /dev/null +++ b/regression/acdl/run-acdls-interval.sh @@ -0,0 +1,19 @@ +PWD=`pwd` +TIMEOUT=3600 +TOOL=acdls +BENCHMARKDIRS=`cat benchmarks-intv.txt` +PROGRESSLOG=${PWD}/progress.log-intervals-${TOOL} +FLAGS="--inline --acdl --decision ordered --propagate chaotic --learning first-uip" +EXEC=/users/rajdeep/thesis-tool-webpage/acdlp_thesis_version/2ls/src/2ls/2ls +echo "Starting experiments at `date` on `hostname`" > ${PROGRESSLOG} +for DIR in $BENCHMARKDIRS +do + echo ${DIR} + cd ${DIR} + LOG=${PWD}/logintv-${DIR} + filename=main.c + echo "Starting to processing $DIR/$filename at `date`" >> ${PROGRESSLOG} + runsolver -C $TIMEOUT -W $TIMEOUT -d 1 -M 32768 ${EXEC} ${FLAGS} $filename >> ${LOG} + echo "done at `date`" >> ${PROGRESSLOG} + cd ../ +done diff --git a/regression/acdl/run-acdls-octagon.sh b/regression/acdl/run-acdls-octagon.sh new file mode 100755 index 000000000..9c1cc6987 --- /dev/null +++ b/regression/acdl/run-acdls-octagon.sh @@ -0,0 +1,19 @@ +PWD=`pwd` +TIMEOUT=3600 +TOOL=acdls +BENCHMARKDIRS=`cat benchmarks-octagons.txt` +PROGRESSLOG=${PWD}/progress.log-oct-${TOOL} +FLAGS="--inline --acdl --decision ordered --propagate chaotic --learning first-uip --octagons" +EXEC=/users/rajdeep/thesis-tool-webpage/acdlp_thesis_version/2ls/src/2ls/2ls +echo "Starting experiments at `date` on `hostname`" > ${PROGRESSLOG} +for DIR in $BENCHMARKDIRS +do + echo ${DIR} + cd ${DIR} + LOG=${PWD}/logoct-${DIR} + filename=main.c + echo "Starting to processing $DIR/$filename at `date`" >> ${PROGRESSLOG} + runsolver -C $TIMEOUT -W $TIMEOUT -d 1 -M 32768 ${EXEC} ${FLAGS} $filename >> ${LOG} + echo "done at `date`" >> ${PROGRESSLOG} + cd ../ +done diff --git a/regression/acdl/statistics.py b/regression/acdl/statistics.py new file mode 100644 index 000000000..08aa6ac51 --- /dev/null +++ b/regression/acdl/statistics.py @@ -0,0 +1,90 @@ +#!/usr/bin/python + +import sys +import re +import subprocess +import csv +import os +import fnmatch + +def processfile(): + + src_path=sys.argv[1] + + properties=0 + verified_prop=0 + false_prop=0 + inconclusive_prop=0 + timeout_prop=0 + memout_prop=0 + error_prop=0 + sum_runtime=0.0 + sum_peak_memory=0.0 + decisions=0 + propagations=0 + conflicts=0 + conflict_literals=0 + learnt_clauses=0 + result="" + # temporary variable + status="" + f_name="" + func_name="" + time=0.0 + + status_decision = re.compile("Decisions::") + status_propagation = re.compile("Propagation::") + status_conflict = re.compile("Learning Iterations::") + status_conflict_literal = re.compile("Learnt literals::") + status_learnt_clauses = re.compile("Learnt clauses::") + status_time = re.compile("runsolver_cputime:") + status_result = re.compile("VERIFICATION") + + report_file=open('statistics.csv', 'wb') + report = csv.writer(report_file, delimiter=',', + quotechar='|', quoting=csv.QUOTE_MINIMAL) + report.writerow(['decisions', 'propagations', 'conflicts', 'conflict literals', 'learnt clauses', 'Time', 'Result']) + for root, dirs, filenames in os.walk(src_path): + for f in filenames: + if fnmatch.fnmatch(f, 'logintv*'): + #if f.endswith(".out"): + log = open(src_path + f, 'r') + lines=[line for line in log] + for line in lines: + if status_decision.search(line): + cols=line.split('::') + str1=cols[1].lstrip() + dec=str1.split(' ',1)[0] + decisions = int(dec) + if status_propagation.search(line): + cols=line.split('::') + str1=cols[1].lstrip() + prop=str1.split(' ',1)[0] + propagations = int(prop) + if status_conflict.search(line): + cols=line.split('::') + str1=cols[1].lstrip() + #str2=st1.rstrip() + con=str1.split(' ',1)[0] + conflicts = int(con) + if status_conflict_literal.search(line): + cols=line.split('::') + str1=cols[1].lstrip() + lit=str1.split(' ',1)[0] + conflict_literals = int(lit) + if status_learnt_clauses.search(line): + cols=line.split('::') + str1=cols[1].lstrip() + res=str1.split(' ',1)[0] + learnt_clauses = int(res) + if status_result.search(line): + result = line + if status_time.search(line): + cols=line.split(':') + str1=cols[1].lstrip() + t=str1.split(' ',1)[0] + time= float(t) + report.writerow([decisions,propagations,conflicts,conflict_literals,learnt_clauses,time,result]) + print root, decisions, propagations, conflicts, conflict_literals, learnt_clauses, time, result + +processfile() diff --git a/regression/acdl/statistics.sh b/regression/acdl/statistics.sh new file mode 100755 index 000000000..44d441ede --- /dev/null +++ b/regression/acdl/statistics.sh @@ -0,0 +1 @@ +WORKSPACE=/users/rajdeep/thesis-tool-webpage/acdlp_thesis_version/2ls/regression/acdl ./result.sh diff --git a/regression/acdl/switch6/main.c b/regression/acdl/switch6/main.c deleted file mode 100644 index e61cc2775..000000000 --- a/regression/acdl/switch6/main.c +++ /dev/null @@ -1,18 +0,0 @@ -#include - -enum { ASD1, ASD2 } e; - -int main() -{ - const char *p; - - e=ASD1; - - p=({ const char *tmp; - switch(e) { case ASD1: tmp="abc"; } tmp; }); - - assert(p[0]=='a'); - assert(p[1]=='b'); - assert(p[2]=='c'); - assert(p[3]==0); -} diff --git a/regression/acdl/switch6/test.desc b/regression/acdl/switch6/test.desc deleted file mode 100644 index 741e6a467..000000000 --- a/regression/acdl/switch6/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -THOROUGH -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ diff --git a/src/2ls/summary_checker_acdl.cpp b/src/2ls/summary_checker_acdl.cpp index 3f3fe10ac..309f26651 100644 --- a/src/2ls/summary_checker_acdl.cpp +++ b/src/2ls/summary_checker_acdl.cpp @@ -43,9 +43,11 @@ property_checkert::resultt summary_checker_acdlt::operator()( const goto_modelt &goto_model) { const namespacet ns(goto_model.symbol_table); - SSA_functions(goto_model, ns); ssa_unwinder.init(false, false); + + irep_idt entry_point=goto_model.goto_functions.entry_point(); + local_SSAt &SSA=ssa_db.get(entry_point); unsigned unwind=options.get_unsigned_int_option("unwind"); if(unwind>0) @@ -55,9 +57,8 @@ property_checkert::resultt summary_checker_acdlt::operator()( ssa_unwinder.unwind_all(unwind); } - irep_idt entry_point=goto_model.goto_functions.entry_point(); + SSA.output_verbose(std::cout); std::cout << entry_point << std::endl; - local_SSAt &SSA=ssa_db.get(entry_point); ssa_local_unwindert &ssa_local_unwinder=ssa_unwinder.get(entry_point); const goto_programt &goto_program=SSA.goto_function.body; diff --git a/src/acdl/acdl_domain.cpp b/src/acdl/acdl_domain.cpp index 335a78076..c54f5e0bb 100644 --- a/src/acdl/acdl_domain.cpp +++ b/src/acdl/acdl_domain.cpp @@ -27,6 +27,8 @@ Author: Rajdeep Mukherjee, Peter Schrammel #include "acdl_domain.h" #include "template_generator_acdl.h" +#define BOX 1 +#define OCTAGONS 0 #define NO_PROJECTION /*******************************************************************\ @@ -91,9 +93,11 @@ void acdl_domaint::operator()( new_value, deductions); if(deductions.empty()) { - bool_inference(statement, bool_vars, old_value, - new_value, deductions); - numerical_inference(statement, num_vars, old_value, + if(!bool_vars.empty()) + bool_inference(statement, bool_vars, old_value, + new_value, deductions); + if(!num_vars.empty()) + numerical_inference(statement, num_vars, old_value, num_new_value, num_deductions); // collect results new_value.insert(new_value.end(), num_new_value.begin(), @@ -217,18 +221,21 @@ void acdl_domaint::bool_inference( ssa_analyzert ssa_analyzer; std::unique_ptr solver( incremental_solvert::allocate(SSA.ns, true)); - varst pvars; - pvars.insert(*it); + /*varst pvars; + pvars.insert(*it);*/ // project _old_value on everything in statement but *it valuet old_value; - remove_vars(_old_value, pvars, old_value); - + //remove_vars(_old_value, pvars, old_value); +#ifdef NO_PROJECTION + old_value=_old_value; +#else + remove_var(_old_value, *it, old_value); #ifdef DEBUG std::cout << "[ACDL-DOMAIN] projected(" << it->get_identifier() << "): "; output(std::cout, old_value) << std::endl; #endif - +#endif meet_irreduciblet deduced; // inference for booleans @@ -276,9 +283,9 @@ void acdl_domaint::bool_inference( { new_value.push_back(deduced); deductions.push_back(deduced); + boolean_deductions.push_back(deduced); } } - // pop_context not needed } else // bottom @@ -287,6 +294,7 @@ void acdl_domaint::bool_inference( std::cout << "deducing in BOTTOM" << std::endl; #endif deductions.push_back(false_exprt()); + boolean_deductions.push_back(false_exprt()); break; // at this point we have a conflict, we return } @@ -318,6 +326,11 @@ void acdl_domaint::numerical_inference( { // add variables in old value varst tvars=vars; + + // ONLY NEEDED for OCTAGON DOMAIN DEDUCTIONS + // Witout this, bottom13 (octagon) does not terminate +//#ifdef OCTAGONS +#if 0 for(valuet::const_iterator it=_old_value.begin(); it!=_old_value.end(); ++it) { @@ -325,6 +338,7 @@ void acdl_domaint::numerical_inference( find_symbols(*it, symbols); tvars.insert(symbols.begin(), symbols.end()); } +#endif #ifdef DEBUG std::cout << "The total number of variables passed to the template generator is " << tvars.size() << std::endl; @@ -342,9 +356,9 @@ void acdl_domaint::numerical_inference( deductions.reserve(1); #else deductions.reserve(vars.size()); +#endif for(varst::const_iterator it=vars.begin(); it!=vars.end(); ++it) -#endif { ssa_analyzert ssa_analyzer; std::unique_ptr solver( @@ -356,7 +370,7 @@ void acdl_domaint::numerical_inference( old_value=_old_value; #else remove_var(_old_value, *it, old_value); -#if def DEBUG +#ifdef DEBUG std::cout << "[ACDL-DOMAIN] projected(" << from_expr(SSA.ns, "", *it) << "): "; output(std::cout, old_value) << std::endl; @@ -392,25 +406,52 @@ void acdl_domaint::numerical_inference( for(unsigned i=0; inew_context(); *solver << not_exprt(var_values[i]); decision_proceduret::resultt result=(*solver)(); assert(result==decision_proceduret::D_UNSATISFIABLE); - +#if 0 + new_value.push_back(var_values[i]); + deductions.push_back(var_values[i]); + solver->pop_context(); +#endif +#ifdef BOX + bool update = update_var_bound(var_values[i], _old_value); +#endif + // We can avoid the syntactic check if update returns true, + // in which case we can safely insert the deduction. #ifdef DEBUG std::cout << "IS_SUBSUMED: " << std::endl; std::cout << " " << from_expr(SSA.ns, "", var_values[i]) << std::endl; std::cout << " "; output(std::cout, _old_value); std::cout << std::endl; #endif + // This is needed to keep the size of the + // Implication graph under control. The following + // scenario must be handled. + // Case 1: lower bound: x>=0 -> x>=-50, so when x>=0 is present, do not insert x>=-50. Otherwise, insert + // Case 2: upper bound: x<=10->x<=20, if x<=10 is present, then do not insert x<=20. Otherwise insert. + +#ifdef BOX + if(update) + { +#ifdef DEBUG + std::cout << "adding new value through Var bound update" << from_expr(SSA.ns, "", var_values[i]) << std::endl; +#endif + new_value.push_back(var_values[i]); + deductions.push_back(var_values[i]); + } +#else if(!is_subsumed_syntactic(var_values[i], _old_value)) { #ifdef DEBUG - std::cout << "adding new value " << from_expr(SSA.ns, "", var_values[i]) << std::endl; + std::cout << "adding new value through syntactic check" << from_expr(SSA.ns, "", var_values[i]) << std::endl; #endif new_value.push_back(var_values[i]); deductions.push_back(var_values[i]); } +#endif solver->pop_context(); } @@ -543,9 +584,13 @@ void acdl_domaint::normalize_meetirrd(const meet_irreduciblet &m, meet_irreducib Function: acdl_domaint::is_subsumed_syntactic() - Inputs: example: 1. x<=3, 0<=x && x<=3 - 2. x<=2, 0<=x && x<=3 - 3. x<=5, 3<=x && x<=3 + Inputs: + 1. x<=3, 0<=x && x<=3 + 2. x<=5, 3<=x && x<=3 + 3. x<=2, 0<=x && x<=3 (updated upper bound=2) + 4. x<=3, 0<=x && x<=2 (don't update, upper bound=2) + 5. x>=7, x>=5 && x<=10 (lower bound = 7) + 6. x>=3, x>=5 && x<=10 (don't update, lower bound = 5) Outputs: example 1: true 2. false 3. false @@ -2772,6 +2817,7 @@ bool acdl_domaint::gamma_complete_deduction(const exprt &ssa_conjunction, std::unique_ptr solver( incremental_solvert::allocate(SSA.ns, true)); + std::cout << "SAT solver statistics" << std::endl; *solver << and_exprt(ssa_conjunction, conjunction(value)); if((*solver)()==decision_proceduret::D_SATISFIABLE) { @@ -2857,3 +2903,598 @@ void acdl_domaint::operator()( // assert(false); } + +/*******************************************************************\ + + Function: acdl_domaint::check_val_syntactic(m,val) + + Inputs: 1) m:= (x>20), val:= (x>10 && y<20) + 2) m:= (x>20), val:= (y<20) + + Outputs: true + false + Purpose: Check whether variable in m is at all present in + val, value of m does not matter, pure syntactic check + +\******************************************************************/ +bool acdl_domaint::check_val_syntactic(const meet_irreduciblet &m, + const valuet &value) const +{ + if(value.empty()) + return false; + + std::cout << "Syntactic match -1 " << m.pretty() << std::endl; + exprt mt; + if(m.id()==ID_symbol || + (m.id()==ID_not && m.op0().id()==ID_symbol)) + mt = m; + else if(m.op0().id()==ID_typecast) + { + mt = m.op0().op0(); + } + std::cout << "Syntactic match -1 " << mt.pretty() << std::endl; + if(mt.id()==ID_symbol || + (mt.id()==ID_not && mt.op0().id()==ID_symbol)) + { + for(unsigned i=0; iN + exprt val; + normalize_meetirrd(v, val); + + assert(val.id() == ID_lt || val.id() == ID_gt || val.id() == ID_ge || val.id() == ID_le); + const exprt &lhsv=to_binary_relation_expr(val).lhs(); + + exprt lhsv_op, lhs_op; + // Check for I/P: (-x<=10) + // Check for val + if(lhsv.id()==ID_unary_minus && + lhsv.op0().id()==ID_typecast) + { + lhsv_op = lhsv.op0().op0(); + } + else + { + lhsv_op = lhsv; + } + + std::cout << "Syntactic match check of meet irreducible " << from_expr(m) << "with final value symbol " + << from_expr(lhsv_op) << "derived from value component" << from_expr(val) << std::endl; + + if(lhsv_op == mt) + { +#ifdef DEBUG + std::cout << "meet irreducible " << from_expr(m) << "matches with value " + << from_expr(v) << std::endl; +#endif + return true; + } + } + } + return false; +} + +/*******************************************************************\ + + Function: acdl_domaint::initialize_var_bounds() + + Inputs: + + Purpose: Initialize Varible bounds with MinInt and MaxInt + +\*******************************************************************/ + +void acdl_domaint::initialize_var_bound(const exprt& expr) +{ + constant_exprt l, u; + mp_integer lower, upper; + std::cout << "Computing the initialization value of numerical variables " << + expr.pretty() << std::endl; + u=tpolyhedra_domaint::get_max_value(expr); + l=tpolyhedra_domaint::get_min_value(expr); + + to_integer(to_constant_expr(u), upper); + to_integer(to_constant_expr(l), lower); + + bound_var_name.push_back(expr); + bound_var_val.push_back(std::make_pair(lower, upper)); +} + +/*******************************************************************\ + + Function: acdl_domaint::update_var_bound() + + Inputs: + 1. x<=3, 0<=x && x<=3 + 2. x<=5, 3<=x && x<=3 + 3. x<=2, 0<=x && x<=3 (updated upper bound=2) + 4. x<=3, 0<=x && x<=2 (don't update, upper bound=2) + 5. x>=7, x>=5 && x<=10 (lower bound = 7) + 6. x>=3, x>=5 && x<=10 (don't update, lower bound = 5) + + Purpose: Update Varible bounds (lower, upper) for Intervals. Only called from numerical inference + +\*******************************************************************/ + +bool acdl_domaint::update_var_bound(const exprt& expr, const valuet& _value) +{ +#ifdef DEBUG + std::cout << "[ACDL-DOMAIN] Update var bound(" + << from_expr(SSA.ns, "", expr) << "): " << std::endl; +#endif +#if 0 + // This case is not needed since it + // is called only from numerical inference + if(expr.type().id()==ID_bool) + { + if(expr.id==ID_not) { + mp_integer l=0; + mp_integer u=0; + } + else { + mp_integer l=1; + mp_integer u=1; + } + val_pair.first=l; + val_pair.second=u; +#ifdef DEBUG + std::cout << "The val pair for " << from_expr(SSA.ns, "", expr) << "is" << "lower" << l << "upper" << u << std::endl; +#endif + return val_pair; + } +#endif + + /*if(!(expr.type().id()==ID_signedbv || + expr.type().id()==ID_unsignedbv || + expr.type().id()==ID_floatbv)) + { + std::cout << "WARNING: do not know how to split " + << from_expr(SSA.ns, "", expr) + << " of type " << from_type(SSA.ns, "", expr.type()) + << std::endl; + return; + } + */ + // process the meet irreducible + exprt c; + mp_integer lb, ub; + bool ub_is_assigned=false; + bool lb_is_assigned=false; + mp_integer v1, v2; + mp_integer ng, cng; + mp_integer ngu, cngu; + + exprt lhs_c; + if(expr.id()==ID_not) { + c = expr.op0(); +#ifdef DEBUG + std::cout << "Bound calculation for " << from_expr(c) << "derived from " << + from_expr(expr) << std::endl; + std::cout << "Bound calculation for " << c.pretty() << std::endl; +#endif + // Handle the singleton case: example : guard#0 + if(c.id()!=ID_le && c.id()!=ID_ge) + { + // don't know how to handle this + std::cout << "Dont know how to handle" << c.pretty() << std::endl; + return false; + } + const exprt &lhs=to_binary_relation_expr(c).lhs(); + const exprt &rhs=to_binary_relation_expr(c).rhs(); + // I/P: !(-x<=10) O/P: -x>10 --> x<(-10) --> ub=-11 + if(c.id()==ID_le && c.op0().id()==ID_unary_minus && + c.op0().op0().id()==ID_typecast) + { + lhs_c=c.op0().op0().op0(); + constant_exprt cexpr=to_constant_expr(c.op0().op0().op1()); + to_integer(cexpr, ng); + cng=-ng-1; + ub=cng; + ub_is_assigned=true; + } + // I/P: !(-x >= 10) O/P: -x<10 --> x>-10, lb=-9 + if(c.id()==ID_ge && c.op0().id()==ID_unary_minus && + c.op0().op0().id()==ID_typecast) + { + lhs_c=c.op0().op0().op0(); + const exprt &rhs=to_binary_relation_expr(c).rhs(); + constant_exprt cexpru=to_constant_expr(rhs); + to_integer(cexpru, ngu); + cngu=-ngu+1; + lb=cngu; + lb_is_assigned=true; + } + else if(c.id()==ID_le) { + lhs_c=lhs; + // !(ID_le) --> ID_gt + exprt t_exp=binary_relation_exprt(lhs, ID_gt, rhs); + constant_exprt cexpr=to_constant_expr(to_binary_relation_expr(t_exp).rhs()); + to_integer(cexpr, v1); + v2=v1+1; + lb=v2; + lb_is_assigned=true; + } + // !(ID_ge) --> ID_lt + else if(c.id()==ID_ge) { + lhs_c=lhs; + exprt t_exp=binary_relation_exprt(lhs, ID_lt, rhs); + constant_exprt cexpr=to_constant_expr(to_binary_relation_expr(t_exp).rhs()); + to_integer(cexpr, v1); + v2=v1-1; + ub=v2; + ub_is_assigned=true; + } + else if(c.id()==ID_lt || c.id()==ID_gt) { + // this must not happen because + // the expressions are now generated as<=or >= + assert(false); + } + else if(c.id()==ID_unary_minus && + c.op0().id()==ID_typecast) + { + // I/P: !(-x<=10) O/P: -x>10 --> x<(-10) --> ub=-11 + lhs_c=c.op0().op0(); + if(c.id()==ID_le) { + const exprt &rhs=to_binary_relation_expr(c).rhs(); + constant_exprt cexpr=to_constant_expr(rhs); + to_integer(cexpr, ng); + cng=-ng-1; + ub=cng; + ub_is_assigned=true; + } + // I/P: !(-x >= 10) O/P: -x<10 --> x>-10, lb=-9 + if(c.id()==ID_ge) { + const exprt &rhs=to_binary_relation_expr(c).rhs(); + constant_exprt cexpru=to_constant_expr(rhs); + to_integer(cexpru, ngu); + cngu=-ngu+1; + lb=cngu; + lb_is_assigned=true; + } + } + else + { + // What else can be the type ? + // assert(false); + } + } // end ID_not + else { + c = expr; + const exprt &lhs=to_binary_relation_expr(c).lhs(); + if(c.id()==ID_le) + { + lhs_c=lhs; + to_integer(to_constant_expr(to_binary_relation_expr(c).rhs()), ub); + ub_is_assigned=true; + } + else if(c.id()==ID_ge) + { + lhs_c=lhs; + to_integer(to_constant_expr(to_binary_relation_expr(c).rhs()), lb); + lb_is_assigned=true; + } + else if(c.id()==ID_unary_minus && + c.op0().id()==ID_typecast) + { + lhs_c=c.op0().op0(); + // I/P: (-x<=10) O/P: x>=(-10) --> lb=-10 + if(c.id()==ID_le) { + const exprt &rhs=to_binary_relation_expr(c).rhs(); + constant_exprt cexpr=to_constant_expr(rhs); + to_integer(cexpr, ng); + cng=-ng; + lb=cng; + lb_is_assigned=true; + } + // I/P: (-x >= 10) O/P: x<=-10 --> ub=-10 + if(c.id()==ID_ge) { + const exprt &rhs=to_binary_relation_expr(c).rhs(); + constant_exprt cexpru=to_constant_expr(rhs); + to_integer(cexpru, ngu); + cngu=-ngu; + ub=cngu; + ub_is_assigned=true; + } + } + else { + // What else can be the type ? + // assert(false); + } + } + + + // we do not store id_c_bool in bound_var_val + // so, just check with is_subsumed_syntactic + if(lhs_c.type().id() == ID_c_bool) { + std::cout << "Not computing bound for ID_c_bool variable " << lhs_c.pretty() << std::endl; + c_bool_deductions.push_back(expr); + if(!is_subsumed_syntactic(expr, _value)) + return true; + } + + // we do not store id_array in bound_var_val + // so, just check with is_subsumed_syntactic + if(lhs_c.type().id() == ID_array) { + std::cout << "Not computing bound for ID_array variable " << lhs_c.pretty() << std::endl; + array_deductions.push_back(expr); + if(!is_subsumed_syntactic(expr, _value)) + return true; + } + mp_integer vall,valu; + // get the original bounds + mp_integer orgl,orgu; + //orgl=var_bound.find(lhs_c)->second.first; + //orgu=var_bound.find(lhs_c)->second.second; + bool found=false; + for(int i=0;i=7, x>=5 && x<=10 (lower bound = 7) + // 6. x>=3, x>=5 && x<=10 (don't update, lower bound = 5) + // both bounds can not be updated at the same time + // since we are computing one meet irreducible at a time + assert(!(lb_is_assigned && ub_is_assigned)); + + if(ub_is_assigned) { + if(ub>orgu) { // x<=3 -> x<=2 + valu = orgu; + ubupdate = false; + } + else if(ub) x<=3 + ubupdate = true; + } + else if(ub==orgu) { + valu = orgu; + ubupdate = false; + } + } + else if(lb_is_assigned) { + if(lb>orgl) { + vall = lb; + lbupdate = true; + } + else if(lb10 && x<20) + + Outputs: new_val:= (y>10 & y<20) + + Purpose: + +\******************************************************************/ +/*bool acdl_domaint::equal_copy(const statementt &statement, + const exprt& expr + const valuet &old_val, + valuet &new_val) const +{ + +}*/ + +/*******************************************************************\ + + Function: acdl_domaint::compute_value(val) + + Inputs: + + Outputs: + + Purpose: + +\******************************************************************/ +void acdl_domaint::compute_normalized_val(valuet &value) +{ + valuet val; + if(value.empty()) + return; + + exprt m; + mp_integer l, u; + constant_exprt uexp, lexp; + for(unsigned i=0; i10 --> x<(-10) --> ub=-11 + if(c.id()==ID_le && c.op0().id()==ID_unary_minus && + c.op0().op0().id()==ID_typecast) + { + lhs_c=c.op0().op0().op0(); + } + // I/P: !(-x >= 10) O/P: -x<10 --> x>-10, lb=-9 + if(c.id()==ID_ge && c.op0().id()==ID_unary_minus && + c.op0().op0().id()==ID_typecast) + { + lhs_c=c.op0().op0().op0(); + } + else if(c.id()==ID_le) { + lhs_c=lhs; + } + // !(ID_ge) --> ID_lt + else if(c.id()==ID_ge) { + lhs_c=lhs; + } + else if(c.id()==ID_lt || c.id()==ID_gt) { + // this must not happen because + // the expressions are now generated as<=or >= + assert(false); + } + else if(c.id()==ID_unary_minus && + c.op0().id()==ID_typecast) + { + // I/P: !(-x<=10) O/P: -x>10 --> x<(-10) --> ub=-11 + lhs_c=c.op0().op0(); + } + else + { + // What else can be the type ? + // assert(false); + } + } // end ID_not + else { + c = expr; + const exprt &lhs=to_binary_relation_expr(c).lhs(); + if(c.id()==ID_le) + { + lhs_c=lhs; + } + else if(c.id()==ID_ge) + { + lhs_c=lhs; + } + else if(c.id()==ID_unary_minus && + c.op0().id()==ID_typecast) + { + lhs_c=c.op0().op0(); + } + else { + // What else can be the type ? + // assert(false); + } + } + return lhs_c; +} diff --git a/src/acdl/acdl_domain.h b/src/acdl/acdl_domain.h index de72c5e2d..ef7ee7356 100644 --- a/src/acdl/acdl_domain.h +++ b/src/acdl/acdl_domain.h @@ -21,6 +21,19 @@ class acdl_domaint : public messaget typedef std::vector deductionst; typedef exprt statementt; typedef std::set varst; + // Only for Interval domain + //typedef std::map> var_boundt; + //var_boundt var_bound; + typedef std::vector bound_var_namet; + bound_var_namet bound_var_name; + typedef std::vector> bound_var_valt; + bound_var_valt bound_var_val; + typedef std::vector boolean_deductionst; + boolean_deductionst boolean_deductions; + typedef std::vector c_bool_deductionst; + c_bool_deductionst c_bool_deductions; + typedef std::vector array_deductionst; + array_deductionst array_deductions; typedef enum clause_statet { CONFLICT=0, UNKNOWN=1, SATISFIED=2, UNIT=3} clause_state; explicit acdl_domaint(optionst &_options, @@ -109,6 +122,8 @@ class acdl_domaint : public messaget bool semantic_subsumption(const meet_irreduciblet &m) const; void normalize_val_syntactic(valuet &value); void preprocess_val(valuet& val); + bool check_val_syntactic(const meet_irreduciblet &m, + const valuet &value) const; // print value inline std::ostream &output( @@ -124,6 +139,11 @@ class acdl_domaint : public messaget return out; } + void initialize_var_bound(const exprt& expr); + bool update_var_bound(const exprt& expr, const valuet& value); + void compute_normalized_val(valuet &val); + exprt get_expr_symbol(exprt& expr); + protected: optionst &options; local_SSAt &SSA; diff --git a/src/acdl/acdl_solver.cpp b/src/acdl/acdl_solver.cpp index d5df32606..6a9ebc938 100644 --- a/src/acdl/acdl_solver.cpp +++ b/src/acdl/acdl_solver.cpp @@ -17,8 +17,12 @@ Author: Rajdeep Mukherjee, Peter Schrammel #include #define DEBUG -// #define PER_STATEMENT_LIVE_VAR +//#define PER_STATEMENT_LIVE_VAR #define LIVE_VAR_OLD_APPROACH +//#define INTERVALS +//#define UNDERAPPROX_LIVE_VAR +#define GAMMA_COMPLETE_CHECK 0 +#define BOX 1 /******************************************************************* @@ -141,7 +145,7 @@ bool acdl_solvert::bcp(const local_SSAt &SSA, unsigned idx) // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(v); + // domain.preprocess_val(v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) @@ -203,10 +207,190 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons { //unsigned init_size=conflict_graph.prop_trail.size(); acdl_domaint::valuet final_val; - while (!worklist.empty()) + + std::vector arith_statement; + std::vector equal_statement; + // Non fixed-point strategy for Propagation + unsigned wl_size=worklist.size(); + std::cout << "Total statements in worklist are " << wl_size << std::endl; + + unsigned prop_iteration=0; + + // must clean the deductions in these containers + // only when there is a conflict +#ifdef BOX + // domain.boolean_deductions.clear(); + // domain.c_bool_deductions.clear(); +#endif + + while (!worklist.empty()) // && wl_size>0) { const acdl_domaint::statementt statement=worklist.pop(); + std::cout << "Remaining number of statements in worklist is " << worklist.size() << std::endl; + + // compute update of abstract value + acdl_domaint::valuet v; + conflict_graph.to_value(v); + +#ifdef DEBUG + std::cout << "Computing old abstract value of implication graph: " << std::endl; + for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) + std::cout << from_expr(SSA.ns, "", *it) << std::endl; +#endif + + // preprocess abstract value + // transform constraints like (x==N) to (x<=N) and (x>=N) + // domain.preprocess_val(v); +#ifdef DEBUG + std::cout << "Computing preprocessed abstract value of implication graph: " << std::endl; + for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) + std::cout << from_expr(SSA.ns, "", *it) << std::endl; +#endif + + // Do we need to normalize value here since + // this will remove all old decisions that are + // still stored in the implication graph. These + // old decisions can still contribute towards the + // future deductions called in domain operator() below +#ifdef INTERVALS +#ifdef BOX + domain.compute_normalized_val(v); +#else + domain.normalize_val_syntactic(v); +#endif +#endif + // Complex arithmetic statements are processed + // only when both their operands are avaluated + // Example, z=x*y, process this only when both + // x and y are available + acdl_domaint::varst arith_vars; + if(statement.id() == ID_equal) + { + exprt expr_rhs=to_equal_expr(statement).rhs(); + // for arithmetic statements like x=y*z + if(expr_rhs.id() == ID_mult || expr_rhs.id() == ID_div) + { + // check if the operands of the multiplier or divider operator + // are already evaluated. If so, they will appear in the abstract value + bool st1 = domain.check_val_syntactic(expr_rhs.op0(), v); + bool st2 = domain.check_val_syntactic(expr_rhs.op1(), v); +#ifdef DEBUG + std::cout << "The syntactic expr-val check for expression " << from_expr(expr_rhs.op0()) << "against value " << from_expr(conjunction(v)) + << "is " << st1 << std::endl; + std::cout << "The syntactic expr-val check for expression " << from_expr(expr_rhs.op1()) << "against value " << from_expr(conjunction(v)) + << "is " << st2 << std::endl; +#endif + if(st1 && st2) + { + // evaluate the statement since both operands + // are available + arith_statement.erase(std::remove(arith_statement.begin(), arith_statement.end(), + statement), arith_statement.end()); + // erase the lhs vars from arith_vars + acdl_domaint::varst avars; + exprt lhs=to_equal_expr(statement).lhs(); + find_symbols(lhs, avars); + for(acdl_domaint::varst::const_iterator it=avars.begin();it!=avars.end();++it) + { + if(arith_vars.find(*it) != arith_vars.end()) + arith_vars.erase(it); + } + std::cout << "The arithmetic statement poped for evaluation is " + << from_expr(SSA.ns, "", statement) << std::endl; + } + else + { + std::vector::iterator it; + it = find(arith_statement.begin(), arith_statement.end(), statement); + if(it == arith_statement.end()) + { + acdl_domaint::varst avars; + exprt lhs=to_equal_expr(statement).lhs(); + find_symbols(lhs, avars); + arith_vars.insert(avars.begin(), avars.end()); + arith_statement.push_back(statement); + std::cout << "The statement pushed for later evaluation is " + << from_expr(SSA.ns, "", statement) << std::endl; + } + continue; + } + } + // for statements like x=y, if neither x nor y is + // evaluated (value present in abstract value), then + // there is no point to process this statement now + // THIS OPTIMIZATION is specific to INTERVAL domain + // Turn OFF if using Octagon domain +#ifdef INTERVALS + std::cout << "Checking the equality statement " << from_expr(SSA.ns, "", statement) << + std::endl; + std::cout << statement.pretty() << std::endl; + exprt elhs=to_equal_expr(statement).lhs(); + exprt lhs, rhs; + if(expr_rhs.id() != ID_constant) { + if(elhs.id() == ID_symbol) + { + lhs = elhs; + } + else if(elhs.op0().id()==ID_typecast) + { + lhs = elhs.op0().op0(); + } + if(expr_rhs.id() == ID_symbol) + { + rhs = expr_rhs; + } + else if(expr_rhs.op0().id()==ID_typecast) + { + rhs = expr_rhs.op0().op0(); + } + if(lhs.id() == ID_symbol && rhs.id() == ID_symbol) + { + // check if the operands are already evaluated. + // If so, they will appear in the abstract value + bool st1 = domain.check_val_syntactic(rhs, v); + bool st2 = domain.check_val_syntactic(lhs, v); +#ifdef DEBUG + std::cout << "The syntactic expr-val check for expression " << from_expr(lhs) << "against value " << from_expr(conjunction(v)) + << "is " << st1 << std::endl; + std::cout << "The syntactic expr-val check for expression " << from_expr(rhs) << "against value " << from_expr(conjunction(v)) + << "is " << st2 << std::endl; +#endif + if(!(st1 || st2)) + { + std::vector::iterator it; + it = find(equal_statement.begin(), equal_statement.end(), statement); + if(it == equal_statement.end()) + { + equal_statement.push_back(statement); + std::cout << "The equality statement pushed for later evaluation is " + << from_expr(SSA.ns, "", statement) << std::endl; + } + continue; + } + else { + // evaluate the statement since at least one operand is available + equal_statement.erase(std::remove(equal_statement.begin(), equal_statement.end(), + statement), equal_statement.end()); + std::cout << "The equality statement poped for evaluation is " + << from_expr(SSA.ns, "", statement) << std::endl; + // if atleast one of the operands is evaluated, + // then syntactically copy the value in other without SAT solver + /*if(!(st1 && st2)) + { + if(st1) + domain.equal_copy(equal_statement, 2, rhs, value); + else if(st2) + domain.equal_copy(equal_statement, 1, lhs, value); + // add the deduction to conflict graph + }*/ + } + } + } +#endif + } // end of optimization for equality statements + //wl_size = wl_size-1; + prop_iteration=prop_iteration+1; #if 0 // MUST NOT DO THE OPTIMIZATION BELOW SINCE THIS CAN // BLOCK SOME RELEVANT DEDUCTIONS. For example, if domain=octagon @@ -219,7 +403,32 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons if (ita != assume_statements.end()) continue; #endif - + +#ifdef UNDERAPPROX_LIVE_VAR + // Identify lhs_vars that belong to statements like z=x*x; + // Computing templates bounds on z at every iteration of propagation is very expensive + // Compute the bound on z only when x is fixed. Once the bound of z is + // computed, do not generate template any further. + acdl_domaint::varst uvars; + if(statement.id()==ID_equal) { + // find lhs vars + exprt expr_lhs=to_equal_expr(statement).lhs(); + find_symbols(expr_lhs, uvars); + } + else { + find_symbols(statement, uvars); + } + // remove all arith_vars from uvars + // since if z=x*x is not evaluated due to absence of values of x, + // then there is no point on generating templates on z for subsequent deductions + for(it=arith_vars.begin();it!=arith_vars.end();++it) + { + if(uvars.find(*it) != uvars.end()) + uvars.erase(it); + } +#endif + + acdl_domaint::varst lvar; #ifdef PER_STATEMENT_LIVE_VAR lvar=worklist.pop_from_map(statement); @@ -230,6 +439,11 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons << std::endl; #endif +#ifdef DEBUG + std::cout << "Old: "; + domain.output(std::cout, v) << std::endl; +#endif + #ifdef DEBUG #ifdef PER_STATEMENT_LIVE_VAR std::cout << "Live variables for " << from_expr(statement) << " are: "; @@ -240,38 +454,9 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons #endif #endif - // compute update of abstract value - acdl_domaint::valuet v; acdl_domaint::valuet v1; acdl_domaint::deductionst deductions; - conflict_graph.to_value(v); - // Do we need to normalize value here since - // this will remove all old decisions that are - // still stored in the implication graph. These - // old decisions can still contribute towards the - // future deductions called in domain operator() below - // domain.normalize_val_syntactic(v); - - // preprocess abstract value - // transform constraints like (x==N) to (x<=N) and (x>=N) - domain.preprocess_val(v); -#ifdef DEBUG - std::cout << "Computing preprocessed abstract value of implication graph: " << std::endl; - for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) - std::cout << from_expr(SSA.ns, "", *it) << std::endl; -#endif - -#ifdef DEBUG - std::cout << "Computing old abstract value of implication graph: " << std::endl; - for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) - std::cout << from_expr(SSA.ns, "", *it) << std::endl; -#endif - -#ifdef DEBUG - std::cout << "Old: "; - domain.output(std::cout, v) << std::endl; -#endif // select vars for projection @@ -281,10 +466,18 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons #ifdef LIVE_VAR_OLD_APPROACH find_symbols(statement, project_vars); projected_live_vars=worklist.check_var_liveness(project_vars); + // remove all arith_vars from project_live_vars + // since if z=x*x is not evaluated due to absence of values of x, + // then there is no point on generating templates on z for subsequent deductions + for(acdl_domaint::varst::const_iterator it=arith_vars.begin();it!=arith_vars.end();++it) + { + if(projected_live_vars.find(*it) != projected_live_vars.end()) + projected_live_vars.erase(it); + } #endif - // do path-sensitive analysis - // for efficient gamma-complete check +#ifdef GAMMA_COMPLETE_CHECK + // gamma-complete check find_symbols(statement, project_vars); acdl_domaint::varst gvar; if(statement.id()==ID_equal) { @@ -370,10 +563,20 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons } #endif #endif +#endif + + clock_t total_time = 0.0; + const clock_t begin_time = clock(); +#ifdef UNDERAPPROX_LIVE_VAR + domain(statement, uvars, v, new_v, deductions); +#endif #ifdef LIVE_VAR_OLD_APPROACH domain(statement, projected_live_vars, v, new_v, deductions); #endif + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Statement: " << from_expr(SSA.ns, "", statement) << + " Propagation Time: " << total_time << " seconds" << std::endl; // [QUERY] find intersection of project_vars and lvar // for per-statement based live variable approach @@ -413,7 +616,7 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(new_v); + // domain.preprocess_val(new_v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=new_v.begin();it!=new_v.end(); ++it) @@ -454,6 +657,156 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons analyzes_conflict.last_proof=analyzes_conflict.ABSINT; return property_checkert::PASS; // potential UNSAT (modulo decisions) } + } // end of while loop + + // check whether we can infer something now + // for the arithmetic statements + if(arith_statement.size() != 0) { + for(std::vector::iterator it = arith_statement.begin(); + it != arith_statement.end();++it) + { + exprt expr_rhs=to_equal_expr(*it).rhs(); + exprt expr_lhs=to_equal_expr(*it).lhs(); + if(expr_rhs.id() == ID_mult || expr_rhs.id() == ID_div) + { + acdl_domaint::valuet v; + conflict_graph.to_value(v); + // check if the operands of the multiplier or divider operator + // are already evaluated. If so, they will appear in the abstract value + bool st1 = domain.check_val_syntactic(expr_rhs.op0(), v); + bool st2 = domain.check_val_syntactic(expr_rhs.op1(), v); +#ifdef DEBUG + std::cout << "The syntactic expr-val check for expression " << from_expr(expr_rhs.op0()) << "against value " << from_expr(conjunction(v)) + << "is " << st1 << std::endl; + std::cout << "The syntactic expr-val check for expression " << from_expr(expr_rhs.op1()) << "against value " << from_expr(conjunction(v)) + << "is " << st2 << std::endl; +#endif + if(st1 && st2) + { + // evaluate the statement since both operands are available + std::cout << "Arithmetic statement evaluated after the propagation loop " << + from_expr(SSA.ns, "", *it) << std::endl; + const acdl_domaint::statementt statement=*it; + acdl_domaint::varst vars; + acdl_domaint::valuet new_v; + acdl_domaint::deductionst deductions; + find_symbols(expr_lhs, vars); + clock_t total_time = 0.0; + const clock_t begin_time = clock(); + domain(statement, vars, v, new_v, deductions); + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Statement: " << from_expr(SSA.ns, "", statement) << + " Propagation Time: " << total_time << " seconds" << std::endl; + // update implication graph + conflict_graph.add_deductions(SSA, deductions, statement); + propagations++; + conflict_graph.to_value(new_v); +#ifdef DEBUG + std::cout << "New: "; + domain.output(std::cout, new_v) << std::endl; +#endif + // domain.preprocess_val(new_v); + final_val=new_v; + // Cool! We got UNSAT + domain.normalize(new_v); + if(domain.is_bottom(new_v)) + { + // Abstract Interpretation proof + analyzes_conflict.last_proof=analyzes_conflict.ABSINT; + return property_checkert::PASS; // potential UNSAT (modulo decisions) + } + } + else { + std::cout << "Arithmetic statement not evaluated in this propagation phase is " << + from_expr(SSA.ns, "", *it) << std::endl; + } + } + } + } + //assert(arith_statement.size() == 0); + // check if we can process equality statements +#ifdef INTERVALS + if(equal_statement.size() != 0) { + for(std::vector::iterator it = equal_statement.begin(); + it != equal_statement.end();++it) + { + exprt expr_rhs=to_equal_expr(*it).rhs(); + exprt expr_lhs=to_equal_expr(*it).lhs(); + exprt lhs, rhs; + if(expr_lhs.id() == ID_symbol) + { + lhs = expr_lhs; + } + else if(expr_lhs.op0().id()==ID_typecast) + { + lhs = expr_lhs.op0().op0(); + } + if(expr_rhs.id() == ID_symbol) + { + rhs = expr_rhs; + } + else if(expr_rhs.op0().id()==ID_typecast) + { + rhs = expr_rhs.op0().op0(); + } + if(lhs.id() == ID_symbol && rhs.id() == ID_symbol) + { + acdl_domaint::valuet v; + conflict_graph.to_value(v); + // check if the operands of the multiplier or divider operator + // are already evaluated. If so, they will appear in the abstract value + bool st1 = domain.check_val_syntactic(lhs, v); + bool st2 = domain.check_val_syntactic(rhs, v); +#ifdef DEBUG + std::cout << "The syntactic expr-val check for expression " << from_expr(lhs) << "against value " << from_expr(conjunction(v)) + << "is " << st1 << std::endl; + std::cout << "The syntactic expr-val check for expression " << from_expr(rhs) << "against value " << from_expr(conjunction(v)) + << "is " << st2 << std::endl; +#endif + if(st1 || st2) + { + // evaluate the statement since both operands are available + std::cout << "Equality statement evaluated after the propagation loop " << + from_expr(SSA.ns, "", *it) << std::endl; + + acdl_domaint::valuet new_v; + clock_t total_time = 0.0; + const clock_t begin_time = clock(); + make_deduction(SSA, *it, v, new_v); + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Statement: " << from_expr(SSA.ns, "", *it) << + " Propagation Time: " << total_time << " seconds" << std::endl; + // domain.preprocess_val(new_v); + final_val=new_v; + // Cool! We got UNSAT + domain.normalize(new_v); + if(domain.is_bottom(new_v)) + { + // Abstract Interpretation proof + analyzes_conflict.last_proof=analyzes_conflict.ABSINT; + return property_checkert::PASS; // potential UNSAT (modulo decisions) + } + } + else + { + std::cout << "Equality statement not evaluated in this propagation phase is " << + from_expr(SSA.ns, "", *it) << std::endl; + } + } + } + } +#endif + std::cout << "Propagation Iteration is" << prop_iteration << std::endl; + // Empty the worklist for + // non fixed-point strategy + if(wl_size <= 0) { + while(!worklist.empty()) + worklist.pop(); + // empty the live variables because the worklist + // items are no more relevent, hence the live variables + // are no more relevant + worklist.live_variables.erase + (worklist.live_variables.begin(), worklist.live_variables.end()); } // [TODO] check if new_v is EMPTY, @@ -493,6 +846,8 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons analyzes_conflict.cancel_once(SSA, conflict_graph); } #endif + +#if 0 // check for closed abstract value std::cout<< "***** CLOSURE Check ******" << std::endl; bool status = is_closed(SSA, final_val); @@ -502,6 +857,7 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons std::cout << "The abstract value is not closed" << std::endl; assert(0); } +#endif #ifdef DEBUG std::cout << "Propagation finished with UNKNOWN" << std::endl; @@ -509,6 +865,41 @@ property_checkert::resultt acdl_solvert::propagation(const local_SSAt &SSA, cons return property_checkert::UNKNOWN; } +/******************************************************************* + + Function: acdl_solvert::make_deduction() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +void acdl_solvert::make_deduction(const local_SSAt &SSA, + const acdl_domaint::statementt &statement, + const acdl_domaint::valuet &old_value, + acdl_domaint::valuet &new_value) +{ + acdl_domaint::varst vars; + acdl_domaint::deductionst deductions; + find_symbols(statement, vars); + clock_t total_time = 0.0; + const clock_t begin_time = clock(); + domain(statement, vars, old_value, new_value, deductions); + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Statement: " << from_expr(SSA.ns, "", statement) << + " Propagation Time: " << total_time << " seconds" << std::endl; + // update implication graph + conflict_graph.add_deductions(SSA, deductions, statement); + propagations++; + conflict_graph.to_value(new_value); +#ifdef DEBUG + std::cout << "New: "; + domain.output(std::cout, new_value) << std::endl; +#endif + // domain.preprocess_val(new_value); +} /******************************************************************* @@ -607,7 +998,7 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(v); + // domain.preprocess_val(v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) @@ -620,7 +1011,7 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(old_v); + // domain.preprocess_val(old_v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=old_v.begin();it!=old_v.end(); ++it) @@ -645,7 +1036,12 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) // Normalizing here is absolute must // Otherwise, unsafe cases does not terminate +#ifdef BOX + domain.compute_normalized_val(v); +#else domain.normalize_val_syntactic(v); +#endif + acdl_domaint::meet_irreduciblet dec_expr=decision_heuristics(SSA, v); if(dec_expr==false_exprt()) return false; @@ -688,6 +1084,13 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) // update conflict graph conflict_graph.add_decision(dec_expr); + +#ifdef BOX + // update the numerical variable bound + // corresponding to the new decision + bool update = domain.update_var_bound(dec_expr, v); +#endif + // save the last decision index last_decision_index=conflict_graph.prop_trail.size(); @@ -702,7 +1105,7 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(new_value); + // domain.preprocess_val(new_value); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=new_value.begin();it!=new_value.end(); ++it) @@ -728,7 +1131,11 @@ bool acdl_solvert::decide (const local_SSAt &SSA, const exprt& assertion) #endif // normalize v +#ifdef BOX + domain.compute_normalized_val(v); +#else domain.normalize_val_syntactic(v); +#endif #ifdef DEBUG std::cout << "New: "; @@ -779,7 +1186,7 @@ bool acdl_solvert::analyze_conflict(const local_SSAt &SSA, const exprt& assertio // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(v); + // domain.preprocess_val(v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) @@ -787,7 +1194,11 @@ bool acdl_solvert::analyze_conflict(const local_SSAt &SSA, const exprt& assertio #endif // call normalize or normalize_val_syntactic ? +#ifdef BOX + domain.compute_normalized_val(v); +#else domain.normalize_val_syntactic(v); +#endif exprt dec_expr=conflict_graph.prop_trail.back(); domain.meet(dec_expr, v); #ifdef DEBUG @@ -913,14 +1324,25 @@ void acdl_solvert::initialize_decision_variables(acdl_domaint::valuet &value) \*******************************************************************/ void acdl_solvert::print_solver_statistics() { +#ifdef BOX + std::cout << "**************************" << std::endl; + std::cout << "Printing VARIABLE BOUNDS " << std::endl; + std::cout << "**************************" << std::endl; + for(int i=0;i::iterator it= worklist.statements.begin(); it!=worklist.statements.end(); it++) std::cout << "Statement: " << from_expr(SSA.ns, "", *it) << std::endl; -// #endif +} + +/******************************************************************* + Function: acdl_solvert::check_using_solver() + + Inputs: + + Outputs: + + Purpose: Resort to SAT solver to solve the SSA equations with + the facts derived by ACDLP so far +********************************************************************/ +property_checkert::resultt acdl_solvert::check_using_solver( + const exprt &ssa_conjunction) +{ + // solve the conjunction of SSA with current abstract value + acdl_domaint::valuet v; + conflict_graph.to_value(v); + bool state = domain.gamma_complete_deduction(ssa_conjunction, v); + if(state==true) { + //print_solver_statistics(); + //std::cout << "Solved by SAT solver" << std::endl; + return property_checkert::FAIL; + } + else { + //print_solver_statistics(); + //std::cout << "Solved by SAT solver" << std::endl; + return property_checkert::PASS; + } } /******************************************************************* @@ -1184,7 +1634,22 @@ property_checkert::resultt acdl_solvert::operator()( // call initialize live variables worklist.initialize_live_variables(); + +#ifdef BOX + for(std::set::iterator it=all_vars.begin();it!=all_vars.end(); it++) + { + // initialize the Intervals for numerical variables + if(it->type().id() != ID_bool && it->type().id()!=ID_c_bool && it->type().id() !=ID_array) + { + domain.initialize_var_bound(*it); + } + else + std::cout << "Not initializing bound for variable " << it->pretty() << std::endl; + } +#endif + std::set decision_variable; + bool unknown_result = false; // initialize the decision variables // Note that the decision variable contains @@ -1223,10 +1688,8 @@ property_checkert::resultt acdl_solvert::operator()( else { #endif decision_heuristics.get_dec_variables(*it); - //} } } - decision_heuristics.initialize_var_set(read_only_vars, assume_vars, cond_vars); // [TODO] order decision variables @@ -1242,6 +1705,18 @@ property_checkert::resultt acdl_solvert::operator()( std::cout << "The additional constraint for the loop is: " << from_expr(SSA.ns, "", additional_constraint) << std::endl; #endif +#ifdef BOX + std::cout << "************************************" << std::endl; + std::cout << "Printing INITIALIZED VARIABLE BOUNDS " << std::endl; + std::cout << "*************************************" << std::endl; + for(int i=0;i=n) - domain.preprocess_val(v); + // domain.preprocess_val(v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) std::cout << from_expr(ssa.ns, "", *it) << std::endl; #endif +#ifdef BOX + domain.compute_normalized_val(v); +#else domain.normalize_val_syntactic(v); +#endif // check if abstract value v of the // implication graph is top for the first time // because ACDL starts with TOP @@ -1295,6 +1774,10 @@ property_checkert::resultt acdl_solvert::operator()( std::vector ded; ded.push_back(lhs); conflict_graph.add_deductions(SSA, ded, stmt); + // push into boolean deductions vector +//#ifdef BOX +// domain.boolean_deductions.push_back(lhs); +//#endif std::cout << "Pushing deduction from assumption into trail: " << from_expr(lhs) << std::endl; ded.clear(); /*ded.push_back(assume_st); @@ -1324,7 +1807,12 @@ property_checkert::resultt acdl_solvert::operator()( std::cout << "********************************" << std::endl; std::cout << " DEDUCTION PHASE " << std::endl; std::cout << "********************************" << std::endl; + clock_t total_time = 0.0; + const clock_t begin_time = clock(); result=propagate(SSA, assertion); + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Propagation Time in Iteration 0: " << total_time << "seconds" << std::endl; + std::cout << "The result after first propagation phase is " << result << std::endl; std::cout << "****************************************************" << std::endl; std::cout << " IMPLICATION GRAPH AFTER DEDUCTION PHASE" << std::endl; @@ -1340,6 +1828,8 @@ property_checkert::resultt acdl_solvert::operator()( print_solver_statistics(); return property_checkert::PASS; } + +#ifdef GAMMA_COMPLETE_CHECK // if result=UNKNOWN or FAIL, // then check for completeness else { @@ -1349,14 +1839,18 @@ property_checkert::resultt acdl_solvert::operator()( // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(res_val); + // domain.preprocess_val(res_val); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=res_val.begin();it!=res_val.end(); ++it) std::cout << from_expr(ssa.ns, "", *it) << std::endl; #endif +#ifdef BOX + domain.compute_normalized_val(res_val); +#else domain.normalize_val_syntactic(res_val); +#endif if(domain.is_complete(res_val, all_vars, non_gamma_complete_var, ssa_conjunction, gamma_decvar, read_only_symbols)) { complete=true; @@ -1375,6 +1869,7 @@ property_checkert::resultt acdl_solvert::operator()( gamma_check_processed.clear(); non_gamma_complete_var.clear(); gamma_decvar.clear(); +#endif // store the initial values // of the decision varaibles @@ -1385,12 +1880,19 @@ property_checkert::resultt acdl_solvert::operator()( while(true) { // check the iteration bound - if(iteration > ITERATION_LIMIT) { + /*if(iteration > 4) { #ifdef DEBUG std::cout << "Iteration limit reached" << std::endl; #endif + print_solver_statistics(); + property_checkert::resultt res=check_using_solver(ssa_conjunction); + //return property_checkert::UNKNOWN; + if (res==property_checkert::PASS) + return property_checkert::PASS; + else if(res==property_checkert::FAIL) + return property_checkert::FAIL; break; - } + }*/ std::cout << std::endl << " ITERATION (decision):: " << iteration++ << std::endl @@ -1418,7 +1920,7 @@ property_checkert::resultt acdl_solvert::operator()( // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(elm); + // domain.preprocess_val(elm); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=elm.begin();it!=elm.end(); ++it) @@ -1428,8 +1930,14 @@ property_checkert::resultt acdl_solvert::operator()( std::cout << "Minimal unsafe element is" << from_expr(SSA.ns, "", conjunction(elm)) << std::endl; #endif print_solver_statistics(); - return property_checkert::UNKNOWN; - // break; + // Checking Using Solver + property_checkert::resultt res=check_using_solver(ssa_conjunction); + //return property_checkert::UNKNOWN; + if (res==property_checkert::PASS) + return property_checkert::PASS; + else if(res==property_checkert::FAIL) + return property_checkert::FAIL; + break; } std::cout << "****************************************************" << std::endl; @@ -1440,7 +1948,11 @@ property_checkert::resultt acdl_solvert::operator()( std::cout << "********************************" << std::endl; std::cout << " DEDUCTION PHASE " << std::endl; std::cout << "********************************" << std::endl; + clock_t total_time = 0.0; + const clock_t begin_time = clock(); result=propagate(SSA, assertion); + total_time = float(clock() - begin_time) / CLOCKS_PER_SEC; + std::cout << "Propagation Time in Iteration " << iteration << ": " << total_time << "seconds" << std::endl; std::cout << "****************************************************" << std::endl; std::cout << " IMPLICATION GRAPH AFTER DEDUCTION PHASE" << std::endl; @@ -1459,7 +1971,7 @@ property_checkert::resultt acdl_solvert::operator()( // preprocess abstract value: // transform constraints like // (x==n) to (x<=n) and (x>=n) - domain.preprocess_val(v); + // domain.preprocess_val(v); #ifdef debug std::cout << "preprocessed abstract value of implication graph: " << std::endl; for(acdl_domaint::valuet::const_iterator it=v.begin();it!=v.end(); ++it) @@ -1467,7 +1979,11 @@ property_checkert::resultt acdl_solvert::operator()( #endif // Do we call normalize_val_syntactic here ? !! +#ifdef BOX + domain.compute_normalized_val(v); +#else domain.normalize_val_syntactic(v); +#endif #ifdef DEBUG std::cout << "checking the propagation result UNKNOWN for completeness" << std::endl; #endif @@ -1475,6 +1991,7 @@ property_checkert::resultt acdl_solvert::operator()( // ensures that all variables are singletons // But we invoke another decision phase // to infer that "no more decisions can be made" +#ifdef GAMMA_COMPLETE_CHECK if(domain.is_complete(v, all_vars, non_gamma_complete_var, ssa_conjunction, gamma_decvar, read_only_symbols)) { // set complete flag to TRUE complete=true; @@ -1496,9 +2013,11 @@ property_checkert::resultt acdl_solvert::operator()( gamma_decvar.clear(); gamma_check_processed.clear(); non_gamma_complete_var.clear(); +#endif } else { std::cout << "SUCCESSFULLY PROVEN CASE" << std::endl; +#ifdef GAMMA_COMPLETE_CHECK // empty the gamma-complete check_processed // statement container and the // non_gamma_complete_var container @@ -1506,6 +2025,7 @@ property_checkert::resultt acdl_solvert::operator()( gamma_check_processed.clear(); if(non_gamma_complete_var.size() > 0) non_gamma_complete_var.clear(); +#endif // check for conflict do { @@ -1538,6 +2058,7 @@ property_checkert::resultt acdl_solvert::operator()( return property_checkert::PASS; } else { + unknown_result = true; goto END; // result=UNKNOWN when it breaks for here } } @@ -1588,6 +2109,14 @@ property_checkert::resultt acdl_solvert::operator()( } // end of while(true) END: std::cout << "Procedure terminated after iteration: " << iteration << std::endl; - print_solver_statistics(); - return property_checkert::UNKNOWN; + if(unknown_result == true) { + // Checking Using Solver + print_solver_statistics(); + property_checkert::resultt res=check_using_solver(ssa_conjunction); + if (res==property_checkert::PASS) + return property_checkert::PASS; + else if(res==property_checkert::FAIL) + return property_checkert::FAIL; + } + //return property_checkert::UNKNOWN; } diff --git a/src/acdl/acdl_solver.h b/src/acdl/acdl_solver.h index 6d8f203e0..143d60763 100644 --- a/src/acdl/acdl_solver.h +++ b/src/acdl/acdl_solver.h @@ -69,7 +69,7 @@ class acdl_solvert : public messaget // conds used by decision heuristics std::set cond_vars; acdl_conflict_grapht conflict_graph; - unsigned ITERATION_LIMIT=999999; + unsigned ITERATION_LIMIT=4; unsigned last_decision_index; @@ -106,6 +106,8 @@ class acdl_solvert : public messaget void initialize_decision_variables(acdl_domaint::valuet &val); void pre_process(const local_SSAt &SSA, const exprt &assertion, const exprt &assumption); bool is_closed(const local_SSAt &SSA, acdl_domaint::valuet& val); + property_checkert::resultt check_using_solver(const exprt &ssa_conjunction); + void make_deduction(const local_SSAt &SSA, const acdl_domaint::statementt &statement, const acdl_domaint::valuet &old_value, acdl_domaint::valuet &new_value); void print_solver_statistics(); }; diff --git a/src/acdl/acdl_worklist_base.cpp b/src/acdl/acdl_worklist_base.cpp index 5a7e4a087..6e6af042d 100644 --- a/src/acdl/acdl_worklist_base.cpp +++ b/src/acdl/acdl_worklist_base.cpp @@ -324,6 +324,22 @@ Function: acdl_worklist_baset::remove_live_variables() } } +/*******************************************************************\ + +Function: acdl_worklist_baset::size() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + + unsigned acdl_worklist_baset::size() + { + return worklist.size(); + } /*******************************************************************\ diff --git a/src/acdl/acdl_worklist_base.h b/src/acdl/acdl_worklist_base.h index 2002d5387..a8c4153bf 100644 --- a/src/acdl/acdl_worklist_base.h +++ b/src/acdl/acdl_worklist_base.h @@ -94,6 +94,8 @@ class acdl_worklist_baset : public messaget const acdl_domaint::statementt &statement); const acdl_domaint::statementt pop_from_list (listt &lexpr); + unsigned size(); + protected: worklistt worklist; diff --git a/src/acdl/acdl_worklist_forward_strategy.cpp b/src/acdl/acdl_worklist_forward_strategy.cpp index a87796f53..a00534c1e 100644 --- a/src/acdl/acdl_worklist_forward_strategy.cpp +++ b/src/acdl/acdl_worklist_forward_strategy.cpp @@ -10,7 +10,7 @@ Author: Rajdeep Mukherjee #include #include "acdl_worklist_forward_strategy.h" -// #define DEBUG +#define DEBUG /*******************************************************************\ diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index 09b5355ab..0e8672924 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -21,7 +21,7 @@ Author: Peter Schrammel #define SYMB_BOUND_VAR "symb_bound#" -#define ENABLE_HEURISTICS +//#define ENABLE_HEURISTICS /*******************************************************************\