Using certain registers in the correctness property gives a Z3 error.

[philzook58]

If you modify the property in resources/exe/simple/config.json to use R1

{
  "func": "main",
  "property" : "(assert (= (bvadd R1_mod #x00000002) R0_orig))",
  "patches" : [
    {"patch-name" : "ret-3",
     "patch-code" : "(var-decls retvar)
                     (set retvar 3)
                     fallthrough",
     "patch-point" : "0x3c8",
     "patch-size" : 4}
  ]
}

The verifier crashes with

=== Starting Verifier ===================================================
    Loading patched exe...
    Beginning weakest-precondition analysis...
Uncaught exception:

  Z3.Error("(error \"line 1 column 17: unknown constant R1_mod\")\n")

Raised by primitive operation at file "../src/api/ml/z3.ml", line 2005, characters 6-91
Called from file "src/z3_utils.ml", line 50, characters 13-120
Called from file "src/compare.ml", line 207, characters 4-44
Called from file "src/compare.ml", line 127, characters 12-79
Called from file "list.ml", line 121, characters 24-34
Called from file "src/list0.ml" (inlined), line 21, characters 22-52
Called from file "src/compare.ml", line 124, characters 4-462
Called from file "src/compare.ml", line 152, characters 4-99
Called from file "src/verifier.ml", line 55, characters 30-155
Called from file "src/verifier.ml", line 110, characters 15-51
Called from file "lib/monads/monads_monad.ml", line 1034, characters 60-63
Called from file "lib/monads/monads_monad.ml" (inlined), line 1029, characters 29-34
Called from file "lib/monads/monads_monad.ml", line 1034, characters 38-42
Called from file "lib/monads/monads_monad.ml" (inlined), line 1029, characters 29-34
Called from file "lib/monads/monads_monad.ml", line 1034, characters 38-42
Called from file "lib/monads/monads_monad.ml" (inlined), line 1029, characters 29-34
Called from file "lib/monads/monads_monad.ml", line 1044, characters 21-27
Called from file "lib/knowledge/bap_knowledge.ml", line 2973, characters 10-45
Called from file "src/pipeline.ml", line 63, characters 15-61
Called from file "vibes.ml", line 100, characters 21-50
Called from file "cmdliner_term.ml", line 25, characters 19-24
Called from file "cmdliner_term.ml", line 23, characters 12-19
Called from file "cmdliner.ml", line 117, characters 32-39
Called from file "cmdliner.ml", line 147, characters 18-36
Called from file "cmdliner.ml", line 265, characters 22-48
Called from file "lib/bap_main/bap_main.ml", line 1054, characters 10-99
Called from file "lib/bap_main/bap_main.ml", line 1207, characters 15-140
Called from file "src/bap_frontend.ml", line 320, characters 8-127
make: *** [Makefile:39: main.patched] Error 2

It is unclear what is going on. This shouldn't succeed, but it also should not be crashing.

[codyroux]

Found the culprit: it's this line right here: https://github.com/draperlaboratory/VIBES/blob/3b673645c7d3ecf2b18cdfab7cafb6ddc95857b6/bap-vibes/src/verifier.ml#L41

Combined with this behavior from here: https://github.com/draperlaboratory/cbat_tools/blob/5460085f68bc2152d6ef2c341dea1d5df1400e9d/wp/lib/bap_wp/src/precondition.ml#L725

The "correct" behavior (I think) is to grab the target from the KB, and match against its name to generate the correct argument to Precondition.mk_env. Otherwise I would assume it's a pretty big modification of WP to do the right thing at the source.

@ivg any other suggestions?

[philzook58]

Is this fixed by chloe's arm branch to an acceptable degree or is there more to discuss?

[codyroux]

Yes, feel free to close at will.

On Fri, Mar 5, 2021 at 10:45 AM Philip Zucker @.***> wrote:

Is this fixed by chloe's arm branch to an acceptable degree or is there more to discuss?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/draperlaboratory/VIBES/issues/51#issuecomment-791501691, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA772UDTDKCFQU4CHERDOZLTCD4BXANCNFSM4YBNC5BA .