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

src/analyses/wp_analyses/liveness.ml

@@ -0,0 +1,191 @@
+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, _ -> 
+      if (D.mem v man.local || v.vglob) then ( (* Global variables are considered live when writing to them. *)
+        let rval_vars = D.of_list (vars_from_expr rval man_forw)
+        in
+        D.union rval_vars (D.diff man.local (D.singleton v))
+      ) 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, _ -> 
+      let may_point_to = Queries.AD.to_var_may (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
+
+      match may_point_to with  (*POSSIBLY UNSOUND: could also be an overapproximation, depending on whether assumption is true*)
+      | [v] ->
+        D.union (assign  man man_forw (Var v, NoOffset) rval) lval_vars  (* We assume that if it my only point to one variable, we can treat this as if we just assigned to that variable*)
+      | _ ->  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) =
+
+    match lval with
+    | Some (Var v, _) -> 
+      if (D.mem v man.local) then ( 
+        [man.local, (D.singleton v)]
+      ) else (
+        [man.local, D.empty()]
+      )
+    | Some (Mem exp, _) -> [man.local, D.of_list (vars_from_expr exp man_forw)] 
+    | None -> [man.local, D.empty()]
+
+  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 -> D.empty()
+    | Some e -> if return_val_is_important
+      then D.of_list (vars_from_expr e man_forw)
+      else D.empty()
+
+
+  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
+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/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

src/framework/backwAnalyses.ml

@@ -0,0 +1,167 @@
+open GoblintCil
+open Analyses
+
+module M  = Messages
+
+module type BackwSpec = 
+sig
+  module D : Lattice.S
+  module G : Lattice.S
+  module C : Printable.S
+  module V: SpecSysVar (** Global constraint variables. *)
+  module P: DisjointDomain.Representative with type elt := D.t (** Path-representative. *)
+
+  module D_forw: Lattice.S
+  module G_forw: Lattice.S 
+  module V_forw: SpecSysVar (** Global constraint variables. *)
+  module P_forw: DisjointDomain.Representative with type elt := D_forw.t (* Path-representative. *)
+  val name : unit -> string
+
+  (** Auxiliary data (outside of solution domains) that needs to be marshaled and unmarshaled.
+      This includes:
+      * hashtables,
+      * varinfos (create_var),
+      * RichVarinfos. *)
+  type marshal
+
+  (** Initialize using unmarshaled auxiliary data (if present). *)
+  val init : marshal option -> unit
+
+  (** Finalize and return auxiliary data to be marshaled. *)
+  val finalize : unit -> marshal
+  (* val finalize : G.t -> unit *)
+
+  val startstate : varinfo -> D.t
+  val morphstate : varinfo -> D.t -> D.t
+  val exitstate  : varinfo -> D.t
+
+  val context: (D_forw.t, G_forw.t, C.t, V_forw.t) man -> fundec -> D_forw.t -> C.t 
+  val startcontext: unit -> C.t
+
+  val sync  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return] -> D.t
+  val query : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> 'a Queries.t -> 'a Queries.result
+
+  (** A transfer function which handles the assignment of a rval to a lval, i.e.,
+      it handles program points of the form "lval = rval;" *)
+  val assign: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval -> exp -> D.t
+
+  (** A transfer function used for declaring local variables.
+      By default only for variable-length arrays (VLAs). *)
+  val vdecl : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> varinfo -> D.t
+
+  (** A transfer function which handles conditional branching yielding the
+      truth value passed as a boolean argument *)
+  val branch: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> exp -> bool -> D.t
+
+  (** A transfer function which handles going from the start node of a function (fundec) into
+      its function body. Meant to handle, e.g., initialization of local variables *)
+  val body  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> fundec -> D.t
+
+  (** A transfer function which handles the return statement, i.e.,
+      "return exp" or "return" in the passed function (fundec) *)
+  val return: (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> exp option  -> fundec -> D.t
+
+  (** A transfer function meant to handle inline assembler program points *)
+  val asm   : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t
+
+  (** A transfer function which works as the identity function, i.e., it skips and does nothing.
+      Used for empty loops. *)
+  val skip  : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t
+
+  (** A transfer function which, for a call to a {e special} function f "lval = f(args)" or "f(args)",
+      computes the caller state after the function call *)
+  val special : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> varinfo -> exp list -> D.t
+
+  (** For a function call "lval = f(args)" or "f(args)",
+      [enter] returns a caller state, and the initial state of the callee.
+      In [enter], the caller state can usually be returned unchanged, as [combine_env] and [combine_assign] (below)
+      will compute the caller state after the function call, given the return state of the callee *)
+  val enter   : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> fundec -> exp list -> (D.t * D.t) list
+
+  (* Combine is split into two steps: *)
+
+  (** Combine environment (global variables, mutexes, etc)
+      between local state (first component from enter) and function return.
+
+      This shouldn't yet assign to the lval. *)
+  val combine_env : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+
+  (** Combine return value assignment
+      to local state (result from combine_env) and function return.
+
+      This should only assign to the lval. *)
+  val combine_assign : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+
+  (* Paths as sets: I know this is ugly! *)
+  val paths_as_set : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> D.t list
+
+  (** Returns initial state for created thread. *)
+  val threadenter : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
+
+  (** Updates the local state of the creator thread using initial state of created thread. *)
+  val threadspawn : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> multiple:bool -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) man -> D.t
+
+  val event : (D.t, G.t, C.t, V.t) man -> (D_forw.t, G_forw.t, C.t, V_forw.t) man -> Events.t -> (D.t, G.t, C.t, V.t) man -> D.t
+end
+
+module type BackwSpecSpec = functor (ForwSpec : Analyses.Spec) -> sig
+  include BackwSpec 
+    with module C = ForwSpec.C
+    with module D_forw = ForwSpec.D
+    with module G_forw = ForwSpec.G
+    with module V_forw = ForwSpec.V
+    with module P_forw = ForwSpec.P  
+end
+
+module DefaultBackwSpec (ForwSpec : Analyses.Spec) =
+struct
+  module G = Lattice.Unit
+  module C = ForwSpec.C
+  module V = EmptyV
+  module P = EmptyP
+
+  module D_forw: Lattice.S = ForwSpec.D
+  module G_forw: Lattice.S = ForwSpec.G
+  module V_forw: SpecSysVar = ForwSpec.V (** Global constraint variables. *)
+  module P_forw: DisjointDomain.Representative with type elt := ForwSpec.D.t = ForwSpec.P (*Path-representative.*)
+
+  type marshal = unit
+  let init _ = ()
+
+  (* This means it does not matter which Spec's context function we use in control and BidirFromSpec. 
+   * For understandability in other parts of the code the context-function of the forward spec should be used explicitely*)
+
+  let context = ForwSpec.context 
+  let startcontext _ =  ForwSpec.startcontext ()
+  let finalize () = ()
+  (* no inits nor finalize -- only analyses like Mutex, Base, ... need
+     these to do postprocessing or other imperative hacks. *)
+
+  let vdecl man _ _ = man.local
+
+  let asm x _ =
+    M.msg_final Info ~category:Unsound "ASM ignored";
+    M.info ~category:Unsound "ASM statement ignored.";
+    x.local (* Just ignore. *)
+
+  let skip x _ = x.local (* Just ignore. *)
+
+  let query _ _ (type a) (q: a Queries.t) = Queries.Result.top q
+  (* Don't know anything --- most will want to redefine this. *)
+
+  let event man _ _ _ = man.local
+
+  let morphstate v d = d
+  (* Only for those who track thread IDs. *)
+
+  let sync man _ _ = man.local
+  (* Most domains do not have a global part. *)
+
+  (* let context man _ fd x = x *)
+  (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
+
+  let paths_as_set man _ = [man.local]
+
+  (* module A = UnitA *)
+  (* let access _ _ = () *)
+end