Mentions légales du service

Skip to content
Snippets Groups Projects

fix provers detection in presence of paths that need escaping

Closed Armaël Guéneau requested to merge agueneau/why3:detection-quote-paths into master
1 unresolved thread

Paths with spaces in particular will currently make prover autodetection fail: query_prover_version fails to properly quote file paths when constructing the shell command. This patch thus uses Filename.quote to quote file paths.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
413 413 let cmd_regexp = Re.Str.regexp "%\\([.]?.\\)" in
414 414 let replace s = match Re.Str.matched_group 1 s with
415 415 | "%" -> "%"
416 | "f" -> use_stdin := false; file
416 | "f" -> use_stdin := false; Filename.quote file
  • I am pretty sure that this is wrong. Filename.quote is only meaningful when composing a whole command as a single string, e.g., to pass to Sys.command. Here the arguments already form a list, so any quote you add will end up in the actual arguments of the prover.

  • Armaël Guéneau changed this line in version 4 of the diff

    changed this line in version 4 of the diff

  • You're right, I was a bit too fast here and did not notice the splitting logic happening before. I was not able to decipher the logic of the code that uses the command after splitting (looks like it sends them to a socket separated by ;); do you know where the code is for the receiving end?

    In any case I removed that last commit---the first commit is really the one that fixes the issue that we were observing.

    Edited by Armaël Guéneau
  • The code is in src/server/request.c, which is part of an external server through which all the calls to provers go through. And now that I look at it, I notice that semicolons cannot be escaped, so it will break badly if there ever is an actual command line with a semicolon in it.

  • Please register or sign in to reply
  • Armaël Guéneau resolved all threads

    resolved all threads

  • GitLab does not let me merge your pull request, because the CI was not run on it, presumably because you have not enabled the CI on your own repository. (I think you are the first one to ever submit a pull request from an external repository, so it is possible that it is also a misconfiguration on our side.)

  • to me it looks like the CI is running on my why3 fork, but failing immediately because it cannot find the docker image registry.gitlab.inria.fr/agueneau/why3:ci-master-2023-11-13. Maybe the CI script only works when the owner of the repo is named why3, thus failing on forked repos?

  • More precisely, it only works for repository that have enabled a Docker registry and filled it with a suitable image. There are a bit more details in misc/ci.md. Summary: manually run a pipeline at least once with the variable NEW_BUILD_IMAGE set to an arbitrary value (e.g., 1).

  • right. now it looks like the dockerfile contains an outdated link to cvc4 (the cvc4 repo is now called cvc4-archived), which makes the build fail: https://gitlab.inria.fr/agueneau/why3/-/jobs/3962422

    (though intuitively I'd imagined PRs would be run against why3's usual CI pipeline, without having to setup one on my fork)

  • Your pipelines and jobs are private, so we cannot see them (which is why I could not distinguish a disabled CI from a failing CI). Anyway, if you fix misc/Dockerfile.build, do not forgot to also update the date in .gitlab-ci.yml (as explained in misc/ci.md). You can also run the following commands (completely untested):

    docker pull registry.gitlab.inria.fr/why3/why3:ci-master-2023-11-13
    docker tag registry.gitlab.inria.fr/why3/why3:ci-master-2023-11-13 registry.gitlab.inria.fr/agueneau/why3:ci-master-2023-11-13
    docker login -u agueneau -p the_access_token_from_your_settings registry.gitlab.inria.fr
    docker push registry.gitlab.inria.fr/agueneau/why3:ci-master-2023-11-13

    As for why the CI is run on the source repository rather than the target repository, it is a security reason. The target repository might be running custom CI workers or have some deployment jobs, so it is critical to prevent random people from triggering an unsanctioned pipeline on it.

  • Armaël Guéneau mentioned in merge request !1037 (merged)

    mentioned in merge request !1037 (merged)

  • Reopened as !1037 (merged) (I timeouted on making CI work on my fork).

  • Please register or sign in to reply
    Loading