--help fails with an exception
fpoli opened this issue · 3 comments
fpoli commented
Executing silicon --help fails with an exception. Also:
- The formatting of the description of some options is broken (
--proverSaturationTimeoutWeights,--stateConsolidationMode,--z3SaturationTimeoutWeights). -Llogger=levelis indented in a different way.- The description of
--numberOfParallelVerifiersmisses a). - I'd increase the maximum line length; the right column is quite narrow. I'd also put a newline between different options.
Output of silicon --help:
Silicon 1.1-SNAPSHOT (09888100@(detached))
Usage: Silicon [options] <file>
Options:
--alternativeFunctionVerificationOrder Calculate the order in which
functions are verified and
function axioms become
available in an alternative
way that takes dependencies
between functions through
predicate unfoldings into
account. This is more
complete in some cases (see
Silicon issue #355) but less
complete in others (see test
all/issues/silicon/unofficial007).
--assertionMode <arg>... Determines how assertion
checks are encoded in SMTLIB.
Options are 'pp' (push-pop)
and 'cs' (soft constraints)
(default: cs).
--assertTimeout <arg> Timeout (in ms) per SMT
solver assertion (default: 0,
i.e. no timeout).Ignored when
using the cvc5 prover.
--assumeInjectivityOnInhale Assumes injectivity of the
receiver expression when
inhaling quantified
permissions, instead of
checking it.
--checkTimeout <arg> Timeout (in ms) per SMT
solver check. Solver checks
differ from solver asserts in
that a failing assert always
yields a verification error
whereas a failing check
doesn't, at least not
directly. However, failing
checks might result in
performance degradation, e.g.
when a dead program path is
nevertheless explored, and
indirectly in verification
failures due to
incompletenesses, e.g. when
the held permission amount is
too coarsely
underapproximated (default:
10).Ignored when using the
cvc5 prover.
--conditionalizePermissions Potentially reduces the
number of symbolic execution
paths, by conditionalising
permission expressions. E.g.
rewrite "b ==> acc(x.f, p)"
to "acc(x.f, b ? p :
none)".This is an
experimental feature; report
problems if you observe any.
--counterexample <arg> Return counterexample for
errors. Pass 'native' for
returning the native model
from the backend, 'variables'
for returning a model of all
local Viper variables, or
'mapped' (only available on
Silicon) for returning a
model with Ref variables
resolved to object-like
structures.
--cvc5Exe <arg> cvc5 executable. The
environment variable CVC5_EXE
can also be used to specify
the path of the executable.
--disableCaches Disables various caches in
Silicon's state.
--disableCatchingExceptions Don't catch exceptions (can
be useful for debugging
problems with Silicon)
--disableChunkOrderHeuristics Disable heuristic ordering of
quantified chunks (context:
iterated separating
conjunctions).
--disableHavocHack407 A Viper method call to
___silicon_hack407_havoc_all_R,
where R is a field or
predicate, results in Silicon
havocking all instances of R.
See also Silicon issue #407.
--disableISCTriggers Don't pick triggers for
quantifiers, let the SMT
solver do it (context:
iterated separating
conjunctions).
--disableShortCircuitingEvaluations Disable short-circuiting
evaluation of AND, OR. If
disabled, evaluating e.g., i
> 0 && f(i), will fail if f's
precondition requires i > 0.
--disableSubsumption Don't add assumptions gained
by verifying an assert
statement
--disableTempDirectory Disable the creation of
temporary data (default:
./tmp)
--disableValueMapCaching Disable caching of value maps
(context: iterated separating
conjunctions).
--enableBranchconditionReporting Report branch conditions (can
be useful for assertions that
fail on multiple branches)
--enableMoreCompleteExhale Enable a more complete exhale
version.
--enablePredicateTriggersOnInhale Emit predicate-based function
trigger on each inhale of a
predicate instance (context:
heap-dependent functions).
--excludeMethods <arg> Exclude methods from
verification (default: '').
Is applied after the include
pattern.
--handlePureConjunctsIndividually Handle pure conjunction
individually.Increases
precision of error reporting,
but may slow down
verification.
--includeMethods <arg> Include methods in
verification (default: '*').
Wildcard characters are '?'
and '*'.
-Llogger=level [logger=level]... Set level of certain internal
loggers
--logConfig <arg> Path to config file
specifying SymbExLogger
options
--logLevel <arg> One of the log levels ALL,
TRACE, DEBUG, INFO, WARN,
ERROR, OFF
--mapAxiomatizationFile <arg> Source file with map
axiomatisation. If omitted,
built-in one is used.
--maxHeuristicsDepth <arg> Maximal number of nested
heuristics applications
(default: 3)
--multisetAxiomatizationFile <arg> Source file with multiset
axiomatisation. If omitted,
built-in one is used.
--numberOfErrorsToReport <arg> Number of errors per member
before the verifier stops. If
this number is set to 0, all
errors are reported.
--numberOfParallelVerifiers <arg> Number of verifiers run in
parallel. This number plus
one is the number of provers
run in parallel (default: 8
--plugin <arg> Load plugin(s) with given
class name(s). Several
plugins can be separated by
':'. The fully qualified
class name of the plugin
should be specified.
--printMethodCFGs Print a DOT (Graphviz)
representation of the CFG of
each method to verify to a
file
'<tempDirectory>/<methodName>.dot'.
--printTranslatedProgram Print the final program that
is going to be verified to
stdout.
--prover <arg> One of the provers Z3, cvc5.
(default: Z3).
--proverArgs <arg> Command-line arguments which
should be forwarded to the
prover. The expected format
is "<opt> <opt> ... <opt>",
excluding the quotation
marks.
--proverConfigArgs <arg>... Configuration options which
should be forwarded to the
prover. The expected format
is "<key>=<val> <key>=<val>
... <key>=<val>", excluding
the quotation marks. The
configuration options given
here will override those from
Silicon's prover preamble.
--proverEnableResourceBounds Use prover's resource bounds
instead of timeouts
--proverLogFile <arg> Log file containing the
interaction with the prover,
extension smt2 will be
appended. (default:
<tempDirectory>/logfile.smt2)
--proverRandomizeSeeds Set various random seeds of
the prover to random values
--proverResourcesPerMillisecond <arg> Prover resources per
milliseconds. Is used to
convert timeouts to resource
bounds.
--proverSaturationTimeout <arg> Timeout (in ms) used for the
prover's state saturation
calls (default: 100). A
timeout of 0 disables all
saturation checks.Note that
for the cvc5 prover, state
saturation calls can either
be disabled (weights or base
timeout of 0) or forced with
no timeout (positive weight
and base timeout).
--proverSaturationTimeoutWeights <arg>... Weights used to compute the
effective timeout for the
prover's state saturation
calls, which are made at
various points during a
symbolic execution. The
effective timeouts for a
particular saturation call is
computed by multiplying the
corresponding weight with the
base timeout for saturation
calls. Defaults to the
following weights:
after
program preamble: 1.0
after inhaling contracts:
0.5
after unfold: 0.4
after inhale: 0.2
before
repeated prover queries:
0.02
Weights must be
non-negative, a weight of 0
disables the corresponding
saturation call and a minimal
timeout of 10ms is
enforced.Note that for the
cvc5 prover, state saturation
calls can either be disabled
(weights or base timeout of
0) or forced with no timeout
(positive weight and base
timeout).
--qpSplitTimeout <arg> Timeout (in ms) used by QP's
split algorithm when 1)
checking if a chunk holds no
further permissions, and 2)
checking if sufficiently many
permissions have already been
split off.
--recursivePredicateUnfoldings <arg> Evaluate n unfolding
expressions in the body of
predicates that
(transitively) unfold other
instances of themselves
(default: 1)
--sequenceAxiomatizationFile <arg> Source file with sequence
axiomatisation. If omitted,
built-in one is used.
--setAxiomatizationFile <arg> Source file with set
axiomatisation. If omitted,
built-in one is used.
--stateConsolidationMode <arg> One of the following modes:
0: Minimal work, many
incompletenesses
1: Most
work, fewest
incompletenesses
2: Similar
to 1, but less eager
3:
Less eager and less complete
than 1
4: Intended for use
with --moreCompleteExhale
--tempDirectory <arg> Path to which all temporary
data will be written
(default: ./tmp)
--timeout <arg> Time out after approx. n
seconds. The timeout is for
the whole verification, not
per method or proof
obligation (default: 0, i.e.
no timeout).
--z3Args <arg> Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverArgs' instead...
Command-line arguments which
should be forwarded to Z3.
The expected format is "<opt>
<opt> ... <opt>", excluding
the quotation marks.
--z3ConfigArgs <arg>... Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverConfigArgs' instead...
Configuration options which
should be forwarded to Z3.
The expected format is
"<key>=<val> <key>=<val> ...
<key>=<val>", excluding the
quotation marks. The
configuration options given
here will override those from
Silicon's Z3 preamble.
--z3EnableResourceBounds Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverEnableResourceBounds'
instead... Use Z3's resource
bounds instead of timeouts
--z3Exe <arg> Z3 executable. The
environment variable Z3_EXE
can also be used to specify
the path of the executable.
--z3LogFile <arg> Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverLogFile' instead...
Log file containing the
interaction with the prover,
extension smt2 will be
appended. (default:
<tempDirectory>/logfile.smt2).
--z3RandomizeSeeds Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverRandomizeSeeds'
instead... Set various Z3
random seeds to random values
--z3ResourcesPerMillisecond <arg> Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverResourcesPerMillisecond'
instead... Z3 resources per
milliseconds. Is used to
convert timeouts to resource
bounds.
--z3SaturationTimeout <arg> Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverSaturationTimeout'
instead... Timeout (in ms)
used for Z3 state saturation
calls (default: 100). A
timeout of 0 disables all
saturation checks.
--z3SaturationTimeoutWeights <arg>... Warning: This option is
deprecated due to
standardization in option
naming. Please use
'proverSaturationTimeoutWeights'
instead... Weights used to
compute the effective timeout
for Z3 state saturation
calls, which are made at
various points during a
symbolic execution. The
effective timeouts for a
particular saturation call is
computed by multiplying the
corresponding weight with the
base timeout for saturation
calls. Defaults to the
following weights:
after
program preamble: 1.0
after inhaling contracts:
0.5
after unfold: 0.4
after inhale: 0.2
before
repeated Z3 queries:
0.02
Weights must be
non-negative, a weight of 0
disables the corresponding
saturation call and a minimal
timeout of 10ms is enforced.
-h, --help Show help message
trailing arguments:
file (required) The file to verify.
Verification aborted exceptionally: org.rogach.scallop.exceptions.RequiredOptionNotFound: Required option 'file' not found
org.rogach.scallop.exceptions.RequiredOptionNotFound: Required option 'file' not found
at org.rogach.scallop.Scallop.parseRest$1(Scallop.scala:127)
at org.rogach.scallop.Scallop.goParseRest$1(Scallop.scala:153)
at org.rogach.scallop.Scallop.goParseRest$1(Scallop.scala:141)
at org.rogach.scallop.Scallop.parse(Scallop.scala:197)
at org.rogach.scallop.Scallop.parse(Scallop.scala:85)
at org.rogach.scallop.Scallop.parsed$lzycompute(Scallop.scala:291)
at org.rogach.scallop.Scallop.parsed(Scallop.scala:291)
at org.rogach.scallop.Scallop.$anonfun$get$7(Scallop.scala:435)
at scala.Option.map(Option.scala:242)
at org.rogach.scallop.Scallop.get(Scallop.scala:434)
at org.rogach.scallop.ScallopConfBase$$anon$1.$anonfun$fn$1(ScallopConfBase.scala:202)
at scala.Function1.$anonfun$andThen$1(Function1.scala:85)
at org.rogach.scallop.ScallopOption.value$lzycompute(ScallopOption.scala:25)
at org.rogach.scallop.ScallopOption.value(ScallopOption.scala:25)
at org.rogach.scallop.ScallopOption.foreach(ScallopOption.scala:90)
at viper.silicon.Silicon.setLogLevelsFromConfig(Silicon.scala:321)
at viper.silicon.Silicon.start(Silicon.scala:129)
at viper.silicon.SiliconFrontend.configureVerifier(Silicon.scala:355)
at viper.silicon.SiliconFrontend.configureVerifier(Silicon.scala:336)
at viper.silver.frontend.SilFrontend.parseCommandLine(SilFrontend.scala:229)
at viper.silver.frontend.SilFrontend.parseCommandLine$(SilFrontend.scala:228)
at viper.silicon.SiliconFrontend.parseCommandLine(Silicon.scala:336)
at viper.silver.frontend.SilFrontend.prepare(SilFrontend.scala:118)
at viper.silver.frontend.SilFrontend.prepare$(SilFrontend.scala:113)
at viper.silicon.SiliconFrontend.prepare(Silicon.scala:336)
at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:153)
at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:147)
at viper.silicon.SiliconFrontend.execute(Silicon.scala:336)
at viper.silicon.SiliconRunner$.main(Silicon.scala:381)
at viper.silicon.SiliconRunner.main(Silicon.scala)
fpoli commented
Also, the default of assertionMode is wrong. It's push-pop in the code.
marcoeilers commented
-Llogger=level is indented in a different way.
I agree it looks weird, but that seems to be a feature of the library we're using for this kind of option, and I don't really want to change the type of option in case that breaks anyone's code. I've addressed the rest (except for the newline between options, which I also haven't found a way to do with the current library).
fpoli commented
Feel free to close this issue when the exeption is fixed. The other stuff might be subjective.