Type inference #14

Enkelmann · 2019-03-29T13:57:26Z

Contains pass that checks which registers hold pointers and which hold data other than pointers. Also tracks values on the stack. Stack access may get reworked when adding pointer target tracking, i.e. tracking to what heap object/function stack frame a pointer is pointing to.

Oh, also contains some unit tests. :-)

…entary stubs

… type_inference

tbarabosch · 2019-03-29T19:48:11Z

First of all: it already looks very nice! 👍

Some general issues:

please add a recipe for type-inference-printer, would be a really nice to have!
same behavior of dune as stated by you: some changes require now make clean && make
in order to make it work with BAP's opam testing, I had to fix some Map.adds, they are now Map.add_exn (grep for them, but there should be also TODO comments), wrapped up in try-with-blocks. Please have a look at them, just in case that I fixed something. It would be even better if you could preserve the Map.adds and unpack them properly (OK a | Duplicate).
regarding the general Makefile: if you run make test it fails because the C samples havent been built yet. We should build them before. Also there should be a make option: "make samples". This could be done in another story.

tbarabosch · 2019-03-29T19:50:12Z

Once again, let's switch now to BAP testing in this branch, this implies using Core 0.11.0
FYI:
opam repo add bap git://github.com/BinaryAnalysisPlatform/opam-repository#testing
opam update
opam install depext --yes
opam depext --install bap --yes

tbarabosch

Another thing: there is not integration/acceptance test for type inference. Let's discuss whether to try dune for this as well or continue with pytest.

plugins/cwe_type_inference/cwe_type_inference.ml

tbarabosch · 2019-03-29T19:52:41Z

plugins/cwe_type_inference_print/cwe_type_inference_print.ml

@@ -0,0  1,14 @@
+open Bap.Std


I was just wondering if we can wrap bap -d somehow and add the type information. This would be brilliant! Is this with little work possible?

As far as I can see, the -d option prints only terms, not attributes of terms. Also, it does not look like the output of -d is meant to be modified by plugins. So I suppose it would be easier to implement our own version of -d. This should not be too hard, but I would still wait with that until type inference is feature complete.

tbarabosch · 2019-03-29T19:54:07Z

src/analysis/mem_region.ml

+  match mem_region with
+  | [] -> new_node :: []
+  | head :: tail ->
+    if head.pos   head.size <= pos then


extract a function from the begin end block (line 46 - 59). This would make the function more readable.

I couldn't think of a useful way to extract a function there. I added some comments to improve readability instead.

tbarabosch · 2019-03-29T19:55:27Z

src/analysis/mem_region.ml

+      None
+    else if head.pos = pos then
+      match head.data with
+      | Ok(x) -> Some(Ok(x, head.size))


I see this Some(Ok()) wrapping all the time. Is that really idiomatic OCaml?

tbarabosch · 2019-03-29T19:58:24Z

src/analysis/type_inference.ml

+  [@@deriving bin_io, compare, sexp]
+
+  let merge reg1 reg2 =
+    if reg1 = reg2 then Some(Ok(reg1)) else Some(Error(()))


This Some(Ok()) wrapping again.

tbarabosch · 2019-03-29T20:09:27Z

src/utils/cconv.ml

+    end
+  | _ -> None
+
+let parse_dyn_syms project =


This function could be in module Symbol_utils

tbarabosch · 2019-03-29T20:10:57Z

src/utils/cconv.ml

+  let line = ref (String.strip line) in
+  let str_list = ref [] in
+  while Option.is_some (String.rsplit2 !line ~on:' ') do
+    let (left, right) = Option.value_exn (String.rsplit2 !line ~on:' ') in


That is a general concern and should be applied to the whole pull request (!): there are many Option.value_exn. I think they are never caught when they blow up. To honor the type system, we should unpack them correctly.

Hmm, in this particular case I would like to keep the value_exn, since I checked in the previous line that it cannot throw an exception. There is a way of writing this without the value_exn using functional programming style, but I think this would be more verbose and less readable in this case.

tbarabosch · 2019-03-29T20:13:43Z

test/unit/analysis/mem_region_test.ml

+  let x = Mem_region.add x "Five" ~pos:(bv 3) ~size:(bv 5) in
+  let x = Mem_region.add x "Seven" ~pos:(bv 9) ~size:(bv 7) in
+  let x = Mem_region.add x "Three" ~pos:(bv 0) ~size:(bv 3) in
+  check "add_ok" (Some(Ok("Five", bv 5)) = (Mem_region.get x (bv 3)));


Some(Ok()) and Some(Error()), I am really not sure what to think about it. Yet I've never seen it in other OCaml projects.

See #14 (comment)

tbarabosch · 2019-03-29T20:15:57Z

test/unit/analysis/mem_region_test.ml

+
+let test_remove () =
+  let bv num = Bitvector.of_int num ~width:32 in
+  let x = Mem_region.empty () in


these let x = look were tedious. Cann't you use the |> operator??

I cannot use |> here, because x is not the last argument in the Mem_region.add calls. I could write an add_list function for Mem_region for nicer looking code. But I actually like the current version more, because this way it is very explicit in which order the elements get added.

src/analysis/type_inference.ml

tbarabosch · 2019-03-29T20:30:07Z

This pull request is HUGE, let's start with the first couple of comments. I will do another iteration once they are fixed.

tbarabosch · 2019-03-29T20:33:05Z

One more thing: we should prefix EVERY plugin with cwe_checker, i.e. cwe_checker_type_inference for instance!

tbarabosch · 2019-03-29T20:46:01Z

And another thing: please adjust the Dockerfile to build everything (all the new plugins) for Travis CI!
Adjust the .travis* scripts to run Alcotest etc.

Enkelmann · 2019-04-01T11:31:21Z

When we switch to opam-testing for the master branch, we have to document it in the Readme and adjust the docker container.
I changed the Map.add_exn to Map.set, because in these use cases the previous value is meant to be overwrittten if it exists.
I will check whether prefixing every pass with cwe_checker works.

Enkelmann · 2019-04-01T12:19:50Z

Regarding the Some(Ok(_))-wrappings: I thought about defining a new wrapper type, but I think this way is more idiomatic: Every information during a fixpoint computation has essentially three states:

We don't have the information -> None
We do have conflicting information (e.g. from a merge) -> Some(Error()). We could also set this to None, but this could lead to infinite loops during fixpoint computation and knowing that there is conflicting infomation could also be useful information
We do have non-conflicting information -> Some(Ok(information))

Unless you think we should define a new wrapper type for this I don't know a more idiomatic way.

Regarding Codacy: Didn't we already fix that space problem in changes.md? Did codacy change its mind?

Enkelmann · 2019-04-02T12:38:45Z

TODO: Update readme for use of core 0.11

Enkelmann added 15 commits March 13, 2019 14:08

Type inference and unit tests initial commit

7bc533d

Correct stack_offset initial value

8e71c61

Adding sexp-derivers

85ffb3c

Rename module State to TypeInfo

91f8658

Refactor unit tests, added unit tests for type inference, added rudim…

8bce707

…entary stubs

Speed up dynamic symbol lookup

6ed2faf

added thumb mode to calling conventions

e73b7a0

Fixed bug for elements with negative start index

24a3b19

Mem_region.get also returns the size of an element

fd74e8b

Removed some TODOs

7879dc9

Print type info tags as debug messages

5eacb6a

Refactor to support multiple plugins

2e5b8ea

fixed typo

3b7a7f3

added dummy pass to print results of type inference pass

a8a6997

Fixed typo

1ba50c3

tbarabosch self-requested a review March 29, 2019 14:34

Enkelmann and others added 4 commits March 29, 2019 16:05

Updated Changes.md

48a890b

Fixed some JaneStreet Core issues related to Maps

3e8186d

Merge branch 'type_inference' of github.com:fkie-cad/cwe_checker into…

d174c87

… type_inference

Fixed more Core issues, all Map related.

7ebeeeb

tbarabosch reviewed Mar 29, 2019

View reviewed changes

tbarabosch mentioned this pull request Mar 29, 2019

cwe_checker_emulation plugin using BAP's Primus #15

Merged

Changed Map.add_exn to Map.set

02725bf

Added simple type inference recipe

1ca6542

Added some commments

3f7d767

Enkelmann added 6 commits April 3, 2019 08:28

Removed .Std from "open Core_kernel"

209aa5f

wrap functions that are only public for unit tests into a Test module

211a46d

Better error handling

d76c2df

Prefix every plugin with cwe_checker

0b8ad24

added unit test plugin to make clean

3273539

Merge branch 'master' into type_inference

f92572a

tbarabosch merged commit 2db57c4 into master Apr 5, 2019

tbarabosch deleted the type_inference branch April 5, 2019 11:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Type inference #14

Type inference #14

Enkelmann commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch left a comment

tbarabosch Mar 29, 2019

Enkelmann Apr 1, 2019 •

edited

Loading

tbarabosch Mar 29, 2019

Enkelmann Apr 1, 2019

tbarabosch Mar 29, 2019

tbarabosch Mar 29, 2019

tbarabosch Mar 29, 2019

tbarabosch Mar 29, 2019

Enkelmann Apr 3, 2019

tbarabosch Mar 29, 2019

Enkelmann Apr 1, 2019

tbarabosch Mar 29, 2019

Enkelmann Apr 1, 2019

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

Enkelmann commented Apr 1, 2019

Enkelmann commented Apr 1, 2019

Enkelmann commented Apr 2, 2019

Type inference #14

Type inference #14

Conversation

Enkelmann commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Enkelmann Apr 1, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

tbarabosch commented Mar 29, 2019

Enkelmann commented Apr 1, 2019

Enkelmann commented Apr 1, 2019

Enkelmann commented Apr 2, 2019

Enkelmann Apr 1, 2019 •

edited

Loading