Bachelor's Thesis – tnilboG: Extending Goblint Analyzer with Weakest Preconditions

src/analyses/wp_analyses/liveness.ml

@@ -0,0 +1,274 @@
+open GoblintCil
+open Analyses
+
+module BackwSpec : BackwAnalyses.BackwSpecSpec = functor (ForwSpec : Analyses.Spec) ->
+struct
+
+  include BackwAnalyses.DefaultBackwSpec (ForwSpec)
+  module C = ForwSpec.C
+
+  (* Adding these module definitions because the "include" of the DefaultBackwSpec is not enough*)
+  module D_forw = ForwSpec.D
+  module G_forw = ForwSpec.G
+  module V_forw = ForwSpec.V
+  module P_forw = ForwSpec.P
+  let name () = "liveness"
+
+  module G = Lattice.Unit
+  module V = EmptyV
+  module P = EmptyP
+
+  module LiveVariableSet =  SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end)
+  module D =  LiveVariableSet (*Set of program variables as domain*)
+
+  let startstate v = D.empty()
+  let exitstate v = D.empty()
+
+  let rec vars_from_lval (l: lval) man_forw : varinfo list  = 
+    let vars_written_to =  
+      match l with
+      | Var v, _ ->  (
+          if (Cil.isFunctionType v.vtype) then [] else [v]  (*I do not want functions in the set of live variables*)
+        )
+      | Mem exp, _ -> (*If a pointer may point to a variable, these variables are live as well...*)
+        let may_point_to = Queries.AD.to_var_may (man_forw.ask (MayPointTo exp)) in
+        if may_point_to = [] then (
+          M.warn ~category:MessageCategory.Unsound "The expression %a may point to an unknown variable. This makes the analysis unsound." d_exp exp; (*UNSOUND: I do not think that this check is enough. Maybe I should just exclude analyzing programs with variables whose address is taken.*)
+          vars_from_expr exp man_forw )
+        else (
+          Logs.debug "(!) The expression %a may point to the variables %s" d_exp exp (String.concat ", " (List.map (fun v -> v.vname) may_point_to));
+          may_point_to @ vars_from_expr exp man_forw)
+    in
+
+    let vars_in_offset = 
+      match l with
+      | Var _, off -> vars_from_offset off man_forw
+      | Mem _, off -> vars_from_offset off man_forw
+    in
+
+    (vars_written_to @ vars_in_offset)
+
+  and vars_from_offset (off: offset) man_forw : varinfo list =
+    match off with
+    | NoOffset -> []
+    | Field (_, off) -> vars_from_offset off man_forw (* what to do with fieldinfo?*)
+    | Index (e, off) -> 
+      let vars_in_e = vars_from_expr e man_forw  in
+      let vars_in_off = vars_from_offset off man_forw in
+      (match vars_in_off with
+       | [] -> []
+       | vars_in_off ->  (vars_in_e @ vars_in_off))
+
+  and vars_from_expr (e: exp) man_forw : varinfo list =
+    let rec aux acc e =
+      match e with
+      | Lval v -> vars_from_lval v man_forw @ acc 
+      | BinOp (_, e1, e2, _)  ->
+        let acc1 = aux acc e1 in
+        aux acc1 e2
+      | UnOp (_, e1, _)       -> aux acc e1
+      | SizeOfE e1            -> aux acc e1
+      | AlignOfE e1           -> aux acc e1
+      | Question (e1, e2, e3, _) -> 
+        let acc1 = aux acc e1 in
+        let acc2 = aux acc1 e2 in
+        aux acc2 e3
+      | CastE (_, e1)         ->   aux acc e1  (*This appears to make problems when building for jobs*)
+      | AddrOf (l1)          ->   (match vars_from_lval l1 man_forw with
+          | [] -> acc
+          |  v -> (v @ acc)
+        )
+      | _ ->  acc 
+
+    in
+    aux [] e
+
+  let rec assign man man_forw (lval:lval) (rval:exp) =
+    match lval with
+    | Var v, offset -> 
+      if (D.mem v man.local) then ( (* Global variables are considered live when writing to them -> No, not anymore. This of course does not wark with concurrent programs, but I am already excluding those. *)
+        let rval_vars = D.of_list (vars_from_expr rval man_forw)in
+        let rval_vars = D.filter (fun v -> not (Cil.isFunctionType v.vtype)) rval_vars in (*remove variables that are just function names*)
+
+        let offset_vars = D.of_list (vars_from_offset offset man_forw) in
+        let base_live =
+          match offset with
+          | NoOffset -> D.diff man.local (D.singleton v)
+          | _ -> man.local
+        in
+
+        D.union rval_vars (D.union offset_vars base_live)
+      ) else (
+        (* let loc = M.Location.Node man.node in *)
+        (* M.warn ~loc:loc ~category:MessageCategory.Program "Unnecessary assignment to variable '%s', as it is not live at this program point." v.vname; *)
+        man.local
+      )
+    | Mem exp, off -> 
+      let ad = man_forw.ask (MayPointTo exp) in
+      let lval_vars = D.of_list (vars_from_expr exp man_forw) in
+      let rval_vars = D.of_list (vars_from_expr rval man_forw) in
+      let rval_vars = D.filter (fun v -> not (Cil.isFunctionType v.vtype)) rval_vars in (*remove variables that are just function names*)
+
+      let strong_target =
+        match off, Queries.AD.to_mval ad with
+        | NoOffset, [(v, `NoOffset)] when Queries.AD.is_element (Queries.AD.Addr.of_mval (v, `NoOffset)) ad -> Some v
+        | _ -> None
+      in
+
+
+      let log_this ()= 
+        Logs.debug "(!) Assignment to memory location %a with may-point-to set [?]" d_exp exp;
+        Logs.debug "Variables in the lval: %s" (String.concat ", " (List.map (fun v -> v.vname) (D.elements lval_vars)));
+        Logs.debug "Variables in the rval: %s" (String.concat ", " (List.map (fun v -> v.vname) (D.elements rval_vars)));
+        match strong_target with
+        | Some v -> Logs.debug "Strong target variable: %s" v.vname
+        | None -> Logs.debug "No strong target variable identified"
+      in
+      log_this (); 
+
+      match strong_target with
+      | Some v ->
+        D.union (assign man man_forw (Var v, NoOffset) rval) lval_vars
+      | None -> D.union rval_vars (D.union lval_vars man.local)
+
+  let branch man man_forw (exp:exp) (tv:bool) =  
+    (* This just randomly asks whether all loops terimante to use getg_forw utilized in man.global *)
+    (* let () =
+       match man_forw.ask(Queries.MustTermAllLoops) with
+       | true -> Logs.debug "MustTermAllLoops is TRUE"
+       | _ -> Logs.debug "MustTermAllLoops is NOT TRUE"
+       in *)
+
+    let branch_irrelevant : bool = (
+      match Queries.eval_bool (Analyses.ask_of_man man_forw) exp with
+      | `Lifted b -> tv <> b
+      | `Bot -> false
+      | `Top -> false
+    )
+    in
+    if branch_irrelevant then (D.of_list (vars_from_expr exp man_forw))
+    else D.join man.local (D.of_list (vars_from_expr exp man_forw))
+
+  let body man man_forw (f:fundec) =
+    man.local
+
+  let enter man man_forw (lval: lval option) (f:fundec) (args:exp list) =
+
+    let global_vars_in_d = D.filter (fun v -> v.vglob) man.local in
+
+    let callee_d = 
+      match lval with
+      | Some (Var v, _) -> 
+        if (D.mem v man.local) then ( 
+          (D.singleton v) 
+        ) else (
+          D.empty()
+        )
+      | Some (Mem exp, _) -> D.of_list (vars_from_expr exp man_forw)
+      | None -> D.empty()
+    in
+
+    [man.local, (D.union callee_d global_vars_in_d)]
+
+
+  let combine_env man man_forw (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+
+    (* map relevant sformals in man.local to the corresponding variables contained in the argument*)
+    let arg_formal_pairs = List.combine args f.sformals in
+    let relevant_arg_vars = 
+      List.fold_left (fun acc (arg_exp, formal_var) ->
+          if D.mem formal_var au then
+            D.join acc (D.of_list(vars_from_expr arg_exp man_forw))
+          else
+            acc
+        ) (D.empty()) arg_formal_pairs
+    in
+
+    (*join relevant*)
+    D.join man.local relevant_arg_vars 
+
+  let combine_assign man man_forw (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =  
+    match lval with 
+    | None -> man.local 
+    | Some l -> assign man man_forw l fexp
+
+  (** A transfer function which handles the return statement, i.e.,
+      "return exp" or "return" in the passed function (fundec) *)
+  let return man man_forw (exp: exp option) (f:fundec) : D.t =
+
+    let return_val_is_important = (not (D.is_bot man.local)) || (String.equal f.svar.vname "main") in
+
+    match exp with
+    | None -> man.local
+    | Some e -> if return_val_is_important
+      then D.of_list (vars_from_expr e man_forw) |> D.union man.local
+      else man.local
+
+
+  let special man man_forw (lval: lval option) (f:varinfo) (arglist:exp list) =
+    (* log when called  *)
+    Logs.debug "(!) Called special for function %s with arguments %s" f.vname (String.concat ", " (List.map (fun e -> Pretty.sprint ~width:80 (d_exp () e)) arglist));
+
+    let desc = LibraryFunctions.find f in 
+    match desc.special arglist with
+    (* Could have some special handeling of library functions here *)
+    | _ ->
+      let argvars = List.fold_left (fun acc arg -> D.union acc (D.of_list (vars_from_expr arg man_forw))) (D.empty()) arglist in 
+      match lval with
+      | None -> D.union man.local argvars
+      | Some (Var v, _) -> D.union (D.diff man.local (D.singleton(v))) argvars
+      | Some (Mem exp, _) -> D.union (D.union argvars (D.of_list (vars_from_expr exp man_forw))) man.local
+
+  let threadenter man man_forw ~multiple lval f args = [man.local]
+  let threadspawn man man_forw ~multiple lval f args fman = man.local
+
+  let query man (type a) man_forw (q: a Queries.t): a Queries.result =
+
+    (* Die recursion ist nicht sauber durchdacht *)
+    let rec is_dead_assign man man_forw (lval:lval) (rval:exp) (is_dead:bool) : (D.t * bool) =
+
+      match lval with
+      | Var v, _ ->
+        Logs.debug "D.mem v man.local is %b" (D.mem v man.local);
+        Logs.debug "v.glob is %b" v.vglob;
+        if (D.mem v man.local) then ( (*I used to care whether a variable is global, I no longer do.*)
+          let rval_vars = D.of_list (vars_from_expr rval man_forw)
+          in
+          (D.union rval_vars (D.diff man.local (D.singleton v)), false)
+        )else (
+          Logs.debug "Variable '%s' is not live at this program point." v.vname;
+          (man.local, true)
+        )
+      | Mem exp, off -> (
+          Logs.debug "lval is expression";
+          let ad = man_forw.ask (MayPointTo exp) in
+          let lval_vars = D.of_list (vars_from_expr exp man_forw) in
+          let rval_vars = D.of_list (vars_from_expr rval man_forw) in
+
+          let strong_target =
+            match off, Queries.AD.to_mval ad with
+            | NoOffset, [(v, `NoOffset)] when Queries.AD.is_element (Queries.AD.Addr.of_mval (v, `NoOffset)) ad -> Some v
+            | _ -> None
+          in
+
+          match strong_target with
+          | Some v ->
+            let rec_assign_result, is_dead = 
+              match (is_dead_assign man man_forw (Var v, NoOffset) rval is_dead) with 
+              | (res, new_is_dead) -> res, new_is_dead
+            in 
+            (D.union rec_assign_result lval_vars, is_dead)
+          | None ->  ((D.union rval_vars (D.union lval_vars man.local)), is_dead)
+        )
+    in 
+
+    let open Queries in
+
+    match q with
+    | IsDeadVar v -> not (D.mem v man.local)
+    | MayBeDeadAssignment lval -> (
+        Logs.debug "Checking if assignment to lval %a may be dead at node %a with local state %a" d_lval lval Node.pretty_trace man.node D.pretty man.local;
+        match is_dead_assign man man_forw lval (Const (CInt (Z.zero, IInt, None))) false with
+        | (_, is_dead) -> Logs.debug "isdead is %b" is_dead ; is_dead )
+    | _ -> Result.top q
+end

src/config/options.schema.json

@@ -1298,6 +1298,13 @@
             }
           },
           "additionalProperties": false
+        },
+         "wp_run": {
+          "title": "ana.wp_run",
+          "description":
+            "Do a wp analysis, in this case the liveness analysis.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

src/domains/queries.ml

@@ -146,6 +146,8 @@ type _ t =
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
+  | IsDeadVar: varinfo -> MayBool.t t (* Whether a variable is dead at a program point, i.e., not read afterwards. *)
+  | MayBeDeadAssignment: lval -> MayBool.t t (* Whether an assignment is dead, i.e., the assigned variable is not read afterwards. *) 
 
 type 'a result = 'a
 
@@ -221,6 +223,8 @@ struct
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
+    | IsDeadVar _ -> (module MayBool)
+    | MayBeDeadAssignment _ -> (module MayBool)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -295,6 +299,8 @@ struct
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
+    | IsDeadVar _ -> MayBool.top ()
+    | MayBeDeadAssignment _ -> MayBool.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -366,6 +372,8 @@ struct
     | Any (MustProtectingLocks _) -> 61
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
+    | Any (IsDeadVar _) -> 64
+    | Any (MayBeDeadAssignment _) -> 65
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -540,6 +548,8 @@ struct
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
+    | Any (IsDeadVar v) -> Pretty.dprintf "IsDeadVar %a" CilType.Varinfo.pretty v
+    | Any (MayBeDeadAssignment s) -> Pretty.dprintf "MayBeDeadAssignment %a" CilType.Lval.pretty s
 end
 
 let to_value_domain_ask (ask: ask) =

src/framework/analyses.ml

@@ -429,9 +429,9 @@ module type SpecSys =
 sig
   module Spec: Spec
   module EQSys: Goblint_constraint.ConstrSys.DemandGlobConstrSys with module LVar = VarF (Spec.C)
-                               and module GVar = GVarF (Spec.V)
-                               and module D = Spec.D
-                               and module G = GVarG (Spec.G) (Spec.C)
+                                                                  and module GVar = GVarF (Spec.V)
+                                                                  and module D = Spec.D
+                                                                  and module G = GVarG (Spec.G) (Spec.C)
   module LHT: BatHashtbl.S with type key = EQSys.LVar.t
   module GHT: BatHashtbl.S with type key = EQSys.GVar.t
 end
@@ -443,4 +443,4 @@ sig
 
   val gh: EQSys.G.t GHT.t
   val lh: SpecSys.Spec.D.t LHT.t (* explicit SpecSys to avoid spurious module cycle *)
-end
+end