[build] address warnings 52 and 57

Summary:
OCaml 4.04.0 new warnings raised a few valid points!

Fixing warning 57 in two ways:
- best way: introduce an auxiliary function to avoid code duplication
- not-so-best way: introduce code duplication. I did that when the branches body are small. Typically the number of bound variables in the pattern is high, so an auxiliary function would need to take many arguments and the whole thing will not be readable (we'd still duplicate the arguments we pass to the function for instance).

Reviewed By: jberdine

Differential Revision: D4851006

fbshipit-source-id: fbf1867

infer/src/backend/dom.ml

@@ -710,7 +710,13 @@ end = struct
     else
       begin
         match atom_in with
-        | Sil.Aneq((Exp.Var id as e), e') | Sil.Aneq(e', (Exp.Var id as e))
+        | Sil.Aneq((Exp.Var id as e), e')
+          when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
+            (* e' cannot also be a normal id according to the guard so we can consider the two cases
+               separately (this case and the next) *)
+            build_other_atoms (fun e0 -> Prop.mk_neq tenv e0 e') side e
+
+        | Sil.Aneq(e', (Exp.Var id as e))
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_neq tenv e0 e') side e
 
@@ -722,7 +728,13 @@ end = struct
           when not (Ident.is_normal id) && List.for_all ~f:exp_contains_only_normal_ids es ->
             build_other_atoms (fun e0 -> Prop.mk_npred tenv a (e0 :: es)) side e
 
-        | Sil.Aeq((Exp.Var id as e), e') | Sil.Aeq(e', (Exp.Var id as e))
+        | Sil.Aeq((Exp.Var id as e), e')
+          when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
+            (* e' cannot also be a normal id according to the guard so we can consider the two cases
+               separately (this case and the next) *)
+            build_other_atoms (fun e0 -> Prop.mk_eq tenv e0 e') side e
+
+        | Sil.Aeq(e', (Exp.Var id as e))
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_eq tenv e0 e') side e
 

infer/src/backend/prop.ml

@@ -1377,21 +1377,25 @@ module Normalize = struct
                  into a strexp of the given type *)
               let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in
               replace_hpred hpred'
-          | (Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst)
+          | Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst),
-            | Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst)),
+            Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt ->
-            Sizeof (Tarray (elt, _) as arr, _, _)
-            when Typ.equal t elt ->
               let len = Some x in
-              let hpred' =
+              let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
-                mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
               replace_hpred (replace_array_contents hpred' esel)
-          | ( Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst)
+          | Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst),
-            | Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst)),
+            Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt ->
-            Sizeof (Tarray (elt, _) as arr, _, _)
+              let len = Some x in
-            when Typ.equal t elt ->
+              let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
+              replace_hpred (replace_array_contents hpred' esel)
+          | Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst),
+            Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt ->
+              let len = Some (Exp.BinOp(Mult, x, len)) in
+              let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
+              replace_hpred (replace_array_contents hpred' esel)
+          | Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst),
+            Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt ->
               let len = Some (Exp.BinOp(Mult, x, len)) in
-              let hpred' =
+              let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
-                mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
               replace_hpred (replace_array_contents hpred' esel)
           | _ ->
               Hpointsto (normalized_root, normalized_cnt, normalized_te)

infer/src/backend/prover.ml

@@ -1183,11 +1183,17 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
           (fst subs, sub2')
         else
           raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2))))
-    | e1, Exp.BinOp (Binop.PlusA, Exp.Var v2, e2)
+    | e1, Exp.BinOp (Binop.PlusA, (Exp.Var v2 as e2), e2')
-    | e1, Exp.BinOp (Binop.PlusA, e2, Exp.Var v2)
       when Ident.is_primed v2 || Ident.is_footprint v2 ->
-        let e' = Exp.BinOp (Binop.MinusA, e1, e2) in
+        (* here e2' could also be a variable that we could try to substitute (as in the next match
-        do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') (Exp.Var v2)
+           case), but we ignore that to avoid backtracking *)
+        let e' = Exp.BinOp (Binop.MinusA, e1, e2') in
+        do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
+    | e1, Exp.BinOp (Binop.PlusA, e2, (Exp.Var v2 as e2'))
+      when Ident.is_primed v2 || Ident.is_footprint v2 ->
+        (* symmetric of above case *)
+        let e' = Exp.BinOp (Binop.MinusA, e1, e2') in
+        do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
     | Exp.Var _, e2 ->
         if calc_missing then
           let () = ProverState.add_missing_pi (Sil.Aeq (e1_in, e2_in)) in
@@ -1219,6 +1225,8 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
     | Exp.Sizeof (t1, Some d1, st1), Exp.Sizeof (t2, Some d2, st2)
       when Typ.equal t1 t2 && Exp.equal d1 d2 && Subtype.equal_modulo_flag st1 st2 -> subs
     | e', Exp.Const (Const.Cint n)
+      when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero ->
+        raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2))))
     | Exp.Const (Const.Cint n), e'
       when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero ->
         raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2))))

infer/src/backend/rearrange.ml

@@ -762,7 +762,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
           None in
 
     List.find_map
-      ~f:(function
+      ~f:(function [@warning "-57"] (* FIXME: silenced warning may be legit *)
           | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _))
           | Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _))
             when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) ->

infer/src/backend/symExec.ml

@@ -323,12 +323,16 @@ let rec prune tenv ~positive condition prop =
   | Exp.UnOp _ ->
       assert false
   | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i))
+    when IntLit.iszero i && not (IntLit.isnull i) ->
+      prune tenv ~positive:(not positive) e prop
   | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e)
     when IntLit.iszero i && not (IntLit.isnull i) ->
       prune tenv ~positive:(not positive) e prop
   | Exp.BinOp (Binop.Eq, e1, e2) ->
       prune_ne tenv ~positive:(not positive) e1 e2 prop
   | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i))
+    when IntLit.iszero i && not (IntLit.isnull i) ->
+      prune tenv ~positive e prop
   | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e)
     when IntLit.iszero i && not (IntLit.isnull i) ->
       prune tenv ~positive e prop

infer/src/base/Config.ml

@@ -318,7 +318,7 @@ let ncpu =
   try
     Utils.with_process_in
       "getconf _NPROCESSORS_ONLN 2>/dev/null"
-      (fun chan -> Scanf.fscanf chan "%d" (fun n -> n))
+      (fun chan -> Scanf.bscanf (Scanf.Scanning.from_channel chan) "%d" (fun n -> n))
     |> fst
   with _ ->
     1

infer/src/clang/Capture.re

@@ -17,11 +17,16 @@ let debug_mode = Config.debug_mode || Config.frontend_stats || Config.frontend_d
 let buffer_len = 262143;
 
 let catch_biniou_buffer_errors f x =>
+  (
     try (f x) {
+    /* suppress warning: allow this one case because we're just reraising the error with another
+       error message so it doesn't really matter if this eventually fails */
     | Invalid_argument "Bi_inbuf.refill_from_channel" =>
       Logging.err "WARNING: biniou buffer too short, skipping the file@\n";
       assert false
-  };
+    }
+  )
+  [@warning "-52"];
 
 /* This function reads the json file in fname, validates it, and encoded in the AST data structure
    defined in Clang_ast_t.  */

infer/src/eradicate/typeCheck.ml

@@ -701,7 +701,7 @@ let typecheck_instr
           res_typestate := pvar_apply loc (handle_pvar ann b) !res_typestate pvar in
 
         let handle_negated_condition cond_node =
-          let do_instr = function
+          let do_instr = (function
               | Sil.Prune (Exp.BinOp (Binop.Eq, _cond_e, Exp.Const (Const.Cint i)), _, _, _)
               | Sil.Prune (Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), _cond_e), _, _, _)
                 when IntLit.iszero i ->
@@ -712,7 +712,7 @@ let typecheck_instr
                         set_flag pvar' AnnotatedSignature.Nullable false
                     | _ -> ()
                   end
-            | _ -> () in
+              | _ -> ()) [@warning "-57"] (* FIXME: silenced warning may be legit *) in
           List.iter ~f:do_instr (Procdesc.Node.get_instrs cond_node) in
         let handle_optional_isPresent node' e =
           match convert_complex_exp_to_pvar node' false e typestate' loc with
@@ -1028,7 +1028,7 @@ let typecheck_instr
               pvar_apply loc handle_pvar typestate2 pvar
           | _ -> typestate2 in
 
-        match c with
+        begin match c with
           | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e)
           | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
               typecheck_expr_for_errors typestate e loc;
@@ -1112,7 +1112,8 @@ let typecheck_instr
               check_condition node' (Exp.BinOp (Binop.Ne, e1, e2))
           | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Ne, e1, e2)), _) ->
               check_condition node' (Exp.BinOp (Binop.Eq, e1, e2))
-        | _ -> typestate in
+          | _ -> typestate
+        end [@warning "-57"] (* FIXME: silenced warning may be legit *) in
 
       (* Handle assigment fron a temp pvar in a condition.
          This recognizes the handling of temp variables in ((x = ...) != null) *)