[CN] Fix #380 (Have ptr_eq typechecks its arguments)

[dsainati1]

Fixes #380

[dc-mak]

On the right track overall, thank you. Should be ready to merge in a couple of iterations I think.

[dc-mak]

Last round of changes - just a few tweaks, thank you so much. If you can rebase and squash that would also be helpful.

[dc-mak]

Also once this PR is done and merged, can you do a quick PR adding .mli files for Core_to_mucore and Compile? https://github.com/rems-project/cerberus/blob/master/backend/cn/ONBOARDING.md#adding-mli-files

[dc-mak]

There look to be CI failures. Can you please investigate? One of them is code-formatting.
For runtime testing related things, you can ask @rbanerjee20 if you get stuck.

[dc-mak]

Lgtm but CI is failing.

[dsainati1]

Hmm, I don't know exactly what the failing runtime tests are or how to invoke them locally, and the CI job needs to be approved by a maintainer.

[dc-mak]

Are you able to view which CI jobs pass or fail? And the logs of those or not?

Regardless, if you look in the workflow file, you'll find the command: https://github.com/rems-project/cerberus/actions/runs/10599783302/workflow?pr=522#L85 : cd tests && ./run-cn-exec.sh

Before running the file, you can open it to see timeout 20 "${CHECK_SCRIPT}" "${SCRIPT_OPT}" "$file" &> /dev/null called in a function which is called in a loop. Alternatively, you can uncomment set -xv for debugging and run the file itself.

It will produce a bunch of output, including something like /home/dhruv/.opam/4.14.1/lib/cn/runtime/libexec/cn-runtime-single-file.sh -oq tests/cn/missing_resource_indirect.error.c which can be simplified down to
${OPAM_SWITCH_PREFIX}/lib/cn/runtime/libexec/cn-runtime-single-file.sh -oq tests/cn/missing_resource_indirect.error.c
or
./runtime/libcn/libexec/cn-runtime-single-file.sh -oq tests/cn/missing_resource_indirect.error.c

We should add this to the ONBOARDING doc.

[dc-mak]

If you follow a similar process with the CI build workflow, you'll see that slf_incr2.c in the tutorial repo is now failing (because ptr_eq is now stricter).

[dsainati1]

I submitted rems-project/cn-tutorial#83 to the tutorial repo to fix the issue with slf_incr2.c, and fixed the runtime issue I believe.

[dc-mak]

The tutorial is still failing for some reason even though your change was merged in rems-project/cn-tutorial#83

The runtime is now showing a further bug - it needs to be told where to find and substitute definitions of the builtins.

[dc-mak]

See above.

[rbanerjee20]

The runtime is now showing a further bug - it needs to be told where to find and substitute definitions of the builtins.

I'll take a look

[rbanerjee20]

This is what I'm getting when running the single-file runtime testing script on slf_incr2.c:

slf_incr2.c:19:21: error: Type error
            ptr_eq (vs_.pv,
                    ~~~^~~ 
Expression 'vs_.pv' has type 'u32'.
I expected it to have type 'pointer' because of other location (<builtin>) 

Failed to generate C files from CN-annotatated source.

Is this the same error you were talking about @dc-mak ?

[dsainati1]

That should be fixed, the tutorial's version of slf_incr2.c should be updated to use == instead of ptr_eq there.

[rbanerjee20]

Ah - the CN runtime testing CI relies on the cn-runtime-testing branch of the CN tutorial, not main. It will use main soon but this is still a WIP. I can update that branch and see if it helps with the Cerberus CI

[rbanerjee20]

Great, so runtime testing CI seems to be working again with that same change from the main branch of CN tutorial now also applied to cn-runtime-testing. I did try the script locally on slf_incr2.c and got the following 2 warnings though:

cn.c:43:34: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return convert_to_cn_bits_i64(-9223372036854775808);
                                 ^
cn.c:78:33: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return convert_to_cn_bits_u64(18446744073709551615);
                                ^
2 warnings generated.

Looks a bit suspicious that these kinds of integer literals are being generated - probably worth investigating even though the runtime testing CI is happy now.

[rbanerjee20]

And the remaining CI failure seems to be CN test-gen-related - @ZippeyKeys12 would be the right person to ask about this.

[dc-mak]

Great, so runtime testing CI seems to be working again with that same change from the main branch of CN tutorial now also applied to cn-runtime-testing. I did try the script locally on slf_incr2.c and got the following 2 warnings though:

cn.c:43:34: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return convert_to_cn_bits_i64(-9223372036854775808);
                                 ^
cn.c:78:33: warning: integer literal is too large to be represented in a signed integer type, interpreting as unsigned [-Wimplicitly-unsigned-literal]
  return convert_to_cn_bits_u64(18446744073709551615);
                                ^
2 warnings generated.

Looks a bit suspicious that these kinds of integer literals are being generated - probably worth investigating even though the runtime testing CI is happy now.

Known issue: #536