moves promises and theories into the core-theory plugin (BinaryAnalys…

…isPlatform#1402) Adds a new core-theory plugin and moves the `name-of-possible-names` rule into it. But what is more important, moves the syntax theory from Primus Lisp to this plugin and disables it by default. Right now this theory is useful only for debugging and it slows down bap a bit so it is better to keep it disabled. You can enable it with `--core-theory-syntax` (or `--core-theory-debug`). To enable it permanently, add a file to `~/.config/bap` folder with the following contents, ``` core-theory-syntax=true ```
thestr4ng3r · Jan 13, 2022 · fb4ed64 · fb4ed64
1 parent 6bdffa6
commit fb4ed64
Show file tree

Hide file tree

Showing 7 changed files with 540 additions and 500 deletions.
diff --git a/lib/bap_core_theory/bap_core_theory_program.ml b/lib/bap_core_theory/bap_core_theory_program.ml
@@ -279,14 +279,6 @@ module Label = struct
     | None -> Knowledge.return Target.unknown
     | Some unit -> Knowledge.collect Unit.target unit
 
-  let _decide_name_from_possible_name : unit =
-    Knowledge.Rule.(declare ~package "name-of-possible-names" |>
-                    require possible_name |>
-                    provide name |>
-                    comment "resolves possible name");
-    Knowledge.promise name @@
-    Knowledge.resolve possible_name
-
   include (val Knowledge.Object.derive cls)
 end
 

diff --git a/oasis/core-theory b/oasis/core-theory
@@ -24,3 +24,13 @@ Library bap_core_theory
         Bap_core_theory_target,
         Bap_core_theory_value,
         Bap_core_theory_var
+
+Library core_theory_plugin
+  Build$:           flag(everything) || flag(core_theory)
+  Path:             plugins/core_theory
+  FindlibName:      bap-plugin-core_theory
+  BuildDepends:     bap-knowledge, bap-core-theory, bap-main,
+                    bitvec, core_kernel, monads, ppx_bap
+  InternalModules:  Core_theory_main
+  XMETADescription: provides core theory rules
+  XMETAExtraLines:  tags="core-theory, semantics"