Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CN: Fix CI #664

Merged
merged 1 commit into from
Oct 28, 2024
Merged

CN: Fix CI #664

merged 1 commit into from
Oct 28, 2024

Conversation

dc-mak
Copy link
Contributor

@dc-mak dc-mak commented Oct 28, 2024

For some reason this test is causing a CI failure related to SMT issues that is not reproducible locally: #663

For some reason this tests is causing a CI failure related to SMT issues
that is not reproducible locally: rems-project#663
@dc-mak
Copy link
Contributor Author

dc-mak commented Oct 28, 2024

E.g like this:

[./cn/record1.c]...
./cn/record1.c:13:18: warning: Treating exponentiation 'power(2'i32
  , 31'i32 /* 0x1f */)' as uninterpreted.
/*@ requires x < power(2i32, 31i32) - 1i32; 
                 ~~~~~^~~~~~~~~~~~~ 
./cn/record1.c:14:18: warning: Treating exponentiation 'power(2'i32
  , 31'i32 /* 0x1f */)' as uninterpreted.
    requires y < power(2i32, 31i32) - 1i32; @*/
                 ~~~~~^~~~~~~~~~~~~ 
cn: internal error, uncaught exception:
    UnexpectedSolverResponse((error
      "line 727 column 67: unknown constant cn_tuple_2 ((_ BitVec 32) (_ BitVec 32)) \
     \ndeclared: (declare-fun cn_tuple_2\
     \n             ((_ BitVec 64) (_ BitVec 64))\
     \n             (cn_tuple_2 (_ BitVec 64) (_ BitVec 64))) "))
    Raised at Cn__Solver.debug_ack_command in file "backend/cn/lib/solver.ml", line 164, characters 4-42
    Called from Cn__Solver.provable in file "backend/cn/lib/solver.ml", line 1409, characters 4-68
    Called from Cn__ResourceInference.General.parametric_ftyp_args_request_step in file "backend/cn/lib/resourceInference.ml", line 142, characters 16-26
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.sandbox in file "backend/cn/lib/typing.ml", line 86, characters 10-13
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 169, characters 6-443
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 188, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
FAIL (Unexpected return code: 125)

It started here: https://github.com/rems-project/cerberus/actions/runs/11468005495/job/31949217625 but that doesn't seem related. Could be related to the Z3 used by the VM used by the CI.

@podhrmic
Copy link
Contributor

This can be caused by the different installation - in the CI, you are pinning various packages, but not calling make in the process. While for the local install, I am assuming you are calling the makefiles as mentioned in the documentation - is that correct?

@podhrmic
Copy link
Contributor

[This MR] is an attempt to at least unify the docker and CI builds, but it is still not clear which way of building/installing Cerberus/CN is the right one.

@dc-mak
Copy link
Contributor Author

dc-mak commented Oct 28, 2024

Pinning the packages should be the same as calling the Makefile (see the Makefile and opam files). Also, the link to the PR in your comment is broken.

@dc-mak dc-mak merged commit fd56751 into rems-project:master Oct 28, 2024
2 checks passed
@dc-mak dc-mak deleted the cn-fix-ci branch October 29, 2024 16:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants