search

uuverifiers / ostrich

An SMT Solver for string constraints
Other
35 stars 8 forks source link

Potential soundness issue of unicode string encoding #26

Closed rainoftime closed 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula 

(set-logic QF_S)
(assert (= "\x4a" "\x4A"))
(check-sat)

ostrich and z3 yield sat, but cvc4 gives unsat.

Intuitively, I may respect the result would be unsat. Is this different because of the changes in the SMT-LIB2 standard?

uuverifiers commented 3 years ago

That's a good observation! The differences in behaviour are due to the supported escape sequences. CVC4 follows the standard literally, and only accepts the escape sequences "" and \u..., whereas Ostrich and Z3 also support \x... (as common in JavaScript, etc.), and therefore interpret \x4a and \x4A as the same character.

This is something I'm trying to clean up in Ostrich at the moment.