Add learning exercises

[bboston7]

This PR adds exercises for learning SAW to the repository and integrates those exercises into the CI system so they do not go stale with future SAW changes. This is a large PR, but I'm only looking for feedback on a small portion of it. Specifically I'm looking for feedback on the CI integration, as well as the placement of the exercises within the repo itself. I'm not so much looking for feedback on the content of the exercises themselves, which have already through review via other channels.

[kquick]

I just have a couple of concerns here.

1. There are a lot of repeated files in each subdirectory (Makefile, helpers.saw). This means that any change needed would need to be repeated identically in about a dozen different places (and divergence and mistaken updates becomes an additional concern). There is probably some extra-CI impact on some of these concerns in regards to the examples being self-contained and easy to follow, but it would be great of those could be moved to someplace like examples/common/Makefile and examples/common/helpers.saw and included directly from there.

2. I'm not wild about checking in the .bc files: we don't usually like to commit output files, and this could fail a make step depending on the order of git file writing; I do see the advantage of having a known .bc file to operate against though. Another point of concern: which version of LLVM was used to create these files? I'd suggest:
   a. At least renaming them to xxx.llvmN.bc,
   b. and then consider whether the CI should regenerate the .bc via make or use one or more existing stored .llvmN.bc files (or both!).

3. The setup may need adjusting; see Fall back to Z3 4.8.8 on AWSLC/BLST proofs #1775 (comment) and here as well, consolidation of setup into a single location would be a plus.

4. Somewhat in contradiction to my consolidation and DRY statements above, I'd suggest creating a separate job in CI rather than combining these with the s2n proofs, and creating whatever necessary dockerfile and corresponding infrastructure needed under examples to keep examples independent of s2n. My reasoning here includes:

   • separation of concerns (it's conceivable that we might do things with s2n like move them in the future)
   • s2n CI is a VERY long run, and if examples is also long (or even if it's short) we will have to adjust things like the allowed time to perform this job.
   • Running examples CI in parallel to s2n CI would decrease overall test time, and it would be great if examples run faster and can reveal issues faster (s2n is good at detecting breakage, but again, it is a VERY long run).

I would prefer to see 2a addressed as a minimum (and 3 checked/confirmed if not consolidated), but the rest of this is subjective and I'd welcome any discussion that brings in other considerations (like the ability to use examples for students).

[RyanGlScott]

At least renaming them to xxx.llvmN.bc

A less invasive alternative is to compile each .bc file using -frecord-command-line. Doing so will cause the Clang version to be embedded into the .bc file itself. At that point, ascertaining the LLVM version is a simple matter of running llvm-dis *.bc and looking at the resulting .ll file.

[kquick]

At least renaming them to xxx.llvmN.bc

A less invasive alternative is to compile each .bc file using -frecord-command-line. Doing so will cause the Clang version to be embedded into the .bc file itself. At that point, ascertaining the LLVM version is a simple matter of running llvm-dis *.bc and looking at the resulting .ll file.

Oh, that's a nice flag, I wasn't aware of that one. I still would suggest a filename difference, because we might want to run some of these tests against different llvm versions (i.e. we may have the same xxx for different N values), plus it's easier to tell the version when you don't have an active llvm-dis environment. That said, I think we should also be always using that flag to record the full command line for the reasons you noted in #1157.

[bboston7]

Thanks for the feedback! I made the following changes:

1. Moved helpers.saw and Makefile to exercises/common and updated all of the exercises to use them.
2. Removed all .bc files and updated the docker entrypoint to build them. The C files are very simple, so I'm not worried about compiler differences causing dramatically different .bc files to the point where SAW proofs have to change.
3. Fixed the issue with redownloading the what4-solvers that I inherited from basing this off the BLST setup.
4. Created a separate job in the CI to run examples.

@kquick Can you please take another look when you get a chance? My .github/workflows/ci.yml file probably deserves some extra attention because I don't have much Github CI experience. Specifically, I was unsure of whether I needed the matrix setting, given that I only have a single element in it.

[kquick]

@bboston7 , can you check the output of the "run exercises" step in the CI: https://github.com/GaloisInc/saw-script/actions/runs/3642679289/jobs/6150910776. It doesn't fail, but there are errors reported from the saw runs: are those expected or is this CI process not detecting failures properly?

If it's the former, we probably want a note about this somewhere (possibly the ci.yaml) but I'm wondering how we would tell the difference between an expected failure and an actual failure?

[bboston7]

It doesn't fail, but there are errors reported from the saw runs: are those expected or is this CI process not detecting failures properly?

This was confusing to me too, but these aren't errors. It looks like at some point the behavior of print_goal changed to also print whatever error message would occur if the goal were to fail. For example, if you look at the pop_count proof output starting on line 1236:

[21:50:21.933] Loading file "/workdir/functional-correctness/popcount/solution.saw"

[21:50:22.014] Verifying pop_count ...
[21:50:22.026] Simulating pop_count ...
[21:50:22.031] Checking proof obligations pop_count ...
[21:50:22.031] Goal pop_count (goal number 0): return value matching
at /workdir/functional-correctness/popcount/solution.saw:12:1 in _SAW_verify_prestate
/workdir/functional-correctness/popcount/solution.saw:12:1: error: in _SAW_verify_prestate
Literal equality postcondition


let { x@1 = bvNat 32 858993459
      x@2 = bvAdd 32
              (bvMul 32 (bvNat 32 4294967295)
                 (bvAnd 32 (bvNat 32 1431655765) (bvShr 32 x 1)))
              x
      x@3 = bvAdd 32 (bvAnd 32 x@1 x@2)
              (bvAnd 32 x@1 (bvShr 32 x@2 2))
      x@4 = bvAnd 32 (bvNat 32 252645135)
              (bvAdd 32 x@3 (bvShr 32 x@3 4))
      x@5 = bvAdd 32 x@4 (bvShr 32 x@4 8)
    }
 in EqTrue
      (implies True
         (implies True
            (bvEq 32
               (bvAnd 32 (bvNat 32 63) (bvAdd 32 x@5 (bvShr 32 x@5 16)))
               (popCount x))))

[21:50:22.945] Proof succeeded! pop_count

The proof succeeds (as evinced by the "Proof succeeded!" text), but the goals have been annotated with their error messages. I'm not sure when this change happened, but it's definitely new since SAW 0.9. The most relevant thing I can find is ticket #1372, which exhibits the same behavior. @RyanGlScott, did you end up adding the feature in that ticket?

[bboston7]

As far as detecting failures goes, the docker image returns a non-zero exit code if a proof fails. I assume that's enough for the CI to detect the error?

[bboston7]

The last few commits did a few things:

• I removed uses of print_goal because the output is confusing and clutters up the CI log.
• I tested the CI catches failing proofs by breaking a proof in commit ea46f09. As expected, this caused the CI job to fail: https://github.com/GaloisInc/saw-script/actions/runs/3643718895/jobs/6152742009

I've now reverted the broken proof, so the job should pass again.

[RyanGlScott]

The most relevant thing I can find is ticket #1372, which exhibits the same behavior. @RyanGlScott, did you end up adding the feature in that ticket?

Nope. I have no idea why the behavior has changed.

[kquick]

Looks good, thanks for the updates!