mod_checker.ml

open! Utils

module F = Format
module L = Logging

(** backward analysis for computing set of maybe-live variables at each program point *)

module Domain = AbstractDomain.FiniteSet(Var.Set)

(* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is
   read, kill the variable when it is assigned *)
module TransferFunctions (CFG : ProcCfg.S) = struct
  module CFG = CFG
  module Domain = Domain
  type extras = ProcData.no_extras

  let rec contains_mod_exp = function
    | Exp.Binop (Binop.Mod, _, _) -> true
    | Exp.Binop (_, e1, e2) | Lindex (e1, e2) -> contains_mod_exp e1 || contains_mod_exp e2
    | Unop e | Lfield (e, _, _) -> contains_mod_exp e
    | _ -> false
    
  let exec_instr astate _ _ = function
    | Sil.Letderef (lhs_id, rhs_exp, _, _) ->
        Domain.remove (Var.of_id lhs_id) astate
        |> contains_mod_exp
    | Sil.Set (Lvar lhs_pvar, _, rhs_exp, _) ->
        let astate' =
          if Pvar.is_global lhs_pvar
          then astate (* never kill globals *)
          else Domain.remove (Var.of_pvar lhs_pvar) astate in
        contains_mod_exp
    | Sil.Set (lhs_exp, _, rhs_exp, _) ->
        contains_mod_exp
        |> contains_mod_exp
    | Sil.Prune (exp, _, _, _) ->
        contains_mod_exp
    | Sil.Call (ret_ids, call_exp, params, _, _) ->
        IList.fold_right
          (fun ret_id astate_acc -> Domain.remove (Var.of_id ret_id) astate_acc)
          ret_ids
          astate
        |> contains_mod_exp
        |> IList.fold_right contains_mod_exp (IList.map fst params)
    | Sil.Declare_locals _ | Stackop _ | Remove_temps _ | Abstract _ | Nullify _ ->
        astate
end

module Analyzer =
  AbstractInterpreter.Make
    (ProcCfg.Backward(ProcCfg.Exceptional))
    (Scheduler.ReversePostorder)
    (TransferFunctions)

let checker { Callbacks.proc_desc; tenv; } =
  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))