slicing: do not slice tick statements by default

we now allow counterexamples with no assertions enabled. this is
somewhat unsatisfying as caesar won't pinpoint that it has identified
tick statements as problematic, but it's a short-term solution to the
crashes of issue #37

src/driver.rs

@@ -435,6 +435,7 @@ impl VerifyUnit {
  if !options.no_slice_error {
  selection |= SliceSelection::FAILURE_SELECTION;
  }
+ selection.slice_ticks = options.slice_ticks;
  if options.slice_verify {
  selection |= SliceSelection::VERIFIED_SELECTION;
  }

src/main.rs

@@ -185,6 +185,10 @@ pub struct Options {
  #[structopt(long)]
  pub no_slice_error: bool,
 
+ /// Enable slicing tick/reward statements during slicing for errors.
+ #[structopt(long)]
+ pub slice_ticks: bool,
+
  /// Slice if the program verifies to return a smaller, verifying program.
  /// This is not enabled by default.
  #[structopt(long)]

src/slicing/selection.rs

@@ -148,6 +148,7 @@ pub struct SliceSelection {
  discordant: bool,
  pub in_slice_verify_annotation: bool,
  pub in_slice_error_annotation: bool,
+ pub slice_ticks: bool,
  /// A success message is printed for a statement if it can be removed while
  /// the program still verifies.
  pub(super) success_message: Option<Symbol>,
@@ -168,6 +169,7 @@ impl SliceSelection {
  discordant: false,
  in_slice_verify_annotation: true,
  in_slice_error_annotation: false,
+ slice_ticks: false,
  success_message: None,
  failure_message: None,
  };
@@ -184,6 +186,7 @@ impl SliceSelection {
  discordant: true,
  in_slice_verify_annotation: false,
  in_slice_error_annotation: true,
+ slice_ticks: false,
  success_message: None,
  failure_message: None,
  };
@@ -209,6 +212,7 @@ impl BitOr for SliceSelection {
  || rhs.in_slice_verify_annotation,
  in_slice_error_annotation: self.in_slice_error_annotation
  || rhs.in_slice_error_annotation,
+ slice_ticks: self.slice_ticks || rhs.slice_ticks,
  success_message: self.success_message.or(rhs.success_message),
  failure_message: self.failure_message.or(rhs.failure_message),
  }
@@ -279,6 +283,11 @@ impl SelectionBuilder {
  self.filter.enables(&self.make_selection(effect))
  }
 
+ /// Whether we want to slice tick statements.
+ pub fn should_slice_ticks(&self) -> bool {
+ self.filter.slice_ticks
+ }
+
  /// Create a new slice selection from the current state and the given slice
  /// effect.
  pub fn make_selection(&self, effect: SliceEffect) -> SliceSelection {

src/slicing/solver.rs

@@ -149,7 +149,6 @@ impl<'ctx> SliceSolver<'ctx> {
  slice(
  &mut exists_forall_solver,
  &active_toggle_values,
- false,
  true,
  limits_ref,
  )?;
@@ -180,13 +179,7 @@ impl<'ctx> SliceSolver<'ctx> {
  self.prover.add_assumption(&inactive_formula);
  self.prover.push();
 
- slice(
- &mut self.prover,
- &active_toggle_values,
- true,
- false,
- limits_ref,
- )?;
+ slice(&mut self.prover, &active_toggle_values, false, limits_ref)?;
  let res = self.prover.check_proof();
  let slice_model = if let ProveResult::Counterexample(model) = &res {
  Some(SliceModel::extract_model(
@@ -205,7 +198,6 @@ impl<'ctx> SliceSolver<'ctx> {
 fn slice<'ctx>(
  prover: &mut Prover<'ctx>,
  active_slice_vars: &[Bool<'ctx>],
- at_least_one: bool,
  continue_on_unknown: bool,
  limits_ref: &LimitsRef,
 ) -> Result<(), VerifyError> {
@@ -223,7 +215,18 @@ fn slice<'ctx>(
  prover.add_assumption(&at_most_n_true);
  };
 
- let min_least_bound = if at_least_one { 1 } else { 0 };
+ // TODO: we could have min_least_bound set to 1 if we could conclude for
+ // sure that the program must verify (assuming the axioms are correct) when
+ // all sliceable statements are removed. however, this is sometimes not the
+ // case:
+ // - tick statements are not sliced by default (because slicing them by
+ // default has adverse performance effects on some benchmarks :( )
+ // - if otherwise the program is partially sliced (this is currently not
+ // supported anyways, but we'd like to have this in the future)
+ //
+ // the fix would be to track explicitly whether we can make that assumption
+ // that min_least_bound is 1.
+ let min_least_bound = 0;
  let mut minimize = PartialMinimizer::new(min_least_bound..=slice_vars.len());
 
  let mut first_acceptance = None;

src/slicing/transform.rs

@@ -242,7 +242,7 @@ impl<'tcx> VisitorMut for StmtSliceVisitor<'tcx> {
  let slice_stmt = self.add_slice_stmt(s.span, effect);
  self.mk_top_toggle(expr, *dir, slice_stmt)
  }
- StmtKind::Tick(expr) => {
+ StmtKind::Tick(expr) if self.selector.should_slice_ticks() => {
  let effect = match self.direction {
  Direction::Down => SliceEffect::Concordant,
  Direction::Up => SliceEffect::Discordant,

website/docs/caesar/slicing.md

@@ -446,7 +446,7 @@ For the `co`-statements, the situation is also exactly reversed.
  <td>Discordant</td>
  </tr>
  <tr>
- <td><code>tick</code></td>
+ <td><code>tick</code>*</td>
  <td>Concordant</td>
  <td>Discordant</td>
  </tr>
@@ -457,6 +457,9 @@ For the `co`-statements, the situation is also exactly reversed.
 
 Note that Caesar only tries to slice `(co)assume` and `(co)assert` statements, but not `(co)havoc` nor `(co)validate`.
 
+*: `tick`/`reward` statements are currently not sliced by default.
+This must be enabled with the `--slice-ticks` command-line option.
+
 ## Implementation Details
 
 Caesar's implementation of slicing is a two-stage approach.