Fix compilation issues after merge

Author: paveon

infer/src/absint/HilExp.ml

@@ -18,18 +18,15 @@ module Access = MemoryAccess
     We could make only the types of [AddressOf] and [Dereference] private but that proved too
     cumbersome... *)
 module T : sig
-  type sizeof_data = {typ: Typ.t; nbytes: int option; dynamic_length: t option; subtype: Subtype.t}
-
-  and t =
+  type t =
     | AccessExpression of access_expression
     | UnaryOperator of Unop.t * t * Typ.t option
     | BinaryOperator of Binop.t * t * t
     | Exception of t
     | Closure of Procname.t * (AccessPath.base * t) list
     | Constant of Const.t
     | Cast of Typ.t * t
-    | Sizeof of sizeof_data
-  (* | Sizeof of Typ.t * t option *)
+    | Sizeof of Typ.t * t option
 
   and access_expression = private
     | Base of AccessPath.base
@@ -56,18 +53,15 @@ module T : sig
       remove_deref_after_base:bool -> AccessPath.base -> access_expression -> access_expression
   end
 end = struct
-  type sizeof_data = {typ: Typ.t; nbytes: int option; dynamic_length: t option; subtype: Subtype.t}
-
-  and t =
+  type t =
     | AccessExpression of access_expression
     | UnaryOperator of Unop.t * t * Typ.t option
     | BinaryOperator of Binop.t * t * t
     | Exception of t
     | Closure of Procname.t * (AccessPath.base * t) list
     | Constant of Const.t
     | Cast of Typ.t * t
-    | Sizeof of sizeof_data
-  (* | Sizeof of Typ.t * t option *)
+    | Sizeof of Typ.t * t option
 
   and access_expression =
     | Base of AccessPath.base
@@ -170,25 +164,23 @@ and pp fmt = function
       Const.pp Pp.text fmt c
   | Cast (typ, e) ->
       F.fprintf fmt "(%a) %a" (Typ.pp_full Pp.text) typ pp e
-  | Sizeof {typ; dynamic_length} ->
+  | Sizeof (typ, length) ->
       let pp_length fmt = Option.iter ~f:(F.fprintf fmt "[%a]" pp) in
-      F.fprintf fmt "sizeof(%a%a)" (Typ.pp_full Pp.text) typ pp_length dynamic_length
+      F.fprintf fmt "sizeof(%a%a)" (Typ.pp_full Pp.text) typ pp_length length
 
 
 let get_access_exprs exp0 =
   let rec get_access_exprs_ exp acc =
     match exp with
     | AccessExpression ae ->
         ae :: acc
-    | Cast (_, e) | UnaryOperator (_, e, _) | Exception e ->
+    | Cast (_, e) | UnaryOperator (_, e, _) | Exception e | Sizeof (_, Some e) ->
         get_access_exprs_ e acc
-    | Sizeof {dynamic_length} ->
-        Option.value_map dynamic_length ~default:acc ~f:(fun e -> get_access_exprs_ e acc)
     | BinaryOperator (_, e1, e2) ->
         get_access_exprs_ e1 acc |> get_access_exprs_ e2
     | Closure (_, captured) ->
         List.fold captured ~f:(fun acc (_, e) -> get_access_exprs_ e acc) ~init:acc
-    | Constant _ ->
+    | Constant _ | Sizeof _ ->
         acc
   in
   get_access_exprs_ exp0 []
@@ -239,6 +231,10 @@ module AccessExpression = struct
         get_base ae
 
 
+  let dereference_2 access = dereference access
+
+  let is_base = function Base _ -> true | _ -> false
+
   let lookup_field_type_annot tenv base_typ field_name =
     let lookup = Tenv.lookup tenv in
     Struct.get_field_type_and_annotation ~lookup field_name base_typ
@@ -303,8 +299,8 @@ module AccessExpression = struct
             fold_vars_exp exp ~init ~f )
     | Constant _ ->
         init
-    | Sizeof {dynamic_length} ->
-        fold_vars_exp_opt dynamic_length ~init ~f
+    | Sizeof (_, exp_opt) ->
+        fold_vars_exp_opt exp_opt ~init ~f
 
 
   let truncate = function
@@ -520,14 +516,8 @@ and of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
         Constant c
     | Cast (cast_typ, e) ->
         Cast (cast_typ, of_sil_ e typ)
-    | Sizeof data ->
-        let hil_data : sizeof_data =
-          { typ= data.typ
-          ; nbytes= data.nbytes
-          ; dynamic_length= Option.map ~f:(fun e -> of_sil_ e typ) data.dynamic_length
-          ; subtype= data.subtype }
-        in
-        Sizeof hil_data
+    | Sizeof {typ; dynamic_length} ->
+        Sizeof (typ, Option.map ~f:(fun e -> of_sil_ e typ) dynamic_length)
     | Closure closure ->
         let environment =
           List.map

infer/src/absint/HilExp.mli

@@ -17,8 +17,7 @@ type t =
   | Closure of Procname.t * (AccessPath.base * t) list  (** Name of function + environment *)
   | Constant of Const.t  (** Constants *)
   | Cast of Typ.t * t  (** Type cast *)
-  | Sizeof of sizeof_data
-  (* | Sizeof of Typ.t * t option *)
+  | Sizeof of Typ.t * t option
       (** C-style sizeof(), and also used to treate a type as an expression. Refer to [Exp] module
           for canonical documentation *)
 
@@ -49,6 +48,10 @@ module AccessExpression : sig
 
   val get_base : access_expression -> AccessPath.base
 
+  val dereference_2 : access_expression -> access_expression
+
+  val is_base : access_expression -> bool
+
   val replace_base :
     remove_deref_after_base:bool -> AccessPath.base -> access_expression -> access_expression
 

infer/src/backend/Payloads.ml

@@ -192,7 +192,7 @@ module SQLite = struct
     ; buffer_overrun_checker= lazy (load table ~proc_uid BufferOverrunChecker)
     ; config_impact_analysis= lazy (load table ~proc_uid ConfigImpactAnalysis)
     ; cost= lazy (load table ~proc_uid Cost)
-    ; looper= lazy (load table ~rowid Looper)
+    ; looper= lazy (load table ~proc_uid Looper)
     ; disjunctive_demo= lazy (load table ~proc_uid DisjunctiveDemo)
     ; lab_resource_leaks= lazy (load table ~proc_uid LabResourceLeaks)
     ; litho_required_props= lazy (load table ~proc_uid LithoRequiredProps)

infer/src/looper/EdgeExp.ml

@@ -1323,7 +1323,7 @@ let rec remove_casts_of_consts exp integer_widths =
       then
         match Typ.get_ikind_opt typ with
         | Some ikind ->
-            let type_max_value = Z.((Typ.range_of_ikind integer_widths ikind |> snd) + ~$1) in
+            let type_max_value = Z.((IntegerWidths.range_of_ikind integer_widths ikind |> snd) + ~$1) in
             let value_after_cast = IntLit.of_big_int Z.(type_max_value - IntLit.to_big_int c) in
             Const (Const.Cint value_after_cast)
         | None ->
@@ -2293,7 +2293,7 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~test_resolver ~for
                complex expressions instead of just access expressions
                as it was originally *)
             map_accesses value ~init:None ~f:(fun ae None ->
-                let ae = if add_deref then HilExp.AccessExpression.dereference ae else ae in
+                let ae = if add_deref then HilExp.AccessExpression.dereference_2 ae else ae in
                 (Access (map_formal ae formal_map |> add_accesses), None) )
             |> fst
           in
@@ -2304,7 +2304,7 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~test_resolver ~for
               ValuePair.P (process_value lb, process_value ub) :: acc )
       | None, missing_id ->
           let ae = HilExp.AccessExpression.address_of_base (base_of_id id typ) in
-          let ae = if add_deref then HilExp.AccessExpression.dereference ae else ae in
+          let ae = if add_deref then HilExp.AccessExpression.dereference_2 ae else ae in
           ValuePair.V (Access (map_formal ae formal_map |> add_accesses)) :: acc
           (* match f_resolve_id (Var.of_id id) with
              | Some access_expr ->
@@ -2344,12 +2344,12 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~test_resolver ~for
       | None, missing_id ->
           let access_expr = of_pvar pvar typ in
           let access_expr =
-            if add_deref then HilExp.AccessExpression.dereference access_expr else access_expr
+            if add_deref then HilExp.AccessExpression.dereference_2 access_expr else access_expr
           in
           ValuePair.V (Access (map_formal access_expr formal_map |> add_accesses)) :: acc )
     | Lvar pvar ->
         let ae = of_pvar pvar typ in
-        let ae = if add_deref then HilExp.AccessExpression.dereference ae else ae in
+        let ae = if add_deref then HilExp.AccessExpression.dereference_2 ae else ae in
         ValuePair.V (Access (map_formal ae formal_map |> add_accesses)) :: acc
     | Lfield (root_exp, fld, root_exp_typ) ->
         let add_field_access_expr access_expr =
@@ -2457,7 +2457,7 @@ and of_sil_exp ~include_array_indexes ~f_resolve_id ~test_resolver ~formal_map ~
       | Some value_pair, _ -> (
           let process_value value =
             map_accesses value ~init:None ~f:(fun ae None ->
-                let ae = if add_deref then HilExp.AccessExpression.dereference ae else ae in
+                let ae = if add_deref then HilExp.AccessExpression.dereference_2 ae else ae in
                 let mapped_ae = map_formal ae formal_map in
                 (Access mapped_ae, None) )
             |> fst
@@ -2470,7 +2470,7 @@ and of_sil_exp ~include_array_indexes ~f_resolve_id ~test_resolver ~formal_map ~
       | None, missing ->
           let access_expr = HilExp.AccessExpression.of_id id typ in
           let access_expr =
-            if add_deref then HilExp.AccessExpression.dereference access_expr else access_expr
+            if add_deref then HilExp.AccessExpression.dereference_2 access_expr else access_expr
           in
           ValuePair.V (Access access_expr)
           (* let ae = match f_resolve_id (Var.of_id id) with

infer/src/looper/EdgeExp.mli

@@ -153,7 +153,7 @@ val separate : T.t -> T.t * (Binop.t * IntLit.t) option
 
 val simplify : T.t -> T.t
 
-val remove_casts_of_consts : T.t -> Typ.IntegerWidths.t -> T.t
+val remove_casts_of_consts : T.t -> IntegerWidths.t -> T.t
 
 val evaluate_const_exp : T.t -> IntLit.t option
 

infer/src/looper/GraphConstructor.ml

@@ -382,7 +382,7 @@ let exec_instr :
                   (fun ptr_arg (lb, ub) acc ->
                     debug_log "Side-effect: %a  --->  [%a, %a]@," EdgeExp.pp ptr_arg EdgeExp.pp lb
                       EdgeExp.pp ub ;
-                    let arg_access = HilExp.AccessExpression.dereference (extract_access ptr_arg) in
+                    let arg_access = HilExp.AccessExpression.dereference_2 (extract_access ptr_arg) in
                     let output_bound = EdgeExp.ValuePair.P (lb, ub) in
                     LTS.EdgeData.add_assignment acc arg_access output_bound )
                   call_model.side_effects graph_data.edge_data
@@ -401,7 +401,7 @@ let exec_instr :
     let locals =
       AccessExpressionSet.fold
         (fun access locals_acc ->
-          let access = HilExp.AccessExpression.dereference access in
+          let access = HilExp.AccessExpression.dereference_2 access in
           debug_log "Checking if local: %a@," HilExp.AccessExpression.pp access ;
           let access_base = HilExp.AccessExpression.get_base access in
           let is_formal = AccessPath.BaseSet.mem access_base proc_data.formals in
@@ -839,7 +839,7 @@ let exec_instr :
           (graph_data, proc_data) )
   | Metadata metadata -> (
     match metadata with
-    | VariableLifetimeBegins (pvar, typ, loc) ->
+    | VariableLifetimeBegins {pvar; typ; loc} ->
         debug_log "@[<v4>[VariableLifetimeBegins] %a@,Variable: %a@," Location.pp loc Pvar.pp_value
           pvar ;
         let pvar_base_access = HilExp.AccessExpression.base (AccessPath.base_of_pvar pvar typ) in
@@ -1055,16 +1055,26 @@ let process_split_node node successors predecessors (graph_data, proc_data) =
       (* Check if it is a loop head and add the join node into scope stack *)
       let prev_node = List.hd_exn predecessors in
       let prev_is_loop_head = Procdesc.is_loop_head graph_data.proc_desc prev_node in
-      let node_map =
-        if prev_is_loop_head then Procdesc.NodeMap.add prev_node prune_node graph_data.node_map
-        else Procdesc.NodeMap.add node prune_node graph_data.node_map
+      let current_is_loop_head = Procdesc.is_loop_head graph_data.proc_desc node in
+      let node_map, loop_heads =
+        if prev_is_loop_head then (
+          let node_map = Procdesc.NodeMap.add prev_node prune_node graph_data.node_map in
+          node_map, graph_data.loop_heads
+        ) else if current_is_loop_head then (
+          let loop_heads = prune_node :: graph_data.loop_heads in
+          Procdesc.NodeMap.add node prune_node graph_data.node_map, loop_heads
+        ) else (
+          Procdesc.NodeMap.add node prune_node graph_data.node_map, 
+          graph_data.loop_heads
+        )
       in
       let graph_data =
         { graph_data with
           last_split_info= Some (prune_node, current_if_kind)
         ; last_node= prune_node
         ; edge_data= LTS.EdgeData.default
-        ; node_map }
+        ; node_map
+        ; loop_heads }
       in
       let proc_data =
         { proc_data with

infer/src/looper/LooperCostModels.ml

@@ -24,7 +24,7 @@ module LooperModelEnv = struct
     ; node_hash: int
     ; location: Location.t
     ; tenv: Tenv.t
-    ; integer_type_widths: Typ.IntegerWidths.t
+    ; integer_type_widths: IntegerWidths.t
     ; get_summary: Procname.t -> LooperSummary.t option }
 
   let mk_model_env pname ~node_hash location tenv integer_type_widths get_summary =
@@ -180,7 +180,7 @@ let get_strtoul_model ~of_function arg_pairs widths =
       in
       (complexity, cache)
     in
-    let ret_lb, ret_ub = Typ.range_of_ikind widths Typ.IULong in
+    let ret_lb, ret_ub = IntegerWidths.range_of_ikind widths Typ.IULong in
     let output_bound =
       ( EdgeExp.T.Const (Const.Cint (IntLit.of_big_int ret_lb))
       , EdgeExp.T.Const (Const.Cint (IntLit.of_big_int ret_ub)) )

opam/infer.opam

@@ -51,6 +51,7 @@ depends: [
   "yojson" {>="1.7.0"}
   "zarith" {>="1.12"}
   "why3"
+  "ocaml-lsp-server"
 ]
 build: [
   ["./autogen.sh"]

opam/infer.opam.locked

@@ -43,7 +43,7 @@ depends: [
   "cppo" {= "1.6.9"}
   "csexp" {= "1.5.1"}
   "ctypes" {= "0.20.1"}
-  "dune" {= "3.7.1"}
+  "dune" {= "3.7.0"}
   "dune-configurator" {= "3.7.0"}
   "easy-format" {= "1.3.4"}
   "expect_test_helpers_core" {= "v0.15.0"}
@@ -158,6 +158,7 @@ depends: [
   "zarith" {= "1.12"}
   "why3" {= "1.6.0"}
   "zed" {= "3.2.1"}
+  "ocaml-lsp-server" {= "1.17.0"}
 ]
 build: [
   ["./autogen.sh"]
@@ -170,4 +171,4 @@ depexts: [
   ["default-jdk"] {"ubuntu"}
   ["default-jdk"] {"debian"}
 ]
-dev-repo: "git://github.com/facebook/infer.git"
+dev-repo: "git://github.com/facebook/infer.git"