Copilot-Language / copilot

A stream-based runtime-verification framework for generating hard real-time C code.
http://copilot-language.github.io
635 stars 50 forks source link

`copilot-c99`: test failure on non-Intel architectures #468

Closed swt2c closed 9 months ago

swt2c commented 10 months ago

After upgrading to copilot 3.17 in Debian, we noticed that copilot-c99 experiences a test failure on non-Intel architectures (e.g., everything but amd64 and i386).

Copilot.Compile.C99:
  Compile specification: [OK, passed 1 tests]
  Compile specification in custom dir: [OK, passed 1 tests]
  Run specification: [Failed]
*** Failed! Exception: 'callProcess: ./main (exit 64): failed' (after 1 test):

This failure was first seen in Debian with copilot 3.16, but there were also a large number of other Haskell changes in Debian simultaneously (e.g., upgrade to GHC 9.4, lots of package updates, etc.), so it's possible it may not even be related to a copilot change.

Here is one build log (arm64): https://buildd.debian.org/status/fetch.php?pkg=haskell-copilot-c99&arch=arm64&ver=3.17-1&stamp=1699927953&raw=0

Do note that there are a large number of compile warnings - not sure if they're related or not. Let me know if I can help test anything on any of the failing architectures.

ivanperez-keera commented 10 months ago

Thanks a lot for filing this. This is very useful.

Looking at the log, I suspect the way that the C code being generated for the tests to be incorrect (not Copilot itself or the C code that Copilot generates). There's a seed for the random number generator, so I'll see if I can reproduce the error on my side.

ivanperez-keera commented 10 months ago

Is there any way to ssh into the machine in which the problem manifests and look at the files that are being generated for the tests?

If you comment out the following lines:

https://github.com/Copilot-Language/copilot/blob/cfc565bcf52dd359eb7ee768549459402c1785df/copilot-c99/tests/Test/Copilot/Compile/C99.hs#L171-L184

or guard them with a Control.Monad.unless (r && r2) $ do, any tests that fail during that stage should leave their temporary files in /tmp/ in a directory with a file name starting with copilot_test_*.

ivanperez-keera commented 10 months ago

I don't want to take a lot of your time, but I'm happy to jump on a teams/jitsi/google meet call as well if that makes things easier.

ivanperez-keera commented 10 months ago

More specifically, for the test that fails, I'd like to know the C code in the temporary directory, if a main file is being generated by this line, if it is executable, and what happens when you run it manually.

ivanperez-keera commented 10 months ago

For the record: the test "Run and compare results: [OK, passed 100 tests]" is in principle a stronger property than "Run specification: [Failed]".

swt2c commented 10 months ago

Yes, I'll provide the info later today.

swt2c commented 10 months ago

OK, so it appears the test failure is due to the exit code of the main program being non-zero. When I run this code on arm64, the return code is 64. When I compile/run the same code on s390x, the return code is 32. When I compile/run it on amd64, the return code is 0, so the test passes.

copilot_test.zip

ivanperez-keera commented 10 months ago

Thanks! That's really helpful.

Looking at the code, the only reason I can think of is that main is void and does not return an int. If you make it:

int main () {
  step();
  return 0; // not really necessary, the compiler should add it.
}

Does that make it finish with a zero exit code on all architectures?

If so, the only thing that should be needed would be to change these lines:

https://github.com/Copilot-Language/copilot/blob/cfc565bcf52dd359eb7ee768549459402c1785df/copilot-c99/tests/Test/Copilot/Compile/C99.hs#L160-L162

To be exactly what I wrote above (without the comment).

swt2c commented 10 months ago

Yes, tested on arm64 and s390x, that does it. In fact, just changing void main to int main seems to be enough.

ivanperez-keera commented 10 months ago

Great! Then I'll change the type and leave the return out.

In that case, since it's a change that does not affect the behavior of Copilot itself, I'm perfectly happy with that being added in a patch in Debian if you don't want to wait until Jan 7, date of the next release.

I'll nevertheless add that change to the next version of Copilot.

swt2c commented 10 months ago

Yes, I'm fine with patching it in Debian for now, thanks for the help on this!

ivanperez-keera commented 10 months ago

Not at all. Thank you for making Copilot available in Debian (and Ubuntu) and staying on top of this. It's very much appreciated!

We can keep this issue open. I'll file a normative change request as part of this issue and you can use the same to track the change as it is incorporated in the code.

swt2c commented 10 months ago

BTW, do you mind also addressing this compiler warning? It's pretty minor but it is making a lot of noise in the logs. If you want me to open separate issue, let me know. I think all that probably needs to change is print uint64_t literals with a 'u' suffix so the compiler knows you meant them as unsigned?

main.c:9:365: warning: integer constant is so large that it is unsigned
    9 | uint64_t input_s[] = {15291473201395682872, 10905784304967329508, 16467342249657270187, 10380022383085673006, 8808850476626865482, 9331686954424886256, 2988792302337284835, 10094298997864850026, 1468541681369587729, 3802989542683056631, 1164297040666367757, 3640577629385025211, 905756448397535883, 17897243026464339846, 14179972523351926499, 9062152164204472610, 18186815000375765879, 4041036899977049094, 11229731164463841047, 10199627404646347090, 7530829744262396702, 6187653587061731428, 4847037323169053880, 3830831149839427783, 4417008097145766959, 3023259657812248252, 11614016706524838309, 15231127259321513957, 10996668593829027093, 12561799129876566620, 4120603157431323089, 18121344584850217889, 9390006711635640817, 16758242090817315342, 3806993773191624339, 18445926482801193618, 1687823873216649825, 16627525741516087341, 17386160218225282051, 3453828944607607838, 2802898128251058135, 12764473243802298326, 11231994547743023304, 12825245891782798760, 4623532431097592945, 586414121165670966, 8547741542992700863, 15559938295201891062, 9670294815228139729, 3710405262775010567, 17468151033345401482, 17716485089625129320, 12747914728439172598, 4801419759350804598, 9125580210493606276, 3823710419484429364, 2154581673505147229, 6467376409986464792, 2408103098282617881, 14444475328776726089, 2705535792281951053, 12413026741257244877, 11678830985309772531, 2267681885789229711, 647152409655960647, 3397826581273517893, 10208667243921605473, 9174888931553107939, 4634462628651462753, 16867097090869968537, 1259451907261022727, 12401447623539863946, 882828797904240771, 18018064055079466704};
      |                                                                                                                                                                                                                                                                                                                                                                             ^~~~~~~~~~~~~~~~~~~~
ivanperez-keera commented 10 months ago

I don't mind at all.

Since it's a separate problem, let's open a separate issue :)

ivanperez-keera commented 10 months ago

Description

copilot-c99's tests fail on non-Intel architectures. The issue is that the return code of the programs being generated (and executed) during tests are not zero, which the test interprets as a failure. More specifically, the return type of the main function included in the generated C code is void, but should be int. By making it int and returning 0, the testing system will not interpret the test as a failure.

Type

Additional context

None.

Requester

Method to check presence of bug

Running copilot-c99' tests can lead to failures depending on the architecture and compiler used, producing errors such as:

Copilot.Compile.C99:
  Compile specification: [OK, passed 1 tests]
  Compile specification in custom dir: [OK, passed 1 tests]
  Run specification: [Failed]
*** Failed! Exception: 'callProcess: ./main (exit 64): failed' (after 1 test):

This error manifests on non-Intel architectures.

Expected result

The above test should run without errors.

Desired result

The above test should run without errors.

Proposed solution

Modify the tests for copilot-c99 so that the main has type int and returns 0.

Further notes

The decision of what value to return upon program termination is dependent on the C standard, the compiler and architecture.

ISO C Standard (ISO/IEC 9899:1999) states in section "5.1.2.2.3 Program termination":

If the return type of the main function is a type compatible with int [...] reaching the } that terminates the main function returns a value of 0. If the return type is not compatible with int, the termination status returned to the host environment is unspecified.

ivanperez-keera commented 10 months ago

Change Manager: Confirmed that the issue manifests.

ivanperez-keera commented 10 months ago

Technical Lead: Confirmed that the issue should be addressed.

ivanperez-keera commented 9 months ago

Technical Lead: Bug scheduled for fixing in Copilot 3.18.

Fix assigned to: @ivanperez-keera.

ivanperez-keera commented 9 months ago

Implementor: Solution implemented, review requested.

ivanperez-keera commented 9 months ago

Change Manager: Verified that:

ivanperez-keera commented 9 months ago

Change Manager: Implementation ready to be merged.