MainFunctor (goblint.Goblint_lib.Base.MainFunctor)

Parameters

module Priv : BasePriv.S

module RVEval : BaseDomain.ExpEvaluator with type t = BaseComponents(Priv.D).t

Signature

include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module P = Analyses.UnitP

val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e

val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e

val morphstate : 'a -> 'b -> 'c

val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e list

module A = Analyses.UnitA

val access : 'a -> 'b -> unit

module Dom : sig ... end

type t = Dom.t

module D = Dom

include sig ... end

module C : sig ... end

val startcontext : unit -> D.t

module V : sig ... end

module G : sig ... end

val priv_getg : 
  ([> `Left of 'a ] -> [> `Bot | `Lifted1 of Priv.G.t ]) ->
  'b ->
  Priv.G.t

val priv_sideg : 
  ([> `Left of 'a ] -> [> `Lifted1 of 'b ] -> 'c) ->
  'd ->
  'e ->
  'f

type extra = (GoblintCil.varinfo * Offs.t * bool) list

type store = D.t

type value = VD.t

type address = AD.t

type glob_fun = V.t -> G.t

type glob_diff = (V.t * G.t) list

val name : unit -> string

val startstate : 'a -> store

val exitstate : 'a -> store

val is_privglob : GoblintCil.varinfo -> bool

module VarH : sig ... end

module VarMap : sig ... end

val array_map : GoblintCil.attributes VarMap.t VarH.t Batteries.ref

type marshal = GoblintCil.attributes VarMap.t VarH.t

val array_domain_annotation_enabled : bool lazy_t

val add_to_array_map : 
  GoblintCil.fundec ->
  (GoblintCil.varinfo * VD.t) list ->
  unit

val attributes_varinfo : 
  VarMap.key ->
  GoblintCil.fundec ->
  (GoblintCil.attributes * GoblintCil.attribute list) option

val project_val : 
  ValueDomain.VDQ.t ->
  (GoblintCil.attributes * GoblintCil.attributes) option ->
  PrecisionUtil.int_precision option ->
  VD.t ->
  bool ->
  VD.t

val project : 
  ValueDomain.VDQ.t ->
  PrecisionUtil.int_precision option ->
  CPA.t ->
  GoblintCil.fundec ->
  CPA.t

val heap_var : bool -> ('a, 'b, 'c, 'd) Analyses.ctx -> Basetype.Variables.t

val char_array : (GoblintCil.lval, Batteries.bytes) Batteries.Hashtbl.t

val init : GoblintCil.attributes VarMap.t VarH.t option -> unit

val finalize : unit -> GoblintCil.attributes VarMap.t VarH.t

val iDtoIdx : ID.t -> ID.t

val unop_ID : GoblintCil.unop -> ID.t -> ID.t

val unop_FD : GoblintCil.unop -> FD.t -> value

val evalunop : GoblintCil.unop -> GoblintCil.Cil.typ -> value -> value

val binop_ID : GoblintCil.Cil.ikind -> GoblintCil.binop -> ID.t -> ID.t -> ID.t

val binop_FD : GoblintCil.Cil.fkind -> GoblintCil.binop -> FD.t -> FD.t -> FD.t

val int_returning_binop_FD : GoblintCil.binop -> FD.t -> FD.t -> ID.t

val is_int_returning_binop_FD : GoblintCil.binop -> bool

val evalbinop_base : 
  ctx:('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.binop ->
  GoblintCil.typ ->
  value ->
  GoblintCil.typ ->
  value ->
  GoblintCil.typ ->
  value

val add_offset_varinfo : Addr.Offs.t -> Addr.t -> Addr.t

val sync' : 
  [ `Init
  | `Join
  | `JoinCall of CilType.Fundec.t
  | `Normal
  | `Return
  | `Thread ] ->
  (BaseDomain.BaseComponents(Priv.D).t,
    [> `Bot | `Lifted1 of Priv.G.t ],
    'a,
    [> `Left of Priv.V.t ])
    Analyses.ctx ->
  D.t

val sync : 
  (BaseDomain.BaseComponents(Priv.D).t,
    [> `Bot | `Lifted1 of Priv.G.t ],
    'a,
    [> `Left of Priv.V.t ])
    Analyses.ctx ->
  [< `Init
  | `Join
  | `JoinCall of CilType.Fundec.t
  | `Normal
  | `Return
  | `Thread ] ->
  D.t

val publish_all : 
  (BaseDomain.BaseComponents(Priv.D).t,
    [> `Bot | `Lifted1 of Priv.G.t ],
    'a,
    [> `Left of Priv.V.t ])
    Analyses.ctx ->
  [ `Init
  | `Join
  | `JoinCall of CilType.Fundec.t
  | `Normal
  | `Return
  | `Thread ] ->
  unit

val get_var : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.varinfo ->
  value

val get : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  ?top:VD.t ->
  ?full:bool ->
  store ->
  address ->
  GoblintCil.exp option ->
  value

get st addr returns the value corresponding to addr in st * adding proper dependencies. * For the exp argument it is always ok to put None. This means not using precise information about * which part of an array is involved.

val get_ptrs : value list -> address list

val reachable_from_value : 
  Queries.ask ->
  value ->
  GoblintCil.typ ->
  string ->
  AD.t

val reachable_from_address : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  address ->
  address

val reachable_vars : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  address list ->
  address list

val drop_non_ptrs : CPA.t -> CPA.t

val drop_ints : CPA.t -> CPA.t

val drop_interval : CPA.t -> CPA.t

val drop_intervalSet : CPA.t -> CPA.t

val context : 'a -> GoblintCil.fundec -> store -> store

val reachable_top_pointers_types : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  AD.t ->
  Queries.TS.t

val eval_rv_ask_evalint : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  VD.t

Evaluate expression using EvalInt query. Base itself also answers EvalInt, so recursion goes indirectly through queries. This allows every subexpression to also meet more precise value from other analyses. Non-integer expression just delegate to next eval_rv function.

val eval_rv_no_ask_evalint : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  value

Evaluate expression without EvalInt query on outermost expression. This is used by base responding to EvalInt to immediately directly avoid EvalInt query cycle, which would return top. Recursive eval_rv calls on subexpressions still go through eval_rv_ask_evalint.

val eval_rv_back_up : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  value

val eval_rv_base : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  value

Evaluate expression structurally by base. This handles constants directly and variables using CPA. Subexpressions delegate to eval_rv, which may use queries on them.

val eval_rv_base_lval : 
  eval_lv:
    (ctx:
       ('a,
         [> `Bot | `Lifted1 of Priv.G.t ] as 'b,
         'c,
         [> `Left of Priv.V.t ] as 'd)
         Analyses.ctx ->
      store ->
      GoblintCil.lval ->
      AD.t) ->
  ctx:('a, 'b, 'c, 'd) Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  GoblintCil.lval ->
  value

val evalbinop : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.binop ->
  e1:GoblintCil.exp ->
  ?t1:GoblintCil.typ ->
  e2:GoblintCil.exp ->
  ?t2:GoblintCil.typ ->
  GoblintCil.typ ->
  value

val evalbinop_mustbeequal : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.binop ->
  e1:GoblintCil.exp ->
  ?t1:GoblintCil.typ ->
  e2:GoblintCil.exp ->
  ?t2:GoblintCil.typ ->
  GoblintCil.typ ->
  value

Evaluate BinOp using MustBeEqual query as fallback.

val eval_fv : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  AD.t

val eval_tv : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  AD.t

val eval_int : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  ValueDomain.ID.t

val convert_offset : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.offset ->
  VD.offs

val eval_lv : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.lval ->
  AD.t

val eval_rv_keep_bot : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  value

val eval_rv : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  value

val query_evalint : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  [> `Bot | `Lifted of ValueDomain.ID.t | `Top ]

val eval_exp : store -> GoblintCil.exp -> ValueDomain.ID.int_t option

val eval_funvar : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.exp ->
  ValueDomain.AD.t

val eval_rv_address : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp ->
  VD.t

Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway.

val is_not_alloc_var : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.varinfo ->
  bool

val is_not_heap_alloc_var : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.varinfo ->
  bool

val query_invariant : 
  (Priv.D.t BaseDomain.basecomponents_t,
    [> `Bot | `Lifted1 of Priv.G.t ],
    'a,
    [> `Left of Priv.V.t ])
    Analyses.ctx ->
  Invariant.context ->
  Invariant.t

val query_invariant_global : 
  ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  [< `Left of Priv.V.t | `Right of 'c ] ->
  Invariant.t

val exp_may_signed_overflow : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp ->
  BoolDomain.MayBool.t

This query returns false if the expression exp will definitely not result in an overflow.

Each subexpression is analyzed to see if an overflow happened. For each operator in the expression, we use the query EvalInt to approximate the bounds of each operand and we compute if in the worst case there could be an overflow.

For now we return true if the expression contains a shift left.

val lval_may_signed_overflow : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval ->
  BoolDomain.MayBool.t

val query : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  'a Q.t ->
  'a0 Q.result

val update_variable : 
  GoblintCil.varinfo ->
  GoblintCil.typ ->
  CPA.value ->
  CPA.t ->
  CPA.t

val add_partitioning_dependencies : 
  GoblintCil.varinfo ->
  VD.t ->
  store ->
  store

Add dependencies between a value and the expression it (or any of its contents) are partitioned by

val set : 
  ctx:
    (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  ?invariant:bool ->
  ?blob_destructive:bool ->
  ?lval_raw:GoblintCil.lval ->
  ?rval_raw:GoblintCil.exp ->
  ?t_override:GoblintCil.Cil.typ ->
  store ->
  AD.t ->
  GoblintCil.Cil.typ ->
  value ->
  store

set st addr val returns a state where addr is set to val * it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining * precise information about arrays.

val set_many : 
  ctx:
    (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  (AD.t * GoblintCil.Cil.typ * value) list ->
  store

val rem_many : 'a -> store -> GoblintCil.varinfo list -> store

val rem_many_partitioning : 
  ValueDomain.VDQ.t ->
  store ->
  GoblintCil.varinfo list ->
  store

val is_some_bot : value -> bool

module InvariantEval : sig ... end

module Invariant : sig ... end

val invariant : 
  (InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
  InvariantEval.D.t ->
  GoblintCil.exp ->
  bool ->
  InvariantEval.D.t

val set_savetop : 
  ctx:
    (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  ?lval_raw:GoblintCil.lval ->
  ?rval_raw:GoblintCil.exp ->
  store ->
  AD.t ->
  GoblintCil.typ ->
  VD.t ->
  store

val assign : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  store

val branch : 
  (store, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
  GoblintCil.exp ->
  bool ->
  store

val body : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.fundec ->
  store

val return : 
  (store,
    [> `Bot | `Lifted1 of Priv.G.t | `Lifted2 of VD.t ],
    'a,
    [> `Left of Priv.V.t | `Right of ThreadIdDomain.Thread.t ])
    Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  store

val vdecl : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.varinfo ->
  store

val collect_funargs : 
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  ?warn:bool ->
  store ->
  GoblintCil.exp list ->
  address list

From a list of expressions, collect a list of addresses that they might point to, or contain pointers to.

val collect_invalidate : 
  deep:bool ->
  ctx:
    ('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  ?warn:bool ->
  store ->
  GoblintCil.exp list ->
  address list

val invalidate : 
  must:bool ->
  ?deep:bool ->
  ctx:
    (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
      Analyses.ctx ->
  store ->
  GoblintCil.exp list ->
  store

val make_entry : 
  ?thread:bool ->
  (D.t, G.t, C.t, V.t) Analyses.ctx ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  D.t

val enter : 
  (D.t, G.t, C.t, V.t) Analyses.ctx ->
  'a ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  (D.t * D.t) list

val forkfun : 
  (D.t, G.t, C.t, V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  (GoblintCil.lval option * GoblintCil.varinfo * GoblintCil.exp list * bool)
    list

val assert_fn : 
  (InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
  GoblintCil.exp ->
  bool ->
  InvariantEval.D.t

val special_unknown_invalidate : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  CilType.Varinfo.t ->
  LibraryDesc.Cil.Cil.exp list ->
  store

val check_invalid_mem_dealloc : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.varinfo ->
  GoblintCil.exp ->
  unit

val points_to_heap_only : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp ->
  bool

val get_size_of_ptr_target : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp ->
  ValueDomainQueries.ID.t Queries.result

val special : 
  (store, G.t, C.t, V.t) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  store

val combine_st : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  store ->
  store ->
  AD.t ->
  store

val combine_env : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  'b ->
  'c ->
  GoblintCil.fundec ->
  'd ->
  'e ->
  D.t ->
  Queries.ask ->
  Priv.D.t Goblint_lib__BaseDomain.basecomponents_t

val combine_assign : 
  (store, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ])
    Analyses.ctx ->
  GoblintCil.lval option ->
  'b ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'c ->
  D.t ->
  Q.ask ->
  D.t

val threadenter : 
  (D.t, G.t, C.t, V.t) Analyses.ctx ->
  multiple:'a ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  D.t list

val threadspawn : 
  (BaseDomain.BaseComponents(Priv.D).t,
    [> `Bot | `Lifted1 of Priv.G.t ],
    'a,
    [> `Left of Priv.V.t ])
    Analyses.ctx ->
  multiple:'b ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  ('c, 'd, 'e, 'f) Analyses.ctx ->
  D.t

val unassume : 
  (D.t,
    [ `Bot | `Lifted1 of Priv.G.t | `Lifted2 of VD.t | `Top ],
    'a,
    [ `Left of Priv.V.t | `Right of ThreadIdDomain.thread ])
    Analyses.ctx ->
  GoblintCil.exp ->
  WideningTokens.TS.elt list ->
  D.t

val event : 
  (store, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
  Events.t ->
  'b ->
  BaseDomain.BaseComponents(Priv.D).t