Merge branch 'master' into master

Author: dabund24

src/arg/argTools.ml

@@ -137,19 +137,6 @@ struct
       | Statement stmt  -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str
       | Function f      -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
       | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
-
-    (* TODO: less hacky way (without ask_indices) to move node *)
-    let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c)))
-    let move_opt (n, c, i) to_n =
-      match ask_indices (to_n, c) with
-      | [] -> None
-      | [to_i] ->
-        let to_node = (to_n, c, to_i) in
-        BatOption.filter is_live (Some to_node)
-      | _ :: _ :: _ ->
-        failwith "Node.move_opt: ambiguous moved index"
-    let equal_node_context (n1, c1, i1) (n2, c2, i2) =
-      EQSys.LVar.equal (n1, c1) (n2, c2)
   end
 
   module NHT = BatHashtbl.Make (Node)

src/arg/myARG.ml

@@ -12,22 +12,19 @@ sig
   val context_id: t -> int
   val path_id: t -> int
   val to_string: t -> string
-
-  val move_opt: t -> MyCFG.node -> t option
-  val equal_node_context: t -> t -> bool
 end
 
 module type Edge =
 sig
-  type t
+  type t [@@deriving eq, ord]
 
   val embed: MyCFG.edge -> t
   val to_string: t -> string
 end
 
 module CFGEdge: Edge with type t = MyCFG.edge =
 struct
-  type t = edge
+  type t = Edge.t [@@deriving eq, ord]
 
   let embed e = e
   let to_string e = GobPretty.sprint Edge.pretty_plain e
@@ -102,7 +99,7 @@ end
 
 module InlineEdge: Edge with type t = inline_edge =
 struct
-  type t = inline_edge
+  type t = inline_edge [@@deriving eq, ord]
 
   let embed e = CFGEdge e
   let to_string e = InlineEdgePrintable.show e
@@ -130,15 +127,6 @@ struct
     nl
     |> List.map Node.to_string
     |> String.concat "@"
-
-  let move_opt nl to_node =
-    let open GobOption.Syntax in
-    match nl with
-    | [] -> None
-    | n :: stack ->
-      let+ to_n = Node.move_opt n to_node in
-      to_n :: stack
-  let equal_node_context _ _ = failwith "StackNode: equal_node_context"
 end
 
 module Stack (Arg: S with module Edge = InlineEdge):
@@ -265,16 +253,19 @@ struct
     end
 end
 
+type cfg_path = (MyCFG.edge * MyCFG.node) list
 
 module type SIntra =
 sig
-  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node) list
+  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * cfg_path list) list
+  (** @return Also the original CFG paths corresponding to the step. *)
 end
 
 module type SIntraOpt =
 sig
   include SIntra
-  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node) list) option
+  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * cfg_path list) list) option
+  (** @return Also the original CFG paths corresponding to the step. *)
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =
@@ -283,51 +274,38 @@ struct
     let open GobList.Syntax in
     let* (es, to_n) = Cfg.next node in
     let+ (_, e) = es in
-    (e, to_n)
+    (e, to_n, [[(e, to_n)]])
   let next_opt _ = None
 end
 
-let partition_if_next if_next_n =
-  (* TODO: refactor, check extra edges for error *)
-  let test_next b = List.find (function
-      | (Test (_, b'), _) when b = b' -> true
-      | (_, _) -> false
-    ) if_next_n
+let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps
+
+let partition_if_next if_next =
+  let (if_next_trues, if_next_falses) = List.partition (function
+      | (Test (_, b), _, _) -> b
+      | (_, _, _) -> failwith "partition_if_next: not Test edge"
+    ) if_next
   in
-  (* assert (List.length if_next <= 2); *)
-  match test_next true, test_next false with
-  | (Test (e_true, true), if_true_next_n), (Test (e_false, false), if_false_next_n) when Basetype.CilExp.equal e_true e_false ->
-    (e_true, if_true_next_n, if_false_next_n)
-  | _, _ -> failwith "partition_if_next: bad branches"
+  match if_next_trues, if_next_falses with
+  | [(Test (e_true, true), if_true_next_n, if_true_next_ps)], [(Test (e_false, false), if_false_next_n, if_false_next_ps)] when Basetype.CilExp.equal e_true e_false ->
+    (e_true, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps))
+  | _, _ ->
+    (* This fails due to any of the following:
+       - Either true or false branch is missing.
+       - Either true or false branch has multiple different exps or nodes (same exp, branch and node should only occur once by construction/assumption).
+       - True and false branch have different exps. *)
+    failwith "partition_if_next: bad branches"
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
   open Cil
-  (* TODO: questionable (=) and (==) use here *)
-
-  let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with
-    | Instr is1, Instr is2 -> GobList.equal (=) is1 is2
-    | Return _, Return _ -> sk1 = sk2
-    | _, _ -> false (* TODO: also consider others? not sure if they ever get duplicated *)
-  let is_equiv_stmt s1 s2 = is_equiv_stmtkind s1.skind s2.skind (* TODO: also consider labels *)
-  let is_equiv_node n1 n2 = match n1, n2 with
-    | Statement s1, Statement s2 -> is_equiv_stmt s1 s2
-    | _, _ -> false (* TODO: also consider FunctionEntry & Function? *)
-  let is_equiv_edge e1 e2 = match e1, e2 with
-    | Entry f1, Entry f2 -> f1 == f2 (* physical equality for fundec to avoid cycle *)
-    | Ret (exp1, f1), Ret (exp2, f2) -> exp1 = exp2 && f1 == f2 (* physical equality for fundec to avoid cycle *)
-    | _, _ -> e1 = e2
-  let rec is_equiv_chain n1 n2 =
-    Node.equal n1 n2 || (is_equiv_node n1 n2 && is_equiv_chain_next n1 n2)
-  and is_equiv_chain_next n1 n2 = match Arg.next n1, Arg.next n2 with
-    | [(e1, to_n1)], [(e2, to_n2)] ->
-      is_equiv_edge e1 e2 && is_equiv_chain to_n1 to_n2
-    | _, _-> false
 
+  let () =
+    assert (not !Cabs2cil.allowDuplication) (* duplication makes it more annoying to detect cilling *)
 
   let rec next_opt' n = match n with
     | Statement {sid; skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
-      let (e, if_true_next_n,  if_false_next_n) = partition_if_next (Arg.next n) in
+      let (e, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = partition_if_next (Arg.next n) in
       (* avoid infinite recursion with sid <> sid2 in if_nondet_var *)
       (* TODO: why physical comparison if_false_next_n != n doesn't work? *)
       (* TODO: need to handle longer loops? *)
@@ -336,24 +314,24 @@ struct
         (* && *)
         | Statement {sid=sid2; skind=If _; _}, _ when sid <> sid2 && CilType.Location.equal loc (Node.location if_true_next_n) ->
           (* get e2 from edge because recursive next returns it there *)
-          let (e2, if_true_next_true_next_n, if_true_next_false_next_n) = partition_if_next (next if_true_next_n) in
-          if is_equiv_chain if_false_next_n if_true_next_false_next_n then
+          let (e2, (if_true_next_true_next_n, if_true_next_true_next_ps), (if_true_next_false_next_n, if_true_next_false_next_ps)) = partition_if_next (next if_true_next_n) in
+          if Node.equal if_false_next_n if_true_next_false_next_n then
             let exp = BinOp (LAnd, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_true_next_n);
-              (Test (exp, false), if_false_next_n)
+              (Test (exp, true), if_true_next_true_next_n, cartesian_concat_paths if_true_next_ps if_true_next_true_next_ps);
+              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_concat_paths if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
             ]
           else
             None
         (* || *)
         | _, Statement {sid=sid2; skind=If _; _} when sid <> sid2 && CilType.Location.equal loc (Node.location if_false_next_n) ->
           (* get e2 from edge because recursive next returns it there *)
-          let (e2, if_false_next_true_next_n, if_false_next_false_next_n) = partition_if_next (next if_false_next_n) in
-          if is_equiv_chain if_true_next_n if_false_next_true_next_n then
+          let (e2, (if_false_next_true_next_n, if_false_next_true_next_ps), (if_false_next_false_next_n, if_false_next_false_next_ps)) = partition_if_next (next if_false_next_n) in
+          if Node.equal if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_n);
-              (Test (exp, false), if_false_next_false_next_n)
+              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
+              (Test (exp, false), if_false_next_false_next_n, cartesian_concat_paths if_false_next_ps if_false_next_false_next_ps)
             ]
           else
             None
@@ -381,14 +359,14 @@ struct
 
   let next_opt' n = match n with
     | Statement {skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
-      let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in
+      let (e_cond, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = partition_if_next (Arg.next n) in
       let loc = Node.location n in
       if CilType.Location.equal (Node.location if_true_next_n) loc && CilType.Location.equal (Node.location if_false_next_n) loc then
         match Arg.next if_true_next_n, Arg.next if_false_next_n with
-        | [(Assign (v_true, e_true), if_true_next_next_n)], [(Assign (v_false, e_false), if_false_next_next_n)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
+        | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_ps)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_ps)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
           let exp = ternary e_cond e_true e_false in
           Some [
-            (Assign (v_true, exp), if_true_next_next_n)
+            (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_next_ps) (* concat two different path families with same variable to same node *)
           ]
         | _, _ -> None
       else
@@ -407,14 +385,30 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
+  (** Starting from ARG node [node], follow CFG path [p] to the resulting ARG node.
+      Returns multiple ARG nodes if ARG contains path-sensitivity splits on the same CFG path. *)
+  let rec follow node p =
+    let open GobList.Syntax in
+    match p with
+    | [] -> [node]
+    | (e, to_n) :: p' ->
+      let* (_, node') = List.filter (fun (e', to_node) ->
+          Edge.equal (Edge.embed e) e' && Node0.equal to_n (Node.cfgnode to_node)
+        ) (Arg.next node)
+      in
+      follow node' p'
+
   let next node =
-    let open GobOption.Syntax in
+    let open GobList.Syntax in
     match ArgIntra.next_opt (Node.cfgnode node) with
     | None -> Arg.next node
     | Some next ->
       next
-      |> BatList.filter_map (fun (e, to_n) ->
-          let+ to_node = Node.move_opt node to_n in
+      |> BatList.concat_map (fun (e, to_n, p) ->
+          let* p in
+          let+ to_node = follow node p in
+          assert (Node0.equal to_n (Node.cfgnode to_node)); (* should always hold by follow filter above *)
           (Edge.embed e, to_node)
         )
+      |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* after following paths, there may be duplicates because same ARG node can be reached via same ARG edge via multiple uncilled CFG paths *) (* TODO: avoid generating duplicates in the first place? *)
 end

src/cdomains/apron/gobApron.apron.ml

@@ -19,6 +19,14 @@ module Coeff =
 struct
   include Coeff
 
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let s_of_z z = Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
 end
 

src/cdomains/apron/sharedFunctions.apron.ml

@@ -41,6 +41,10 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
     | _ ->
       failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
+let int_of_coeff ?scalewith ?round (coeff: Coeff.union_5) =
+  match coeff with
+  | Scalar scalar -> int_of_scalar ?scalewith ?round scalar
+  | Interval _ -> None
 
 module type ConvertArg =
 sig
@@ -269,37 +273,44 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
+  let int_of_coeff_warn ~scalewith coeff =
+    match int_of_coeff ~scalewith coeff with
+    | Some i -> i
+    | None ->
+      M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty coeff;
+      raise Unsupported_Linexpr1
 
   (** Returned boolean indicates whether returned expression should be negated. *)
-  let coeff_to_const ~scalewith (c:Coeff.union_5) =
-    match c with
-    | Scalar c ->
-      (match int_of_scalar ?scalewith c with
-       | Some i ->
-         let ci,truncation = truncateCilint ILongLong i in
-         if truncation = NoTruncation then
-           if Z.compare i Z.zero >= 0 then
-             false, Const (CInt(i,ILongLong,None))
-           else
-             (* attempt to negate if that does not cause an overflow *)
-             let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
-             if truncation = NoTruncation then
-               true, Const (CInt((Z.neg i),ILongLong,None))
-             else
-               false, Const (CInt(i,ILongLong,None))
-         else
-           (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
-       | None -> raise Unsupported_Linexpr1)
-    | _ -> raise Unsupported_Linexpr1
+  let cil_exp_of_int i =
+    let ci,truncation = truncateCilint ILongLong i in
+    if truncation = NoTruncation then
+      if Z.compare i Z.zero >= 0 then
+        false, Const (CInt(i,ILongLong,None))
+      else
+        (* attempt to negate if that does not cause an overflow *)
+        let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
+        if truncation = NoTruncation then
+          true, Const (CInt((Z.neg i),ILongLong,None))
+        else
+          false, Const (CInt(i,ILongLong,None))
+    else
+      raise Unsupported_Linexpr1
 
   (** Returned boolean indicates whether returned expression should be negated. *)
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
-      let flip, coeff = coeff_to_const ~scalewith c in
-      let prod = BinOp(Mult, coeff, var, longlong) in
-      flip, prod
+      let i = int_of_coeff_warn ~scalewith c in
+      if Z.equal i Z.one then
+        false, var
+      else if Z.equal i Z.minus_one then
+        true, var
+      else (
+        let flip, coeff = cil_exp_of_int i in
+        let prod = BinOp(Mult, coeff, var, longlong) in
+        flip, prod
+      )
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
@@ -308,8 +319,14 @@ struct
       raise Unsupported_Linexpr1
 
   (** Returned booleans indicates whether returned expressions should be negated. *)
-  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
+  let cil_exp_of_linexpr1 ~scalewith (linexpr1:Linexpr1.t) =
+    let terms =
+      let c = Linexpr1.get_cst linexpr1 in
+      if Coeff.is_zero c then
+        ref []
+      else
+        ref [cil_exp_of_int (int_of_coeff_warn ~scalewith c)]
+    in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
         terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
@@ -369,7 +386,7 @@ struct
         | DISEQ -> Ne
         | EQMOD _ -> raise Unsupported_Linexpr1
       in
-      Some (Cil.constFold false @@ BinOp(binop, lhs, rhs, TInt(IInt,[]))) (* constFold removes multiplication by factor 1 *)
+      Some (BinOp(binop, lhs, rhs, TInt(IInt,[])))
     with
       Unsupported_Linexpr1 -> None
 end

src/common/util/cilfacade.ml

@@ -90,7 +90,7 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false;
+  Cabs2cil.allowDuplication := false; (* needed for ARG uncilling, maybe something else as well? *)
   Cabs2cil.silenceLongDoubleWarning := true;
   Cabs2cil.addLoopConditionLabels := true
 

src/util/std/gobYaml.ml

@@ -3,7 +3,7 @@ let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v =
   let rec aux len =
     match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with
     | Ok _ as o -> o
-    | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed")) when len < Sys.max_string_length / 2 ->
+    | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed" | "mapping_start failed")) when len < Sys.max_string_length / 2 ->
       aux (len * 2)
     | Error (`Msg _) as e -> e
   in