draperlaboratory / cbat_tools

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

Failed to build `value_set` #301

Closed xudon9 closed 3 years ago

xudon9 commented 3 years ago

The following line declared equal to be t -> t -> bool: https://github.com/draperlaboratory/cbat_tools/blob/4ff5ae9bdfbfa85947f1bcb3e5141309fffb39ae/vsa/value_set/lib/src/cbat_lattice_intf.ml#L34

For the definition, https://github.com/draperlaboratory/cbat_tools/blob/4ff5ae9bdfbfa85947f1bcb3e5141309fffb39ae/vsa/value_set/lib/src/cbat_lattice_intf.ml#L142 OCaml think the (=) is Core_kernel.Int.t -> Core_kernel.Int.t -> bool (even when we annotate it with let equal (a:t) (b:t) = a = b).

Changing the definition to let equal a b = Bool.(a = b) solves the problem here, but brings more similar typing errors.


Tested with 2 environments,

File "src/cbat_lattice_intf.ml", lines 133-147, characters 6-3:
133 | ......struct
134 | 
135 |   type t = bool[@@deriving bin_io, sexp, compare]
136 | 
137 |   let top = true
...
144 | 
145 |   let pp ppf (b : t) = Format.fprintf ppf (if b then "top" else "bottom")
146 | 
147 | 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 '/home/opam/cbat_tools/vsa/value_set/lib'
Makefile:10: recipe for target 'install' failed
make: *** [install] Error 2
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.

xudon9 commented 3 years ago

Thank you Chris!

I managed to build it with BAP 2.2.0. I created a PR to show the changes.

Be warned that they're a bit hacky though. :P

zhouxuan009 commented 3 years ago

Seems that we are looking at the same problem lol. Your PR is cool. Coincidentally we have the same solution. The issue I raised is #298, which also mentioned a runtime problem which can be met. Probably we can communicate about it if you are interested @whst

xudon9 commented 3 years ago

Ah yes, turned out passing all the unit tests doesn't mean it works. I encountered exactly the same problem now :(

ccasin commented 3 years ago

Thanks @whst and @zhouxuan009! I've merged PR #303 and it builds now. Please feel free to open a new issue documenting the broken behavior, and we'll take a look.