Module `Checker.ComputeConstraint`

the module holding constraint generation primitives of the borrow checker. It contains the first phase of the borrow checker, as well as several utilities used by later phases.

Constraints computed in this module are divided into two kinds:

flow-insensitive/persistent constraints. These constraints hold at any program point (more precisely, it does not matter to assume that they hold at any program point), so we can compute them only once, and store them globally (in constraint_info).
In the borrow checker, constraints are never deleated, since assignment is handled using change of type. So flow-insensitive constraints are exactly those constraints that hold immediately after related locations are introduced.
flow-sensitive constraints are those constraints that appear dynamically during program execution, usually due to assignment to a mutable borrow. Function calls can introduce flow-sensitive constraints too, by assigning to its borrow arguments.
Usually there are fewer flow sensitive constraints than insensitive ones, and they are computed multiple times instead of computed once and stored somewhere (because we need to store a constraint set for every IR node to achieve enough precision).

module L = Location

type block_info = { param_typ : Type.typ; overwrites : Type.typ IR.VarMap.t; flow_constrs : L.ConstrSet.t; scope : IR.variable list; }

overwrites stores change in type of variables due to assignment. When a variable is not present in overwrites, its type default to that of variables of constraint_info
flow_constrs stores the flow-sensitive constraints at the beginning of a block. For loop blocks, the stored constraint set is the fixed point of looping for zero or more times.
scope is the set of variables that are in-scope in the body of the block. Only those variables that corresponds to source variables (i.e. whose IR.var_kind is IR.SrcVar) are counted

type constraint_info = { functions : (string, Type.function_typ) Stdlib.Hashtbl.t; variables : (IR.variable, Type.typ) Stdlib.Hashtbl.t; blocks : (IR.label, block_info) Stdlib.Hashtbl.t; mutable constrs : L.ConstrSet.t; }: constraints store the global set of flow-insensitive constraints during the checking of a complete program.

val make_constraint_info : unit -> constraint_info
val merge_block_info : constraint_info -> block_info -> block_info -> block_info
val merge_info_into_block : constraint_info -> IR.label -> block_info -> unit
val find_var : constraint_info -> Type.typ IR.VarMap.t -> IR.VarMap.key -> Type.typ
val typ_of_lvalue : constraint_info -> Type.typ IR.VarMap.t -> IR.lvalue -> Syntax.permission * Type.typ * Type.typ
val typ_of_value : constraint_info -> Type.typ IR.VarMap.t -> IR.value -> Type.typ
val typ_of_expr : constraint_info -> Type.typ IR.VarMap.t -> IR.expr -> Type.typ
val process_expr : constraint_info -> IR.variable list -> Type.typ IR.VarMap.t -> Type.L.ConstrSet.t -> IR.expr -> IR.variable list * Type.typ IR.VarMap.t * Type.L.ConstrSet.t
val process_program : Typecheck.type_info -> constraint_info -> IR.variable list -> Type.typ IR.VarMap.t -> L.ConstrSet.t -> IR.program -> unit
val process_function : Typecheck.type_info -> constraint_info -> IR.function_def -> unit