Skip to content

Commit

Permalink
Correct & clarify --per_path_timeout documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
pschanely committed Feb 28, 2024
1 parent e4d1e75 commit 3d4eeac
Show file tree
Hide file tree
Showing 5 changed files with 90 additions and 75 deletions.
79 changes: 41 additions & 38 deletions crosshair/main.py
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,7 @@
from crosshair.path_search import OptimizationKind, path_search
from crosshair.pure_importer import prefer_pure_python_imports
from crosshair.register_contract import REGISTERED_CONTRACTS
from crosshair.statespace import NotDeterministic, context_statespace
from crosshair.tracers import NoTracing
from crosshair.statespace import NotDeterministic
from crosshair.util import (
ErrorDuringImport,
add_to_pypath,
Expand Down Expand Up @@ -168,11 +167,11 @@ def command_line_parser() -> argparse.ArgumentParser:
formatter_class=argparse.RawTextHelpFormatter,
description=textwrap.dedent(
"""\
The search command finds arguments for a function that causes it to complete without
error.
The search command finds arguments for a function that causes it to
complete without error.
Results (if any) are written to stdout in the form of a repr'd dictionary, mapping
argument names to values.
Results (if any) are written to stdout in the form of a repr'd
dictionary, mapping argument names to values.
"""
),
)
Expand All @@ -191,13 +190,13 @@ def command_line_parser() -> argparse.ArgumentParser:
help=textwrap.dedent(
"""\
Controls what kind of arguments are produced.
Optimization effectiveness will vary wildly depnding on the nature of the
function.
simplify : [default] Attempt to minimize the size (in characters) of the
arguments.
Optimization effectiveness will vary wildly depnding on the nature of
the function.
simplify : [default] Attempt to minimize the size
(in characters) of the arguments.
none : Output the first set of arguments found.
minimize_int : Attempt to minimize an integer returned by the function.
Negative return values are ignored.
minimize_int : Attempt to minimize an integer returned by the
function. Negative return values are ignored.
"""
),
)
Expand All @@ -217,11 +216,11 @@ def command_line_parser() -> argparse.ArgumentParser:
type=str,
help=textwrap.dedent(
"""\
The (fully-qualified) name of a function for formatting produced arguments.
If specified, crosshair will call this function instead of repr() when printing
arguments to stdout.
Your formatting function will be pased an `inspect.BoundArguments` instance.
It should return a string.
The (fully-qualified) name of a function for formatting produced
arguments. If specified, crosshair will call this function instead of
repr() when printing arguments to stdout.
Your formatting function will be pased an `inspect.BoundArguments`
instance. It should return a string.
"""
),
)
Expand Down Expand Up @@ -280,8 +279,8 @@ def command_line_parser() -> argparse.ArgumentParser:
help="Generate inputs for a function, attempting to exercise different code paths",
description=textwrap.dedent(
"""\
Generates inputs to a function, hopefully getting good line, branch, and path
coverage.
Generates inputs to a function, hopefully getting good line, branch,
and path coverage.
See https://crosshair.readthedocs.io/en/latest/cover.html
"""
),
Expand Down Expand Up @@ -310,9 +309,10 @@ def command_line_parser() -> argparse.ArgumentParser:
help=textwrap.dedent(
"""\
Determines how to output examples.
eval_expression : [default] Output examples as expressions, suitable for
eval()
arg_dictionary : Output arguments as repr'd, ordered dictionaries
eval_expression : [default] Output examples as expressions,
suitable for eval()
arg_dictionary : Output arguments as repr'd, ordered
dictionaries
pytest : Output examples as stub pytest tests
argument_dictionary : Deprecated
"""
Expand All @@ -327,14 +327,15 @@ def command_line_parser() -> argparse.ArgumentParser:
help=textwrap.dedent(
"""\
Determines what kind of coverage to achieve.
opcode : [default] Cover as many opcodes of the function as possible.
This is similar to "branch" coverage.
opcode : [default] Cover as many opcodes of the function as
possible. This is similar to "branch" coverage.
path : Cover any possible execution path.
There will usually be an infinite number of paths (e.g. loops are
effectively unrolled). Use max_uninteresting_iterations and/or
per_condition_timeout to bound results.
Many path decisions are internal to CrossHair, so you may see more
duplicative-ness in the output than you'd expect.
There will usually be an infinite number of paths (e.g.
loops are effectively unrolled). Use
max_uninteresting_iterations and/or per_condition_timeout
to bound results.
Many path decisions are internal to CrossHair, so you may
see more duplicative-ness in the output than you'd expect.
"""
),
)
Expand All @@ -346,14 +347,15 @@ def command_line_parser() -> argparse.ArgumentParser:
"""\
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations, unless --per_condition_timeout is set)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
of the code under analysis.
Use a small integer (3-5) for fast but weak analysis.
Values in the hundreds or thousands may be appropriate if you intend to
run CrossHair for hours.
Values in the hundreds or thousands may be appropriate if you
intend to run CrossHair for hours.
"""
),
)
Expand All @@ -366,11 +368,14 @@ def command_line_parser() -> argparse.ArgumentParser:
help=textwrap.dedent(
"""\
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds
equal to `--max_uninteresting_iterations`, unless it is
explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
"""
),
)
Expand Down Expand Up @@ -894,15 +899,13 @@ def unwalled_main(cmd_args: Union[List[str], argparse.Namespace]) -> int:
defaults = DEFAULT_OPTIONS.overlay(
AnalysisOptionSet(
per_path_timeout=30.0, # mostly, we don't want to time out paths
max_uninteresting_iterations=5,
)
)
return diffbehavior(args, defaults.overlay(options), sys.stdout, sys.stderr)
elif args.action == "cover":
defaults = DEFAULT_OPTIONS.overlay(
AnalysisOptionSet(
per_path_timeout=30.0, # mostly, we don't want to time out paths
max_uninteresting_iterations=5,
)
)
return cover(args, defaults.overlay(options), sys.stdout, sys.stderr)
Expand Down
6 changes: 2 additions & 4 deletions crosshair/options.py
Original file line number Diff line number Diff line change
Expand Up @@ -135,10 +135,8 @@ class AnalysisOptions:

def get_max_uninteresting_iterations(self):
max_uninteresting_iterations = self.max_uninteresting_iterations
if (
max_uninteresting_iterations == sys.maxsize
and (not math.isfinite(self.per_condition_timeout))
and (not math.isfinite(self.per_path_timeout))
if max_uninteresting_iterations == sys.maxsize and (
not math.isfinite(self.per_condition_timeout)
):
return 5
elif max_uninteresting_iterations == 0:
Expand Down
18 changes: 11 additions & 7 deletions doc/source/contracts.rst
Original file line number Diff line number Diff line change
Expand Up @@ -176,21 +176,25 @@ It is more customizable than ``watch`` and produces machine-readable output.
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations, unless --per_condition_timeout is set)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
of the code under analysis.
Use a small integer (3-5) for fast but weak analysis.
Values in the hundreds or thousands may be appropriate if you intend to
run CrossHair for hours.
Values in the hundreds or thousands may be appropriate if you
intend to run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds
equal to `--max_uninteresting_iterations`, unless it is
explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
--analysis_kind KIND Kind of contract to check.
Expand Down
44 changes: 25 additions & 19 deletions doc/source/cover.rst
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,8 @@ How do I try it?
[--per_condition_timeout FLOAT]
TARGET [TARGET ...]
Generates inputs to a function, hopefully getting good line, branch, and path
coverage.
Generates inputs to a function, hopefully getting good line, branch,
and path coverage.
See https://crosshair.readthedocs.io/en/latest/cover.html
positional arguments:
Expand All @@ -88,38 +88,44 @@ How do I try it?
Plugin file(s) you wish to use during the current execution
--example_output_format FORMAT
Determines how to output examples.
eval_expression : [default] Output examples as expressions, suitable for
eval()
arg_dictionary : Output arguments as repr'd, ordered dictionaries
eval_expression : [default] Output examples as expressions,
suitable for eval()
arg_dictionary : Output arguments as repr'd, ordered
dictionaries
pytest : Output examples as stub pytest tests
argument_dictionary : Deprecated
--coverage_type TYPE Determines what kind of coverage to achieve.
opcode : [default] Cover as many opcodes of the function as possible.
This is similar to "branch" coverage.
opcode : [default] Cover as many opcodes of the function as
possible. This is similar to "branch" coverage.
path : Cover any possible execution path.
There will usually be an infinite number of paths (e.g. loops are
effectively unrolled). Use max_uninteresting_iterations and/or
per_condition_timeout to bound results.
Many path decisions are internal to CrossHair, so you may see more
duplicative-ness in the output than you'd expect.
There will usually be an infinite number of paths (e.g.
loops are effectively unrolled). Use
max_uninteresting_iterations and/or per_condition_timeout
to bound results.
Many path decisions are internal to CrossHair, so you may
see more duplicative-ness in the output than you'd expect.
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations, unless --per_condition_timeout is set)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
of the code under analysis.
Use a small integer (3-5) for fast but weak analysis.
Values in the hundreds or thousands may be appropriate if you intend to
run CrossHair for hours.
Values in the hundreds or thousands may be appropriate if you
intend to run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds
equal to `--max_uninteresting_iterations`, unless it is
explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
Expand Down
18 changes: 11 additions & 7 deletions doc/source/diff_behavior.rst
Original file line number Diff line number Diff line change
Expand Up @@ -66,21 +66,25 @@ How do I try it?
--max_uninteresting_iterations MAX_UNINTERESTING_ITERATIONS
Maximum number of consecutive iterations to run without making
significant progress in exploring the codebase.
(by default, 5 iterations, unless --per_condition_timeout is set)
This option can be more useful than --per_condition_timeout
because the amount of time invested will scale with the complexity
of the code under analysis.
Use a small integer (3-5) for fast but weak analysis.
Values in the hundreds or thousands may be appropriate if you intend to
run CrossHair for hours.
Values in the hundreds or thousands may be appropriate if you
intend to run CrossHair for hours.
--per_path_timeout FLOAT
Maximum seconds to spend checking one execution path.
If unspecified, CrossHair will timeout each path:
1. At the square root of `--per_condition_timeout`, if specified.
2. Otherwise, at a number of seconds equal to
`--max_uninteresting_iterations`, if specified.
3. Otherwise, there will be no per-path timeout.
If unspecified:
1. CrossHair will timeout each path at the square root of
`--per_condition_timeout`, if specified.
3. Otherwise, it will timeout each path at a number of seconds
equal to `--max_uninteresting_iterations`, unless it is
explicitly set to zero.
(NOTE: `--max_uninteresting_iterations` is 5 by default)
2. Otherwise, it will not use any per-path timeout.
--per_condition_timeout FLOAT
Maximum seconds to spend checking execution paths for one condition
Expand Down

0 comments on commit 3d4eeac

Please sign in to comment.