search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

value set build problem #298

Closed zhouxuan009 closed 3 years ago

zhouxuan009 commented 3 years ago

Hi, I entered make under the folder cbat_tools/vsa/value_set, then the make error message appeared in the command line as below

make -C lib install.local
make[1]: Entering directory '/open/zhouxuan/cbat_tools/vsa/value_set/lib'
dune build -p cbat_value_set
      ocamlc src/.cbat_value_set.objs/byte/cbat_value_set__Cbat_lattice_intf.{cmi,cmo,cmt} (exit 2)
(cd _build/default && /home/zhouxuan/.opam/4.09.0/bin/ocamlc.opt -w -40 -g -bin-annot -I src/.cbat_value_set.objs/byte -I /home/zhouxuan/.opam/4.09.0/lib/angstrom -I /home/zhouxuan/.opam/4.09.0/lib/bap -I /home/zhouxuan/.opam/4.09.0/lib/bap-bundle -I /home/zhouxuan/.opam/4.09.0/lib/bap-core-theory -I /home/zhouxuan/.opam/4.09.0/lib/bap-future -I /home/zhouxuan/.opam/4.09.0/lib/bap-knowledge -I /home/zhouxuan/.opam/4.09.0/lib/bap-main -I /home/zhouxuan/.opam/4.09.0/lib/bap-plugins -I /home/zhouxuan/.opam/4.09.0/lib/bap-recipe -I /home/zhouxuan/.opam/4.09.0/lib/bap-relation -I /home/zhouxuan/.opam/4.09.0/lib/base -I /home/zhouxuan/.opam/4.09.0/lib/base/base_internalhash_types -I /home/zhouxuan/.opam/4.09.0/lib/base/caml -I /home/zhouxuan/.opam/4.09.0/lib/base/md5 -I /home/zhouxuan/.opam/4.09.0/lib/base/shadow_stdlib -I /home/zhouxuan/.opam/4.09.0/lib/base_bigstring -I /home/zhouxuan/.opam/4.09.0/lib/base_quickcheck -I /home/zhouxuan/.opam/4.09.0/lib/bigarray-compat -I /home/zhouxuan/.opam/4.09.0/lib/bigstringaf -I /home/zhouxuan/.opam/4.09.0/lib/bin_prot -I /home/zhouxuan/.opam/4.09.0/lib/bin_prot/shape -I /home/zhouxuan/.opam/4.09.0/lib/bitvec -I /home/zhouxuan/.opam/4.09.0/lib/bitvec-binprot -I /home/zhouxuan/.opam/4.09.0/lib/bitvec-order -I /home/zhouxuan/.opam/4.09.0/lib/bitvec-sexp -I /home/zhouxuan/.opam/4.09.0/lib/bytes -I /home/zhouxuan/.opam/4.09.0/lib/camlzip -I /home/zhouxuan/.opam/4.09.0/lib/cmdliner -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel/base_for_tests -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel/caml_unix -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel/pairing_heap -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel/rope -I /home/zhouxuan/.opam/4.09.0/lib/core_kernel/tuple_pool -I /home/zhouxuan/.opam/4.09.0/lib/fieldslib -I /home/zhouxuan/.opam/4.09.0/lib/fileutils -I /home/zhouxuan/.opam/4.09.0/lib/findlib -I /home/zhouxuan/.opam/4.09.0/lib/graphlib -I /home/zhouxuan/.opam/4.09.0/lib/jane-street-headers -I /home/zhouxuan/.opam/4.09.0/lib/mmap -I /home/zhouxuan/.opam/4.09.0/lib/monads -I /home/zhouxuan/.opam/4.09.0/lib/ocaml-compiler-libs/common -I /home/zhouxuan/.opam/4.09.0/lib/ocaml-compiler-libs/shadow -I /home/zhouxuan/.opam/4.09.0/lib/ocaml-migrate-parsetree -I /home/zhouxuan/.opam/4.09.0/lib/ocaml/compiler-libs -I /home/zhouxuan/.opam/4.09.0/lib/ocamlgraph -I /home/zhouxuan/.opam/4.09.0/lib/ogre -I /home/zhouxuan/.opam/4.09.0/lib/parsexp -I /home/zhouxuan/.opam/4.09.0/lib/ppx_assert -I /home/zhouxuan/.opam/4.09.0/lib/ppx_assert/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_bap -I /home/zhouxuan/.opam/4.09.0/lib/ppx_bench -I /home/zhouxuan/.opam/4.09.0/lib/ppx_bench/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_bin_prot -I /home/zhouxuan/.opam/4.09.0/lib/ppx_bin_prot/shape-expander -I /home/zhouxuan/.opam/4.09.0/lib/ppx_compare -I /home/zhouxuan/.opam/4.09.0/lib/ppx_compare/expander -I /home/zhouxuan/.opam/4.09.0/lib/ppx_compare/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_derivers -I /home/zhouxuan/.opam/4.09.0/lib/ppx_enumerate -I /home/zhouxuan/.opam/4.09.0/lib/ppx_enumerate/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_expect/collector -I /home/zhouxuan/.opam/4.09.0/lib/ppx_expect/common -I /home/zhouxuan/.opam/4.09.0/lib/ppx_expect/config -I /home/zhouxuan/.opam/4.09.0/lib/ppx_expect/config_types -I /home/zhouxuan/.opam/4.09.0/lib/ppx_fields_conv -I /home/zhouxuan/.opam/4.09.0/lib/ppx_hash -I /home/zhouxuan/.opam/4.09.0/lib/ppx_hash/expander -I /home/zhouxuan/.opam/4.09.0/lib/ppx_hash/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_here -I /home/zhouxuan/.opam/4.09.0/lib/ppx_here/expander -I /home/zhouxuan/.opam/4.09.0/lib/ppx_here/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_inline_test/config -I /home/zhouxuan/.opam/4.09.0/lib/ppx_inline_test/libname -I /home/zhouxuan/.opam/4.09.0/lib/ppx_inline_test/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_module_timer/runtime -I /home/zhouxuan/.opam/4.09.0/lib/ppx_optcomp -I /home/zhouxuan/.opam/4.09.0/lib/ppx_sexp_conv -I /home/zhouxuan/.opam/4.09.0/lib/ppx_sexp_conv/expander -I /home/zhouxuan/.opam/4.09.0/lib/ppx_sexp_conv/runtime-lib -I /home/zhouxuan/.opam/4.09.0/lib/ppx_sexp_value -I /home/zhouxuan/.opam/4.09.0/lib/ppx_variants_conv -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib/ast -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib/metaquot_lifters -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib/print_diff -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib/stdppx -I /home/zhouxuan/.opam/4.09.0/lib/ppxlib/traverse_builtins -I /home/zhouxuan/.opam/4.09.0/lib/regular -I /home/zhouxuan/.opam/4.09.0/lib/result -I /home/zhouxuan/.opam/4.09.0/lib/sexplib -I /home/zhouxuan/.opam/4.09.0/lib/sexplib0 -I /home/zhouxuan/.opam/4.09.0/lib/splittable_random -I /home/zhouxuan/.opam/4.09.0/lib/stdio -I /home/zhouxuan/.opam/4.09.0/lib/stdlib-shims -I /home/zhouxuan/.opam/4.09.0/lib/stringext -I /home/zhouxuan/.opam/4.09.0/lib/time_now -I /home/zhouxuan/.opam/4.09.0/lib/typerep -I /home/zhouxuan/.opam/4.09.0/lib/uri -I /home/zhouxuan/.opam/4.09.0/lib/uuidm -I /home/zhouxuan/.opam/4.09.0/lib/variantslib -I /home/zhouxuan/.opam/4.09.0/lib/zarith -I /home/zhouxuan/.opam/4.09.0/lib/zip -no-alias-deps -open Cbat_value_set -o src/.cbat_value_set.objs/byte/cbat_value_set__Cbat_lattice_intf.cmo -c -impl src/cbat_lattice_intf.pp.ml)
File "src/cbat_lattice_intf.ml", lines 133-148, characters 6-3:
133 | ......struct
134 | 
135 |   type t = bool[@@deriving bin_io, sexp, compare] 
136 | 
137 |   let top = true
...
145 | 
146 |   let pp ppf (b : t) = Format.fprintf ppf (if b then "top" else "bottom")
147 | 
148 | end
Error: Signature mismatch:
       ...
       Values do not match:
         val equal : Core_kernel.Int.t -> Core_kernel.Int.t -> bool
       is not included in
         val equal : t -> t -> bool
       File "src/cbat_lattice_intf.ml", line 34, characters 2-28:
         Expected declaration
       File "src/cbat_lattice_intf.ml", line 142, characters 6-11:
         Actual declaration
Makefile:11: recipe for target 'build' failed
make[1]: *** [build] Error 1
make[1]: Leaving directory '/open/zhouxuan/cbat_tools/vsa/value_set/lib'
Makefile:10: recipe for target 'install' failed
make: *** [install] Error 2

And I can't find where the bug is

Below are some dependencies information on my PC

(base) ➜  value_set git:(master) ✗ bap --version
2.2.0
(base) ➜  value_set git:(master) ✗ 
(base) ➜  value_set git:(master) ✗ ocamlfind query core
/home/zhouxuan/.opam/4.09.0/lib/core
(base) ➜  value_set git:(master) ✗ ocamlfind query ppx_deriving
/home/zhouxuan/.opam/4.09.0/lib/ppx_deriving
(base) ➜  value_set git:(master) ✗ ocamlfind query oUnit
/home/zhouxuan/.opam/4.09.0/lib/oUnit
(base) ➜  value_set git:(master) ✗ opam show ounit

<><> ounit: information on all versions <><><><><><><><><><><><><><><><><><><><>
name                   ounit
all-installed-versions 2.2.4 [4.09.0]
all-versions           1.1.2  2.0.0  2.0.5  2.0.6  2.0.7  2.0.8  2.1.2  2.2.0
                       2.2.1  2.2.2  2.2.3  2.2.4

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version       2.2.4
repository    default
url.src:      "https://github.com/gildor478/ounit/releases/download/v2.2.4/ounit-v2.2.4.tbz"
url.checksum:
          "sha256=b5c069a5d957220ca0669e945f1e81e6b6db9622766d860913e136e1168e3345"
          "sha512=d69dc501a360c31f7854322b5e2c2abcb1e43890737e1cc00c167ee104d5dee471b6b8d8186f8044b0482c91a8f15210a25d833a1e03ed7baabfba923815962f"
homepage:     "https://github.com/gildor478/ounit"
bug-reports:  "https://github.com/gildor478/ounit/issues"
dev-repo:     "git+https://github.com/gildor478/ounit.git"
authors:      "Maas-Maarten Zeeman" "Sylvain Le Gall"
maintainer:   "Sylvain Le Gall <sylvaini+ocaml@le-gall.net>"
depends:      "ocamlfind" {build} "ounit2" {= version}
synopsis      This is a transition package, ounit is now ounit2
description   More details for the transition:
              https://github.com/gildor478/ounit#transition-to-ounit2
(base) ➜  value_set git:(master) ✗ dune --version
2.8.2

Thanks a lot !

ccasin commented 3 years ago

Sorry! We are aware the value_set plugin does not compile with BAP 2.x - it was built for BAP 1. Our main work is on the wp plugin in this repo, these days, but we hope to find time to revisit the value set analysis soon. I will update the readme to reflect the fact that value_set is known not to work.

zhouxuan009 commented 3 years ago

Thanks ! I will take a try with BAP 1 for VSA.

As to BAP2.x for VSA, I have fixed such build error. That's because the comparasion operators make the operands inferred as Integers. Replacing comparasion operators as Module.compare can solve such issue.

After the plugin is built successfully, it still raise an error at runtime

The pass "value-set" failed with:
source tid does not represent block

I found that the error is triggered because the cfg of subroutine passed to the fixpoint function has @start-pseudo-node and @exit-pseudo-node. And line#391 in vsa/value_set/lib/src/cbat_vsa.ml Program.lookup blk_t ctx source don't recognize the pseudo node as basic blocks. I am trying to fix this error

ccasin commented 3 years ago

Fixed by #303 . Thanks!