Intrinsics

Intrinsics

An intrinsic is a function without body whose semantics is given by the abstract domain based on its name. Each abstract domain can decide either to ignore the call to the intrinsic, delegate the call to some or all subdomains, or give it a tailored semantics and update the abstract state correspondingly. By default, an abstract domain treats the call to an intrinsic as a non-op and pass the call to the intrinsic to all of its subdomains.

Adding a call to an intrinsic function is much easier than modifying the CrabIR to add a new statement. For instance, in Verification of an optimized NTT algorithm, the Longa and Naehrig's reduction which peforms several hard-to-analyze arithmetic/bitwise operations was modeled as an intrinsic. This allowed to build a specialized interval domain with support for Longa and Naehrig's reduction without making any modification in Crab or re-implementing any Crab's functionality .

Over time, intrinsics have been also used for modeling too specialized CrabIR statements which we decided to keep as intrinsics in order to keep a relatively small the number of CrabIR statements. The (incomplete) list of intrinsic functions is currently:

• b := is_unfreed_or_null(rgn, ref)

  b is set to true if ref does not point to a freed memory object or it is null. If the abstract domain cannot decide then b is havoced.

• unfreed_or_null(rgn,ref)

  restricts the abstract state to ensure that ref does not point to a freed memory object.

• nonnull(ref)

  restricts the abstract state to ensure that ref is not null.

• b := is_dereferenceable(rgn, ref, sz)

  b is set to true if the memory [ref, ref+sz] has been allocated. If the abstract domain cannot decide then b is havoced.

• add_tag(rgn, ref, TAG)

  add TAG to the set of tags associated with the data pointed by ref.

• b := does_not_have_tag(rgn, ref, TAG)

• set b to true if the data pointed by ref does not have tag TAG If the abstract domain cannot decide then b is havoced.

• print_invariants(v1,...)

  Print the abstract state projected on variables v1,...

• var_packing_merge(v1,...)

  It has only meaning to the numerical variable packing domain. Merge all the variables into the same variable pack.