Deep concretization can reduce exploration if a concrete call happens before a symbolic one

ExpoSEJS / ExpoSE

A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.

MIT License

185 stars 36 forks source link

Deep concretization can reduce exploration if a concrete call happens before a symbolic one #37

Closed jawline closed 5 years ago

jawline commented 5 years ago

The safety check on concretization of objects (for example the result of exec) can make that object concrete prior to a symbolic call.

The correct behavior here is difficult to model but it would be nice if there was at least a limit support for code like

var x = /Hello/.exec(S$.symbol('A', ''));
console.log(x);
if (x && x[0] == "What") { throw 'Woops' }