search

SRI-CSL / OCCAM

OCCAM: Object Culling and Concretization for Assurance Maximization
BSD 3-Clause "New" or "Revised" License
26 stars 10 forks source link

Runtime error in Yices after specialization with OCCAM #40

Closed mudbri closed 3 years ago

mudbri commented 3 years ago

The specialized Yices results in the following runtime error.

../abc.ys: internal error Internal exception: opcode = 7

*************************************************************
FATAL ERROR: Term-stack error

Please report this bug to yices-bugs@csl.sri.com.
To help us diagnose this problem, please include the
following information in your bug report:

  Yices version: 2.6.1
  Build date: 2021-04-15
  Platform: x86_64-pc-linux-gnu (release)

Thank you for your help.
*************************************************************

I am using version 2.6.1 of Yices. The tar file for Yices-2.6.1, make file to get bitcode, and manifest file is included in the zip.: yices_issue.zip. The issue can be reproduced in the following way:

  1. make
  2. slash --work-dir=slash --disable-inlining --inter-spec-policy=none --intra-spec-policy=onlyonce --use-pointer-analysis yices_main.manifest
  3. cd slash and then ./yices_main_fin ../abc.ys

Note: This error disappears and the specialized binary works correctly if we don't use the --use-pointer-analysis flag with slash.

caballa commented 3 years ago

I think here yices_main_fin crashes for the same reason that https://github.com/SRI-CSL/OCCAM/issues/41. So after you do the steps I mentioned in https://github.com/SRI-CSL/OCCAM/issues/41, try again.

caballa commented 3 years ago

I'll close it for now. Let me know if you still have problems.

mudbri commented 3 years ago

I am still getting the same error when I run yices_main_fin after specializing it with the --use-pointer-analysis flag. I am using commit 07241b3fad62eaa280b80e4801da229fd1a3a475. Again, this error disappears and the specialized binary works correctly if I don't use the --use-pointer-analysis flag with slash.

caballa commented 3 years ago

This seems to be solved after commit https://github.com/SRI-CSL/OCCAM/commit/ca2e84536c7d356af439634de0fb2900db1f622e