Module BufferOverrunDomain.AliasTarget

type alias_typ =
  1. | Eq
    (*

    The value of alias target is exactly the same to the alias key.

    *)
  2. | Le
    (*

    The value of alias target is less than or equal to the alias key. For example, if there is an alias between %r and size(x)+i with the Le type, it means size(x)+i <= %r.

    *)
type t =
  1. | Simple of {
    1. i : IR.IntLit.t;
    2. java_tmp : AbsLoc.Loc.t option;
    }
    (*

    Since Sil distinguishes logical and program variables, we need a relation for pruning values of program variables. For example, a C statement if(x){...} is translated to %r=load(x); if(%r){...} in Sil. At the load statement, we record the alias between the values of %r and x, then we can prune not only the value of %r, but also that of x inside the if branch. The java_tmp field is an additional slot for keeping one more alias of temporary variable in Java. The i field is to express %r=load(x)+i.

    *)
  2. | Empty
    (*

    For pruning vector.length with vector::empty() results, we adopt a specific relation between %r and v->elements, where %r=v.empty(). So, if %r!=0, v's array length (v->elements->length) is pruned by =0. On the other hand, if %r==0, v's array length is pruned by >=1.

    *)
  3. | Size of {
    1. alias_typ : alias_typ;
    2. i : IR.IntLit.t;
    3. java_tmp : AbsLoc.Loc.t option;
    }
    (*

    This is for pruning vector's length. When there is a function call, %r=x.size(), the alias target for %r becomes AliasTarget.size {l=x.elements}. The java_tmp field is an additional slot for keeping one more alias of temporary variable in Java. The i field is to express %r=x.size()+i, which is required to follow the semantics of Array.add inside loops precisely.

    *)
  4. | Fgets
    (*

    This is for pruning return values of fgets. If the result of fgets is not null, the length of return value will be pruned to greater than or equal to 1.

    *)
  5. | IteratorSimple of {
    1. i : IR.IntLit.t;
    2. java_tmp : AbsLoc.Loc.t option;
    }
    (*

    This is for tracking a relation between an iterator offset and an integer value. If %r has an alias to IteratorSimple {l; i}, which means that %r's iterator offset is same to l.

    *)
  6. | IteratorOffset of {
    1. alias_typ : alias_typ;
    2. i : IR.IntLit.t;
    3. java_tmp : AbsLoc.Loc.t option;
    }
    (*

    This is for tracking a relation between an iterator offset and the length of the underlying collection. If %r has an alias to IteratorOffset {l; i}, which means that %r's iterator offset is same to length(l)+i.

    *)
  7. | IteratorHasNext of {
    1. java_tmp : AbsLoc.Loc.t option;
    }
    (*

    This is for tracking return values of the hasNext function. If %r has an alias to HasNext {l}, which means that %r is same to l.hasNext().

    *)
  8. | IteratorNextObject of {
    1. objc_tmp : AbsLoc.Loc.t option;
    }
    (*

    This is for tracking the return values of nextObject function. If %r has an alias to nextObject {l}, which means that %r is the same to l.nextObject().

    *)
  9. | Top

Relations between values of logical variables(registers) and program variables

include Absint.AbstractDomain.S with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val equal : t -> t -> bool