Updated from KLEE:2.0 to 2.3.

[kt218]

Updated expected output of KLEE in tests/fixtures/.stdout and e2e.test.js. Added Klee header within frontend fixtures that use Klee functions. Updated to clang-11 within worker/processor/.py. Replaced klee_stats.py with one from Klee/klee and modified to return dict. Updated ymls to use import_tasks due to depraction of include.

[ccadar]

Thanks for this useful update, @kt218 .
Just wondering: do you know why we keep a copy of klee-stats.py in there?

[kt218]

Previously klee-stats.py was the old version with changes made to return a list of tuples for the stats. I decided to work from there and realising the issue was caused by the switch from csv to sql, I decided to copy the new klee-stats and made it return the list of tuples. Let me know if I should instead remove this file and use docker>klee>klee-stats to return csv and use csv data instead.

[ccadar]

@kt218 yes, we need to use the new klee-stats, which stores data in SQL format.
But I think it would be better to use it directly from the Docker container if possible, so as not to have the same file in two places.

[kt218]

I've had a chat with Anastasios and for the removal of the duplicated klee-stats within klee-web, I would need to run klee-stats to KLEE docker. However, it requires tabulate to be installed. I've PR the main KLEE with this fix #1521. I'm not sure if it was fixed within #1070. I've pulled from KLEE:latest from Docker and tabulate wasn't installed for me.

[kt218]

Updated commit to have klee-stats.py removed and now using KLEE docker's klee-stats. This will only work assuming the KLEE container has tabulate dependency installed.

[ccadar]

Great, I merged https://github.com/klee/klee/pull/1521 and restarted the CI

[kt218]

I think the KLEE image on Dockerhub needs to be updated.

[ccadar]

@MartinNowack would it be possible to help with this?

[MartinNowack]

Please try again - the updated image is online.

[ccadar]

Thanks, @MartinNowack, we appreciate doing this so quickly. @kt218 I restarted the CI, but it still fails. Is the failure due to something else?

[kt218]

I'll have to change the tag of the KLEE docker image to latest instead of 2.3

[MartinNowack]

@kt218 Current error message is:

"Error running klee-stats --table-format csv /tmp/code/klee-out-0:\n    usage: klee-stats [-h] [--to-csv] [--grafana] [--grafana-host GRAFANA_HOST]\n                      [--grafana-port GRAFANA_PORT]\n                      [--print-all | --print-rel-times | --print-abs-times | --print-more | --print-columns COLUMNS]\n                      dir [dir ...]\n    klee-stats: error: unrecognized arguments: --table-format\"\n\n      20 | 

Do you need the continuous values of one run or the final ones?

[kt218]

Just the final ones. That should have been fixed with tabulate installed.

[kt218]

I've ran the latest docker locally and found that tabulate wasn't installed. I'm unsure why this is the case.

[ccadar]

Something to debug. @MartinNowack mentioned to me that we need to pay attention for which users it is installed (klee? root?)

[kt218]

@ccadar @MartinNowack Not sure if this is the right place but removing tabulate install within both scripts/build/p-klee-osx.inc and scripts/build/p-klee-linux-ubuntu.inc, allows pip3 to be installed from the Dockerfile. Now tabulate is installed on my local machine.

With the current latest the console message when Docker RUN pip3 install tabulate is:

Step 38/46 : RUN pip3 install tabulate
 ---> Running in bc6a1903e605
Requirement already satisfied: tabulate in /root/.local/lib/python3.6/site-packages

I'm unsure how these removals would affect other installation methods; e.g. through manual LLVM build.

[MartinNowack]

I opened a new PR (https://github.com/klee/klee/pull/1525). This fixes a couple of other annoyances and also installs the python modules in the right directory. @ccadar needs to merge it and I can build and push the image. With a locally built version, the tabulate works for me.

In a nutshell, the build scripts are now executed by the klee user while earlier versions required the root user to be successful. That should hopefully fix your issue.

Beside that, changes in this PR look good 😄 - it's just a matter of upstream fixes.

[MartinNowack]

I just pushed the updated image - please give it a try :)

[ccadar]

Thanks, @MartinNowack ! I've restarted the checks.

[ccadar]

Excellent, they pass now, let's merge this!

[andronat]

🚀🍾

[andronat]

BTW may I suggest that we shouldn't point directly to the latest klee docker image. Rather we should set a fixed version. The reason is that any changes should be first reflected into the code so CI can catch any errors. Currently, with using latest, if I re-deploy klee-web in production, I might download a newer version on klee which might break.

[ccadar]

@andronat I agree, the reason for that change was that the latest release of KLEE does not have the full klee-stats functionality in the Docker image.

@kt218 One option would be to apply the Dockerfile change to the 2.3 branch in KLEE, after which we can push a new Docker image for KLEE 2.3.

[MartinNowack]

Another alternative would be to use klee_version to specify the sha of the image (https://hub.docker.com/layers/klee/klee/latest/images/sha256-b38cc919a569319ad58bd9ab39e0e657b2b30bb1a2ea8e2df8cef7cde36ff5f6?context=explore) to keep this version fixed for now. And update later to a newer version if required. Currently this variable is only used for the docker image so it should work.