From 2eb6eb3655adf5f73e47e039235d6f7177ae9529 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 13 Aug 2020 03:11:49 -0700
Subject: [PATCH] [pulse] skeleton for unit testing pulse

Summary:
Add unit tests to pulse in order to write tests for the arithmetic
solver, because it is a pain to write programs to do that end to end.

Reviewed By: ezgicicek

Differential Revision: D22864607

fbshipit-source-id: 0a20a3593
---
 .gitignore                                |  4 --
 infer/dune-project                        |  1 -
 infer/src/.ocamlformat-ignore             | 12 ++++++
 infer/src/Makefile                        | 11 +++++-
 infer/src/base/Config.ml                  | 15 +++++--
 infer/src/base/Config.mli                 |  3 +-
 infer/src/base/ScubaLogging.ml            |  3 +-
 infer/src/dune.in                         |  6 ++-
 infer/src/infer.ml                        |  2 +-
 infer/src/pulse/unit/PulseFormulaTest.ml  | 48 +++++++++++++++++++++++
 infer/src/pulse/unit/PulseFormulaTest.mli |  8 ++++
 infer/src/pulse/unit/dune                 | 13 ++++++
 opam                                      |  1 +
 13 files changed, 111 insertions(+), 16 deletions(-)
 create mode 100644 infer/src/.ocamlformat-ignore
 create mode 100644 infer/src/pulse/unit/PulseFormulaTest.ml
 create mode 100644 infer/src/pulse/unit/PulseFormulaTest.mli
 create mode 100644 infer/src/pulse/unit/dune

diff --git a/.gitignore b/.gitignore
index cd23ac9c0..407b42c34 100644
--- a/.gitignore
+++ b/.gitignore
@@ -141,10 +141,6 @@ buck-out/
 # intelliJ files
 /infer/src/backend/.projectSettings
 
-# copied from facebook-clang-plugins or generated by atdgen
-/infer/src/clang_plugin/*.ml
-/infer/src/clang_plugin/*.mli
-
 /infer/annotations/annot_classes/
 /infer/annotations/annotations.jar
 /infer/annotations/annotations-src.jar
diff --git a/infer/dune-project b/infer/dune-project
index bb4ff3258..1d537821a 100644
--- a/infer/dune-project
+++ b/infer/dune-project
@@ -5,4 +5,3 @@
 ; LICENSE file in the root directory of this source tree.
 
 (using menhir 1.0)
-(formatting (enabled_for dune))
diff --git a/infer/src/.ocamlformat-ignore b/infer/src/.ocamlformat-ignore
new file mode 100644
index 000000000..f47c53e6e
--- /dev/null
+++ b/infer/src/.ocamlformat-ignore
@@ -0,0 +1,12 @@
+# generated by ATD
+atd/*_b.ml
+atd/*_b.mli
+atd/*_j.ml
+atd/*_j.mli
+atd/*_t.ml
+atd/*_t.mli
+atd/clang_*.ml
+atd/clang_*.mli
+# generated
+base/Version.ml
+deadcode/all_infer_in_one_file.ml
diff --git a/infer/src/Makefile b/infer/src/Makefile
index 7df9fd4f1..e9682d877 100644
--- a/infer/src/Makefile
+++ b/infer/src/Makefile
@@ -86,13 +86,20 @@ endif
 .PHONY: src_build_common
 src_build_common: $(SRC_BUILD_COMMON)
 
+# NOTE: the complexity below is because @runtest and @fmt interact poorly: we want dune to format
+# test files *after* having promoted them when the test outputs change
 .PHONY: test
 test: BUILD_MODE = test
 test: $(SRC_BUILD_COMMON) $(MAKEFILE_LIST)
-	$(QUIET)$(DUNE_BUILD) \
+	$(QUIET)exit_code=0; \
+	$(DUNE_BUILD) \
 	  $(patsubst %.exe, %.bc.exe, $(INFER_CONFIG_TARGETS)) \
 	  scripts/$(CHECKCOPYRIGHT_MAIN).bc.exe $(INFERUNIT_MAIN).bc.exe $(INFERTOP_MAIN).bc.exe \
-	  @fmt --auto-promote
+	  || exit_code=$$?; \
+	$(DUNE_BUILD) @runtest --auto-promote || exit_code=$$?; \
+	$(DUNE_BUILD) @fmt --auto-promote || exit_code=$$?; \
+	exit $$exit_code
+
 
 .PHONY: doc
 doc: $(SRC_BUILD_COMMON) $(MAKEFILE_LIST)
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index fdc135e86..468730e5d 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -408,7 +408,12 @@ let implicit_sdk_root =
 let startup_action =
   let open CLOpt in
   if infer_is_javac then Javac
-  else if !Sys.interactive || String.is_substring ~substring:"inferunit" exe_basename then NoParse
+  else if
+    !Sys.interactive
+    || String.is_substring ~substring:"inferunit" exe_basename
+    || String.equal "run.exe" exe_basename
+    || String.equal "run.bc" exe_basename
+  then NoParse
   else if infer_is_clang then NoParse
   else InferCommand
 
@@ -3290,9 +3295,11 @@ let is_in_custom_symbols list_name symbol =
       false
 
 
-let execution_id =
-  Random.self_init () ;
-  Random.int64 Int64.max_value
+let scuba_execution_id =
+  if scuba_logging then (
+    Random.self_init () ;
+    Some (Random.int64 Int64.max_value) )
+  else None
 
 
 let toplevel_results_dir =
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index bfc793138..3c736579f 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -641,7 +641,8 @@ val is_in_custom_symbols : string -> string -> bool
 val java_package_is_external : string -> bool
 (** Check if a Java package is external to the repository *)
 
-val execution_id : Int64.t
+val scuba_execution_id : Int64.t option
+(** a random number to (hopefully) uniquely identify this run *)
 
 (** {2 Global variables with initial values specified by command-line options} *)
 
diff --git a/infer/src/base/ScubaLogging.ml b/infer/src/base/ScubaLogging.ml
index 33bbeea6a..4cb040503 100644
--- a/infer/src/base/ScubaLogging.ml
+++ b/infer/src/base/ScubaLogging.ml
@@ -35,7 +35,8 @@ let set_common_fields sample =
   |> maybe_add_normal ~name:"job_id" ~value:Config.job_id
   |> add_normal ~name:"command" ~value:(InferCommand.to_string Config.command)
   |> add_normal ~name:"infer_commit" ~value:Version.commit
-  |> add_normal ~name:"execution_id" ~value:(Int64.to_string Config.execution_id)
+  |> maybe_add_normal ~name:"execution_id"
+       ~value:(Option.map ~f:Int64.to_string Config.scuba_execution_id)
 
 
 let sample_from_event ({label; created_at_ts; data} : LogEntry.t) =
diff --git a/infer/src/dune.in b/infer/src/dune.in
index d5962c21f..e8bc3e9f9 100644
--- a/infer/src/dune.in
+++ b/infer/src/dune.in
@@ -41,12 +41,14 @@ let env_stanza =
     {|
 (env
   (dev
-    (flags %s))
+    (flags %s)
+    (inline_tests enabled))
   (opt
     (flags %s)
     (ocamlopt_flags (:standard -O3)))
   (test
-    (flags %s))
+    (flags %s)
+    (inline_tests enabled))
   )
 |}
     lenient_flags lenient_flags strict_flags
diff --git a/infer/src/infer.ml b/infer/src/infer.ml
index 12678effd..8d1124130 100644
--- a/infer/src/infer.ml
+++ b/infer/src/infer.ml
@@ -152,7 +152,7 @@ let () =
   if has_results_dir then log_environment_info () ;
   if has_results_dir && Config.debug_mode && CLOpt.is_originator then (
     L.progress "Logs in %s@." (ResultsDir.get_path Logs) ;
-    L.progress "Execution ID %Ld@." Config.execution_id ) ;
+    Option.iter Config.scuba_execution_id ~f:(fun id -> L.progress "Execution ID %Ld@." id) ) ;
   ( match Config.command with
   | _ when Config.test_determinator && not Config.process_clang_ast ->
       TestDeterminator.compute_and_emit_test_to_run ()
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
new file mode 100644
index 000000000..8d941b5c0
--- /dev/null
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -0,0 +1,48 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+module AbstractValue = PulseAbstractValue
+module Formula = PulseFormula
+
+let%test_module _ =
+  ( module struct
+    let normalize phi = Formula.normalize phi |> F.printf "%a" Formula.pp
+
+    (** shorthand for defining formulas easily *)
+
+    let i i = Formula.Term.of_intlit (IntLit.of_int i)
+
+    let ( + ) t1 t2 = Formula.Term.of_binop (PlusA None) t1 t2
+
+    let ( - ) t1 t2 = Formula.Term.of_binop (MinusA None) t1 t2
+
+    let ( = ) t1 t2 = Formula.mk_equal t1 t2
+
+    let ( < ) t1 t2 = Formula.mk_less_than t1 t2
+
+    let ( && ) phi1 phi2 = Formula.aand phi1 phi2
+
+    let x = Formula.Term.of_absval (AbstractValue.mk_fresh ())
+
+    let y = Formula.Term.of_absval (AbstractValue.mk_fresh ())
+
+    let z = Formula.Term.of_absval (AbstractValue.mk_fresh ())
+
+    let%expect_test _ =
+      normalize (x + i 1 - i 1 < x) ;
+      [%expect "\n        [ &&\n        {((v1)+(1))+(-1) < v1}]"]
+
+    let%expect_test _ =
+      normalize (x + (y - x) < y) ;
+      [%expect "\n        [ &&\n        {(v1)+((v2)+(-(v1))) < v2}]"]
+
+    let%expect_test _ =
+      normalize (x = y && y = z && z = i 0 && x = i 1) ;
+      [%expect "\n        [0=1=v1=v2=v3 &&\n        ]"]
+  end )
diff --git a/infer/src/pulse/unit/PulseFormulaTest.mli b/infer/src/pulse/unit/PulseFormulaTest.mli
new file mode 100644
index 000000000..ec12bc776
--- /dev/null
+++ b/infer/src/pulse/unit/PulseFormulaTest.mli
@@ -0,0 +1,8 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
diff --git a/infer/src/pulse/unit/dune b/infer/src/pulse/unit/dune
new file mode 100644
index 000000000..45fdde440
--- /dev/null
+++ b/infer/src/pulse/unit/dune
@@ -0,0 +1,13 @@
+; Copyright (c) Facebook, Inc. and its affiliates.
+;
+; This source code is licensed under the MIT license found in the
+; LICENSE file in the root directory of this source tree.
+
+(library
+ (name PulseTest)
+ (flags
+  (:standard -open IStdlib -open IStd -open Pulselib -open IR))
+ (libraries IStdlib Pulselib)
+ (preprocess
+  (pps ppx_expect ppx_inline_test))
+ (inline_tests))
diff --git a/opam b/opam
index b091519e6..5ee305bc8 100644
--- a/opam
+++ b/opam
@@ -42,6 +42,7 @@ depends: [
   "ppx_compare" {>= "v0.14.0" & < "v0.15"}
   "ppx_deriving" {>="4.1"}
   "ppx_enumerate" {>= "v0.14.0" & < "v0.15"}
+  "ppx_expect" {>= "v0.14.0" & < "v0.15"}
   "ppx_fields_conv" {>= "v0.14.0" & < "v0.15"}
   "sawja" {>="1.5.8"}
   "sqlite3"