search

pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
101 stars 29 forks source link

State refinement is incorrect in presence of some assumptions on class pre-loading #34

Closed pietrobraione closed 4 years ago

pietrobraione commented 4 years ago

One of the invariants of the method State.refine() is that if i is the initial state of a symbolic execution and f is the final state, then i.refine(f) can be the initial state of another symbolic execution that will end in a state equivalent to f. This currently does not work because refinement of clauses on pre-loading of classes is broken in the case the clause is pre_init(class), with the further constraint that class is not symbolically but concretely pre-loaded (e.g., when it has a pure class initializer). The refined state should re-run the class initializer, since its (concrete) Klass deriving from the refinement is in a zeroed state, but this is not done.

pietrobraione commented 4 years ago

Fixed by commit 66a1208.