Fixed bug in procedure bir_populate_blacklist'

[adrwes]

Fixes bug in procedure bir_populate_blacklist' causing it to throw an exception because equalities between strings and characters are not properly reduced. For example it throws the exception HOL_ERR {message = "", origin_function = "EQT_ELIM", origin_structure = "Drule"} in the following code snippet

open HolKernel Parse boolLib bossLib;
open bslSyntax;
open bir_compositionLib;
open bir_bool_expTheory;

val observe_type = Type `: 'a`
val bdefprog_list = bdefprog_list observe_type

val p_def = bdefprog_list "p" [(blabel_str "entry", [], (bjmp o belabel_str) "0w"),
                               (blabel_str "0w", [], (bjmp o belabel_str) "1w"),
                               (blabel_str "1w", [], (bjmp o belabel_addr64) 2),
                               (blabel_addr64 2, [], (bhalt o bconst64) 0)]

val c = prove(
  “bir_simp_jgmt p bir_exp_true (BL_Label "entry") {BL_Address (Imm64 2w) ; BL_Label "0w" ; BL_Label "1w"} {} bir_exp_true (λl. if (l = BL_Address (Imm64 2w)) then bir_exp_true else bir_exp_false)”,
  cheat)

val c' = bir_populate_blacklist_predset c

[andreaslindner]

Oh that's nice, thanks! I guess we didn't notice this because we never have string labels with the BIR code from the lifter. Maybe you could also add your test case in your initial pull request message as a test case somewhere? This way we would try/check this also with future HolBA commits.

[adrwes]

Maybe you could also add your test case in your initial pull request message as a test case somewhere? This way we would try/check this also with future HolBA commits.

Sure, any suggestion where to put the test case? I'm not familiar with your testing infrastructure.

[andreaslindner]

It could be either under examples or somewhere under src. If you can't fit this with one of the existing examples (under examples), it probably makes sense to add it directly under src/tools/comp. In this case, I would suggest to create a directory examples there and add a file test-{somenamehere}.sml, which is supposed to be a script that raises an unhandled exception if the test fails. (You need to use this naming pattern to let the CI run this test.) You can see an example of such a script in src/shared/examples/test-smtLib.sml.

(Also with the first option, you would add such a script. But in this case you would want to to be related to the example that you add it to. But these are just conventions we follow in the repo.)

[andreaslindner]

The CI didn't ran by itself because this is your first pull request in this repository apparently. I clicked the button now and when we can see that the new test actually runs in the CI, you can merge this pull request. I would assume that Didrik is still fine with it otherwise because the main part didn't change.

[adrwes]

I also ran the tests locally without my fixing commit and my test case failed as expected.

Unfortunately, I cannot merge it since I don't have write access to the repo :)