Infer# integration #1361

xi-liu-ds · 2020-12-16T04:39:42Z

Dear Infer team,

To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.

Please help to review, discuss and consider to merge this feature.

Thanks,
Xiaoyu

…gration

Integration

jvillard

This looks good overall I think. I haven't read much of AnalyzeJson yet.

Are you able to run the auto-formatter with make fmt? You'll need this version of ocamlformat: https://github.com/ocaml-ppx/ocamlformat/tree/nebuchadnezzar
I think this command does the trick: opam pin add ocamlformat.0.14.1-13-g000da99 -k git https://github.com/ocaml-ppx/ocamlformat.git#nebuchadnezzar

jvillard · 2020-12-18T13:14:24Z

.github/workflows/install.yml

@@ -65,7 +65,7 @@ jobs:

      - name: Install Required Apt Packages for Ubuntu
        run: |
-          sudo apt install libmpfr-dev libsqlite3-dev ninja-build
+          sudo apt install libmpfr-dev sqlite3 libsqlite3-dev ninja-build


Is sqlite3 itself used anywhere yet?

This looks good overall I think. I haven't read much of AnalyzeJson yet.

Are you able to run the auto-formatter with make fmt? You'll need this version of ocamlformat: https://github.com/ocaml-ppx/ocamlformat/tree/nebuchadnezzar
I think this command does the trick: opam pin add ocamlformat.0.14.1-13-g000da99 -k git https://github.com/ocaml-ppx/ocamlformat.git#nebuchadnezzar

I got build error in this ocamlformat branch. I will try again after they fixed the pipeline.

Is sqlite3 itself used anywhere yet?

Removed. Good catch!

jvillard · 2020-12-18T16:40:33Z

infer/src/IR/CallFlags.ml

@@ -17,17 +17,19 @@ type t =
  ; cf_injected_destructor: bool
  ; cf_interface: bool
  ; cf_is_objc_block: bool
+  ; cf_noreturn: bool


This was deleted by 9979489 because it is dead code. It looks like the flag has been reintroduced by mistake in this PR.

This was deleted by 9979489 because it is dead code. It looks like the flag has been reintroduced by mistake in this PR.

Removed. Thanks

jvillard · 2020-12-18T16:47:48Z

infer/src/IR/Cfg.ml

@@ -40,6 +39,14 @@ let create_proc_desc cfg (proc_attributes : ProcAttributes.t) =
  Procname.Hash.add cfg pname pdesc ;
  pdesc

+(** Get a procdesc or create if it is a new one*)
+let get_proc_desc cfg (proc_attributes : ProcAttributes.t) =


This looks a bit dangerous to add to the Cfg module and I'm not sure I understand why it's needed: what happens if the proc name is already present? The proc desc will get created but not recorded in the CFG, so in the end it's discarded?

This is only used once, could you maybe rewrite the call site to if not (Cfg.mem proc_attributes.proc_name) then Cfg.create_proc_desc ...?

This looks a bit dangerous to add to the Cfg module and I'm not sure I understand why it's needed: what happens if the proc name is already present? The proc desc will get created but not recorded in the CFG, so in the end it's discarded?

This is only used once, could you maybe rewrite the call site to if not (Cfg.mem proc_attributes.proc_name) then Cfg.create_proc_desc ...?

Good suggestion. I have rewritten this call.

jvillard · 2020-12-18T16:55:36Z

infer/src/IR/Procdesc.mli

@@ -315,6 +317,8 @@ val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum) -> 'accum
 val fold_slope_range : Node.t -> Node.t -> init:'accum -> f:('accum -> Node.t -> 'accum) -> 'accum
 (** fold between two nodes or until we reach a branching structure *)

+val set_succs_exn_base : Node.t -> Node.t list -> Node.t list -> unit


Why not use set_succs instead?

If this is needed could you add a doc string explaining that it should be used carefully because it won't update the node's successors' pred links? (not sure why that is ok except when the current node is known to have no succs, but then this is the same as set_succs just below) Named arguments like set_succs would be nice too since the types don't help to disambiguate the arguments here.

Why not use set_succs instead?

If this is needed could you add a doc string explaining that it should be used carefully because it won't update the node's successors' pred links? (not sure why that is ok except when the current node is known to have no succs, but then this is the same as set_succs just below) Named arguments like set_succs would be nice too since the types don't help to disambiguate the arguments here.

It was an outdated function. I have replaced it with set_succs

jvillard · 2020-12-18T16:58:20Z

infer/src/atd/InferCommand.mli

@@ -8,6 +8,7 @@
 (** Main modes of operation for infer *)
 type t =
  | Analyze  (** analyze previously captured source files *)
+  | AnalyzeJson


A doc comment like the other commands would be nice.

A doc comment like the other commands would be nice.

Added. Thanks for suggestion

jvillard · 2020-12-18T17:01:06Z

infer/src/backend/InferAnalyzeJson.mli

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2009-2013, Monoidics ltd.


Please delete this line, it's only present on older source code where appropriate but new code should be just (c) Facebook.

Please delete this line, it's only present on older source code where appropriate but new code should be just (c) Facebook.

Deleted

jvillard · 2020-12-18T17:01:51Z

infer/src/backend/registerCheckers.ml

+          , Java )
+          ;( interprocedural Payloads.Fields.lab_resource_leaks ResourceLeaks.checker
+          , CIL ) ] }
+  ; (* toy resource analysis to use in the infer lab, see the lab/ directory *)


outdated comment?

outdated comment?

Deleted

jvillard · 2020-12-18T17:02:01Z

infer/src/backend/registerCheckers.ml

+        [ ( (* the checked-in version is intraprocedural, but the lab asks to make it
+               interprocedural later on *)


outdated?

Deleted

jvillard · 2020-12-18T17:03:55Z

infer/src/base/DB.ml

+  let clean_specs_dir () =
+    (* create dir just in case it doesn't exist to avoid errors *)
+    Utils.create_dir specs_dir ;
+    Array.iter (Sys.readdir specs_dir) ~f:(fun specs ->
+        Filename.concat specs_dir specs |> Sys.remove )
+
+


Is this a rebase error or is the specs/ directory really back?

Is this a rebase error or is the specs/ directory really back?

Yes, it is a rebase error. I have updated to comply with latest infer. Good catch. Thanks

jvillard · 2020-12-18T17:11:06Z

infer/src/base/CommandDoc.ml

+  mk_command_doc ~title:"Infer Analysis" ~short_description:"analyze the files captured by infer"
+    ~synopsis:{|$(b,infer) $(b,analyze) $(i,[options])
+$(b,infer) $(i,[options])|}
+    ~description:[`P "Analyze the files captured in the project results directory and report."]
+    ~see_also:InferCommand.[Report; Run]


Could you update this to document the new command? Having an example of how to run the new command would be helpful. Would you be able to paste an example json somewhere? I'd love to be able to experiment with this PR locally.

Could you update this to document the new command? Having an example of how to run the new command would be helpful. Would you be able to paste an example json somewhere? I'd love to be able to experiment with this PR locally.

Added. And I have added example jsons in examples/dotnet_hello/jsons

add unit tests

xi-liu-ds · 2021-01-06T07:41:25Z

I was able to figure out ocamlformat installation issue and ran make fmt successfully. It turns out that ocamlformat needs to be reinstalled first and then install nebuchadnezzar version.

Now all comments are resolved and this PR is ready for a second round of review.

jvillard · 2021-01-06T10:59:21Z

Makefile

@@ -190,6 +190,25 @@ BUILD_SYSTEMS_TESTS += mvn
 endif
 endif

+ifeq ($(BUILD_DOTNET_ANALYZERS),yes)


Is this ifeq needed? We provide compile-time options in ./configure to disable the clang or Java frontends because sometimes it makes sense for the user, but these tests are independent of any frontends since they rely on infer-analyzejson. If you remove the ifeq or run make BUILD_DOTNET_ANALYZERS=yes you should be able to run these tests as part of make test or individually with, eg, make BUILD_DOTNET_ANALYZERS=yes direct_dotnet_box_test.

Got it. Thanks.

facebook-github-bot

@bigfootjon has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

facebook-github-bot · 2021-01-19T20:18:58Z

@xi-liu-ds has updated the pull request. You must reimport the pull request before landing.

facebook-github-bot · 2021-01-22T08:33:08Z

@xi-liu-ds has updated the pull request. You must reimport the pull request before landing.

facebook-github-bot

@jvillard has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

xi-liu-ds · 2021-01-26T18:13:39Z

Hi~

I saw there might have some tests failed in Facebook Internal Builds & Tests. I can't see what exactly caused the failure... But if it is about infersharp unit tests, I can either check in compressed json files (they are ready and good to go!) or remove all of them from DIRECT_TESTS in make file.

Let me know what is the best option for you~

Thanks!

xz unit tests

facebook-github-bot · 2021-01-28T16:34:18Z

@xi-liu-ds has updated the pull request. You must reimport the pull request before landing.

jvillard · 2021-01-28T16:36:15Z

The compilation failures are due to a small amount of extra code we have in the internal repo that needs to be updated by us. I'll do that.

xi-liu-ds · 2021-01-28T17:05:51Z

The compilation failures are due to a small amount of extra code we have in the internal repo that needs to be updated by us. I'll do that.

I see. Thanks!

Now all compressed jsons are in. Feel free to give it a run simply with make direct_tests.

facebook-github-bot

@jvillard has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

facebook-github-bot · 2021-02-02T16:11:15Z

@xi-liu-ds has updated the pull request. You must reimport the pull request before landing.

facebook-github-bot · 2021-02-04T16:39:47Z

@jvillard merged this pull request in 285ddb4.

xi-liu-ds added 18 commits November 3, 2020 21:50

integrate with infersharp

661ef65

more changes to compatible with infersharp

cd1e6fc

remove useless adds

3fa4160

resolve incompatibilities

a5c023b

Merge remote-tracking branch 'upstream/master' into integration

d9b00ca

null dereference support for C#

0e4489a

Merge branch 'master' of github.com:xi-liu-ds/infer into integration

9374648

generate specs files

b5a8d6d

Merge branch 'master' of https://github.com/xi-liu-ds/infer into inte…

545c78b

…gration

add resource leak support

cc87294

Merge pull request #1 from xi-liu-ds/integration

4f4acf6

Integration

Merge branch 'master' of https://github.com/xi-liu-ds/infer

4e86aa8

remove fallbacknode

280a5fb

add get proc desc function for .net

ebf8e88

fix float on nan

f0b6e33

Merge remote-tracking branch 'upstream/master'

0ec94eb

seperate infer analyze json logics

71914ae

fix deprecated warnings

a0e0c28

facebook-github-bot added the CLA Signed label Dec 16, 2020

Merge branch 'master' into master

01b1037

jvillard reviewed Dec 18, 2020

View reviewed changes

xi-liu-ds added 4 commits December 24, 2020 07:10

resolve comments

a67918c

Merge branch 'master' of https://github.com/xi-liu-ds/infer

7047a71

Merge remote-tracking branch 'upstream/master'

8848fdb

fix build failure

6986656

xinshiMSFT mentioned this pull request Dec 24, 2020

Merge language-agnostic layer back to Infer microsoft/infersharp#27

Closed

xi-liu-ds added 4 commits December 29, 2020 04:43

add unit tests

f3b95de

add unit tests make file

db3ada8

Merge pull request #2 from xi-liu-ds/xiaoyu/integration/unittests

4a001b4

add unit tests

Merge remote-tracking branch 'upstream/master'

b2f300a

xi-liu-ds added 2 commits January 6, 2021 07:34

format cleanup

77270e2

Merge branch 'master' of https://github.com/xi-liu-ds/infer

4270215

jvillard reviewed Jan 6, 2021

View reviewed changes

remove BUILD_DOTNET_ANALYZERS condition

de588c5

facebook-github-bot reviewed Jan 15, 2021

View reviewed changes

focus on resource leaks and null deref

6ca305a

remove unit test jsons files

0145560

xz unit tests

d0945ba

facebook-github-bot reviewed Jan 25, 2021

View reviewed changes

Merge pull request #3 from xi-liu-ds/xi-liu-ds/xzjsons

56d910e

xz unit tests

facebook-github-bot reviewed Jan 28, 2021

View reviewed changes

Merge branch 'master' into master

c35f6c1

facebook-github-bot closed this in 285ddb4 Feb 4, 2021

facebook-github-bot added the Merged label Feb 4, 2021

		[ ( (* the checked-in version is intraprocedural, but the lab asks to make it
		interprocedural later on *)

Infer# integration #1361

Infer# integration #1361

Conversation

xi-liu-ds commented Dec 16, 2020 • edited Loading

jvillard left a 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

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

xi-liu-ds Dec 24, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xi-liu-ds commented Jan 6, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

facebook-github-bot left a comment

Choose a reason for hiding this comment

facebook-github-bot commented Jan 19, 2021

facebook-github-bot commented Jan 22, 2021

facebook-github-bot left a comment

Choose a reason for hiding this comment

xi-liu-ds commented Jan 26, 2021 • edited Loading

facebook-github-bot commented Jan 28, 2021

jvillard commented Jan 28, 2021

xi-liu-ds commented Jan 28, 2021

facebook-github-bot left a comment

Choose a reason for hiding this comment

facebook-github-bot commented Feb 2, 2021

facebook-github-bot commented Feb 4, 2021

xi-liu-ds commented Dec 16, 2020 •

edited

Loading

xi-liu-ds Dec 24, 2020 •

edited

Loading

xi-liu-ds commented Jan 26, 2021 •

edited

Loading