[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

@@ -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

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))

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

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)

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 =
+let scuba_execution_id =
+  if scuba_logging then (
     Random.self_init () ;
-  Random.int64 Int64.max_value
+    Some (Random.int64 Int64.max_value) )
+  else None
 
 
 let toplevel_results_dir =

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} *)
 

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) =

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

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 ()

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 )

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

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))

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"