search

PLSysSec / sys

Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
https://cseweb.ucsd.edu/~dstefan/pubs/brown:2020:sys.pdf
GNU General Public License v2.0
215 stars 41 forks source link

Timed out when perform the uninit check #25

Closed pcy190 closed 3 years ago

pcy190 commented 3 years ago

I run the sys with the uninit check:

stack exec sys -- -c uninit -e prod -d ./compile_out/

However, after a long while, it failed with the timed out error:

Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector
Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector
Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector

I wonder whether there is an option or modification of code to change the default time for solver to solve the constraint, in order to avoid the timed out case.

deian commented 3 years ago

Yep! https://github.com/PLSysSec/sys/blob/821c4d7cf924e68838c128cbe824be46c9955416/src/Checkers/SymexConfigs/CheckerConfigs.hs#L61

deian commented 3 years ago

We should make the cli more friendly #26