Open moyix opened 2 years ago
Ah, ok. The problem is that 0x17ed2e7f1ccbb000*33 is too big to turn into a 32-bit int. In JS I think this is silently handled but adding a & 0xffffffff
there helps ExpoSE get past that point. Unfortunately, after that it seems that XOR is not supported:
[!] Symbolic execution does not support operand ^, concretizing.
Oh, I forgot to add support for ^.
You could try adding support for xor through real to int conversion around here, see the >> and << operators for an example. If it works please let me know https://github.com/ExpoSEJS/ExpoSE/blob/20e2357764e6b007da4206ae89312722e58c33f0/Analyser/src/SymbolicState.js#L452. It might be a bit slow though because converting reals to ints in SMT is expensive.
I'm not sure if I added support for xor to z3javascript either but the change there is quite straightforward too.
Thanks, Blake
On Tue, 31 Aug 2021, 00:41 Brendan Dolan-Gavitt, @.***> wrote:
Ah, ok. The problem is that 0x17ed2e7f1ccbb000*33 is too big to turn into a 32-bit int. In JS I think this is silently handled but adding a & 0xffffffff there helps it. Unfortunately, after that it seems that XOR is not supported:
[!] Symbolic execution does not support operand ^, concretizing.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ExpoSEJS/ExpoSE/issues/107#issuecomment-908500062, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABYJP3CUQXWTKBUSZSWJ4TT7OYE7ANCNFSM5DCE73EQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.
I'm trying to test a small (non-cryptographic) hash function (NB: the actual function I want to test uses
charCodeAt()
, but since this isn't supported in ExpoSE, I switched to arrays of ints with some reasonable constraints):When I run this through ExpoSE with
EXPOSE_PRINT_PATHS=1
, it never finds the "Reachable" line (which can be reached with the inputtest
, i.e.[116, 101, 115, 116]
. Instead it generates lots of test cases with this exception (full log attached):Full log: expose_error.txt
Any idea what is going wrong here? Or did I do something wrong with the constraints?