search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

Fixing bug in TxPathCondition::unsatCoreInterpolation to mark constra… #320

Closed rasoolmaghareh closed 7 years ago

rasoolmaghareh commented 7 years ago

…ints in the currentPC node and all related parents

domainexpert commented 7 years ago

I noticed a difference in the subsumption profile in for loop_safe2.c. The patch seems to have fixed the wrong subsumption here as well. Before the patch, the tree looks like this: tree The subsumption is incorrect in the above picture since, e.g., i==1 is subsumed by i==0. The following is the tree after applying the patch (no subsumption). tree

domainexpert commented 7 years ago

Also for basic/regexp_mark.c of klee-examples the reduction in the number of subsumptions from 15 to 12 is justified: Subsumption no. 2 in the old version no longer happens with this patch. This is justified since there are contradictory constraints !(36=re[1]) (an interpolant) in one of the path and (36=re[1]) in the other path. Similarly with subsumpton no. 8 and no. 9. See the old tree before the patch below. The mentioned subsumptions no longer exist in the new version.

tree

domainexpert commented 7 years ago

Reduction in subumption count also noticeable in basic/queens.c. The reduction is justifiable since in the old version subumption no. 8 was wrong (of node 50 by 40).

domainexpert commented 7 years ago

Reduction of subsumption is also noticeable for basic/regexp_nonrecursive1.c. Similar to the previous cases, 2 over-subsumptions corrected, reducing the subsumption count from 4 to 2.

domainexpert commented 7 years ago

Thanks @rasoolmaghareh !