saw abort override

[I-am-Batman]

When applying an override, I get this message a number of times. However, since the proof eventually succeeds, it seems like the override is in fact being applied -- removing the overrides makes saw spin for longer than I care to wait)

Are the overrides being applied? Maybe only sometimes? If not, how can I tell what the issue is? debugging flags maybe?

...
Abort due to false assumption:
  no override specification applies for add_round_key
  in overrideBranches at verify_aes/aes_cipher.saw:183:22
  When calling overrideBranches
  When calling add_round_key
  In aes_cipher at internal
...
Symbolic simulation completed with side conditions.
Proof succeeded! aes_cipher

[WeeknightMVP]

As of 7c58270, saw-script/examples/llvm/dotprod_struct-crucible.saw behaves likewise:

> saw dotprod_struct-crucible.saw
Loading file "saw-script/examples/llvm/dotprod_struct-crucible.saw"
Proof succeeded! dotprod_struct
Registering override for `dotprod_struct`
Abort due to false assumption:
  no override specification applies for dotprod_struct
  in overrideBranches at saw-script/examples/llvm/dotprod_struct-crucible.saw:30:1
  When calling overrideBranches
  When calling dotprod_struct
  In dotprod_wrap at internal
Symbolic simulation completed with side conditions.
Proof succeeded! dotprod_wrap

[robdockins]

This is entirely a UI problem. The SAW frontend is reporting path abort conditions that occur even in cases where we can later prove that the speculative branch of execution is impossible. This new message is occurring because we recently reengineered the way that overrides are selected.

The fix for this is to avoid reporting spurious abort messages. It shouldn't be hard; I'll look into it.

[robdockins]

As a workaround, you can silence these options by lowering the "simulator" verbosity to 0 (using option -d 0). I've increased the required crucible verbosity to see these messages to 3, so at some point when that update gets pulled into saw, these messages will be silenced unless requested by a high verbosity setting.

[robdockins]

The change regarding verbosity levels has now propagated into master saw-script.