[erlang] Fix encoding of 'φ is true'

Summary:
We often encoded 'φ is true' by saying 'φ=v and v>0' for some fresh
variable v. The main reason is code organization: some part of the code
generates φ but returns only v to the caller, which adds the v>0
condition. But `PulseFormula` rightly does not infer that φ should be
true. Indeed the encoding of truth values should be complimentary; that
is, if 'true' is '>0' then 'false' should be '<=0', which is weird.

The convention that works better is 'true' is '!=0' and 'false is '=0'.
And with this convention the prover does what we expect.

The outcome: a lot of states that were infeasible are now detected as
such.

Reviewed By: thizanne

Differential Revision: D63838812

fbshipit-source-id: b45c82ec0ceb8d4f484006bc01ae9287cb4b6f2f

infer/src/pulse/PulseModelsErlang.ml

@@ -143,7 +143,7 @@ let prune_type path location (value, hist) typ astate : AbductiveDomain.t result
      |> PulseResult.ok |> SatUnsat.of_option
    in
    let** astate, instanceof_val = has_erlang_type value typ astate in
-   PulseArithmetic.prune_positive instanceof_val astate )
+   PulseArithmetic.prune_ne_zero instanceof_val astate )
   |> SatUnsat.to_list
 
 
@@ -335,7 +335,7 @@ module Atoms = struct
   (* Converts [bool_value] into true/false, and write it to [addr_atom]. *)
   let of_bool path location bool_value astate =
     let astate_true =
-      let** astate = PulseArithmetic.prune_positive bool_value astate in
+      let** astate = PulseArithmetic.prune_ne_zero bool_value astate in
       of_string location path ErlangTypeName.atom_true astate
     in
     let astate_false :
@@ -434,7 +434,7 @@ module Comparison = struct
     let const_true _x _y _tenv _location _path : value_maker =
      fun astate ->
       let const_true = AbstractValue.mk_fresh () in
-      let++ astate = PulseArithmetic.prune_positive const_true astate in
+      let++ astate = PulseArithmetic.prune_ne_zero const_true astate in
       (astate, const_true)
 
 
@@ -665,7 +665,7 @@ module Comparison = struct
   (** Returns an abstract state that has been pruned on the comparison result being true. *)
   let prune cmp tenv location path x y astate : AbductiveDomain.t AccessResult.t list =
     let> astate, (comparison, _hist) = make_raw cmp tenv location path x y astate in
-    PulseArithmetic.prune_positive comparison astate |> SatUnsat.to_list
+    PulseArithmetic.prune_ne_zero comparison astate |> SatUnsat.to_list
 
 
   (** {1 Specific comparison operators} *)
@@ -965,7 +965,7 @@ module Maps = struct
       let astate, _isempty_addr, (is_empty, _isempty_hist) =
         load_field path is_empty_field location map astate
       in
-      let> astate = PulseArithmetic.prune_positive is_empty astate |> SatUnsat.to_list in
+      let> astate = PulseArithmetic.prune_ne_zero is_empty astate |> SatUnsat.to_list in
       let> astate =
         PulseArithmetic.and_eq_int ret_val_false IntLit.zero astate |> SatUnsat.to_list
       in
@@ -1012,7 +1012,7 @@ module Maps = struct
       let astate, _isempty_addr, (is_empty, _isempty_hist) =
         load_field path is_empty_field location map astate
       in
-      let> astate = PulseArithmetic.prune_positive is_empty astate |> SatUnsat.to_list in
+      let> astate = PulseArithmetic.prune_ne_zero is_empty astate |> SatUnsat.to_list in
       Errors.badkey data astate
     in
     List.map ~f:Basic.map_continue astate_ok @ astate_badkey @ astate_badmap
@@ -1062,7 +1062,7 @@ module Maps = struct
       let astate, _isempty_addr, (is_empty, _isempty_hist) =
         load_field path is_empty_field location map astate
       in
-      let> astate = PulseArithmetic.prune_positive is_empty astate |> SatUnsat.to_list in
+      let> astate = PulseArithmetic.prune_ne_zero is_empty astate |> SatUnsat.to_list in
       let<+> astate, addr_nil = Lists.make_nil_raw location path astate in
       PulseOperations.write_id ret_id addr_nil astate
     in
@@ -1187,13 +1187,13 @@ module BIF = struct
     let astate_is_cons =
       let is_cons = AbstractValue.mk_fresh () in
       let<**> astate = PulseArithmetic.and_equal_instanceof is_cons list_val cons_typ astate in
-      let<**> astate = PulseArithmetic.prune_positive is_cons astate in
+      let<**> astate = PulseArithmetic.prune_ne_zero is_cons astate in
       Atoms.write_return_from_bool path location is_cons ret_id astate
     in
     let astate_is_nil =
       let is_nil = AbstractValue.mk_fresh () in
       let<**> astate = PulseArithmetic.and_equal_instanceof is_nil list_val nil_typ astate in
-      let<**> astate = PulseArithmetic.prune_positive is_nil astate in
+      let<**> astate = PulseArithmetic.prune_ne_zero is_nil astate in
       Atoms.write_return_from_bool path location is_nil ret_id astate
     in
     let astate_not_list =

infer/tests/codetoanalyze/erlang/pulse/features/features_maps.erl

@@ -177,9 +177,7 @@ test_record_unpack_Latent(X) ->
         true -> ok
     end.
 
-% The two latent issues have different causes:
-%  - not using the map spec
-%  - encoding of equality prunning confuses the prover
+% The latent issue is caused by not using the map spec.
 -spec fpl_test_record_unpack_Ok(ab()) -> ok.
 fpl_test_record_unpack_Ok(X) ->
     #{a := A, b := B} = X,

infer/tests/codetoanalyze/erlang/pulse/issues.exp

@@ -217,9 +217,7 @@ codetoanalyze/erlang/pulse/features/features_maps.erl, test_to_list2_Bad/0, 1, N
 codetoanalyze/erlang/pulse/features/features_maps.erl, test_to_list4_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_maps.erl, fp_test_to_list5_Ok/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_maps.erl, test_record_unpack_Latent/1, 1, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
-codetoanalyze/erlang/pulse/features/features_maps.erl, test_record_unpack_Latent/1, 4, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_maps.erl, fpl_test_record_unpack_Ok/1, 1, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
-codetoanalyze/erlang/pulse/features/features_maps.erl, fpl_test_record_unpack_Ok/1, 5, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_matchexpr.erl, test_match2_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_matchexpr.erl, test_match4_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/features/features_maybe.erl, test_maybe_simple_Bad/0, 8, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]