Remove quotes around Z3 arguments

[fpoli]

The quotation marks that Silicon requires around Z3 arguments are annoying but also unnecessary. Usually, the issue is that scripts don't correctly forward arguments with spaces or quotes, but if so it's the script that should be fixed.

This PR removes the requirement for quotes and fixes the silicon.sh script. I also attempted to fix the silicon.bat script (%* should preserve spaces and quotes and %CMD% was probably dropping all quotes), but I don't have a Windows OS to test it.

For reference, I tested the following ways to run Silicon and they all work fine:

• From the sbt shell: run --z3ConfigArgs "model=true model_validate=true" prog.vpr
• From bash: sbt "run --z3ConfigArgs \"model=true model_validate=true\" prog.vpr"
• From bash: sbt 'run --z3ConfigArgs "model=true model_validate=true" prog.vpr'
• From bash: ./silicon.sh --z3ConfigArgs "model=true model_validate=true" prog.vpr
• From bash: ./silicon.sh --z3ConfigArgs 'model=true model_validate=true' prog.vpr

This PR is an alternative to #568.

This is a (small) breaking change for clients of Silicon that use --z3Args or --z3ConfigArgs.

[fpoli]

By the way, https://www.shellcheck.net/ is great for checking bash scripts.

[mschwerhoff]

Thank you! I'll try to find some time soon to test it on Windows, but not before next week.

Did you also test argument forwarding via sbt test, e.g. testOnly -- -n arithmetic.vpr -Dsilicon:z3ConfigArgs="model=true model_validate=true"?

[fpoli]

Did you also test argument forwarding via sbt test, e.g. testOnly -- -n arithmetic.vpr -Dsilicon:z3ConfigArgs="model=true model_validate=true"?

Is that the exact command? It doesn't seem to work for me, not even on master.

On master, the following works in the sbt shell:

sbt:Silicon> testOnly -- -n arithmetic.vpr "-Dsilicon:z3ConfigArgs=\\"model=true model_validate=true\\""

With this PR, the previous doesn't work and one of the following commands must be used.

sbt:Silicon> testOnly -- -n arithmetic.vpr "-Dsilicon:z3ConfigArgs=model=true model_validate=true"
sbt:Silicon> testOnly -- -n arithmetic.vpr \"-Dsilicon:z3ConfigArgs=model=true model_validate=true\"

It turns out that this is the expected behavior of the scalatest runner. First, sbt splits the command line in a list of arguments. This seems to be done in a naive way, so -Dsilicon:z3ConfigArgs="model=true model_validate=true" is (incorrectly, IMO) parsed as two arguments and makes scalatest complain, but "-Dsilicon:z3ConfigArgs=model=true model_validate=true" is parserd as one argument. I couldn't pinpoint the exact sbt code that implements this step. Then, if an argument starts with -D scalatest splits that into a key and a value using the first = in the argument (source). So, our spaces luckily end up in the value, and Silicon correctly preserves the spaces of the value (source).

[mschwerhoff]

Did you also test argument forwarding via sbt test, e.g. testOnly -- -n arithmetic.vpr -Dsilicon:z3ConfigArgs="model=true model_validate=true"?

Is that the exact command? It doesn't seem to work for me, not even on master.

I found that snippet in Silicon's wiki, I'm not surprised that the exact syntax no longer works.

On master, the following works in the sbt shell:

sbt:Silicon> testOnly -- -n arithmetic.vpr "-Dsilicon:z3ConfigArgs=\\"model=true model_validate=true\\""

With this PR, the previous sbt command incorrectly includes the quote at the beginning of the first key and at the end of the last value :-/ However, the following works fine (but it looks a bit odd):

sbt:Silicon> testOnly -- -n arithmetic.vpr "-Dsilicon:z3ConfigArgs=model=true model_validate=true"

I can live with that. It's probably a rather esoteric use-case anyway.

I'm now thinking that testOnly doesn't correctly parse arguments with quotes and spaces. Do you know if it's our code or sbt's code?

I guess everybody is involved in this syntax party: testOnly -- ... is due to sbt, the -D... bit is due to ScalaTest, the stuff after -D is then handled by us (Silver or Silicon).

[fpoli]

I just checked the command prompt on Windows 10 and pushed a fix:

• silicon.bat --z3ConfigArgs="model=true model_validate=true" prog.vpr works fine.
• silicon.bat --z3ConfigArgs "model=true model_validate=true" prog.vpr works fine.
• silicon.bat "--z3ConfigArgs=model=true model_validate=true" prog.vpr works (surprisingly) fine.
• silicon.bat --z3ConfigArgs 'model=true model_validate=true' prog.vpr and other attempts don't work.

[fpoli]

The testOnly -- -n arithmetic.vpr -Dsilicon:z3ConfigArgs="model=true model_validate=true" that doesn't work in the Sbt shell is a bug of Sbt. It should be fixed in the future Sbt v1.6.3.

[fpoli]

Any objection to merging this?

[mschwerhoff]

Any objection to merging this?

Not from my side.

[fpoli]

Great; I'll merge. I find really odd that users have to write things like --z3Args """""trace=true proof=true""""" :)