Bug in `havoc_oracle`: `Fatal error: exception Not_found` occurs when using a reference to an array

[0npv527yh9]

Current Implementation

Before describing the main problem, I will describe the current implementation.

The function havoc_oracle in flowInference.ml "havocs" any integer value if some reference points to it and the ownership of that reference is 0. ("Havoc" is to set True to an integer value refinement that some reference is pointing to)

Currently, even though the ownership of an array a itself is 0, the integer value representing the length of a, which path is denoted as a!len, is NOT necessarily havoced.

If there is a reference r that points to an array a and the ownership of r is 0, then the integer value representing the length of a, which path is denotated r->*!len, is havoced. The same is true if a reference points to a tuple and the tuple contains an array, and in similar cases.

Example

The following program is VERIFIED.

// VERIFIED
{
    let n = (_: ~ > 0) in
    let a = mkarray n in
    let b = a in { // The ownership of `a` becomes 0.
        b[0] <- 1;

        // Even though `a` has ownership 0, 
        // the following assertion is VERIFIED.
        assert(a.length = n)
    }
}

However, the following one is UNVERIFIED.

// UNVERIFIED (unsafe)
{
    let n = (_: ~ > 0) in
    let r1 = mkref mkarray n in
    let r2 = r1 in { // the ownership of `r1` becomes 0
        
        // The following assertion is NOT verified.
        // `r1->*!len` is havoced because the ownership of `r1` itself is 0, 
        // not because the ownership of the array which `r1` points to is 0.
        // (In fact, the latter ownership is also 0 
        //  by ownership well-formedness, though.)
        assert(*r1.length = n); 
        
        r2 := mkarray _;
    }
}

Problem

Next, I will explain the main problem with an example.

The following program raises an error.

{
    let n = (_: ~ > 0) in
    let a = mkarray n in
    let r1 = mkref a in {
        alias(*r1 = a);
    }
}

The error message is:

Fatal error: exception Not_found

The error raises in the function havoc_oracle in flowInference.ml.

Why

• For each program point, the module OwnershipInference records the ownerships that may change (and be havoced) by gen: GenMap.t.
  • gen: GenMap.t: Partial Map from (program point, path) to ownerships
  • However, unchanged ownerships are not recorded.
• havoc_oracle determines whether to havoc integer values using the ownership information recorded in gen.
• In alias(*r1 = a), ownerships of a itself and the content of r1 are redistributed, but not that of r1 itself.
  • The ownership of r1 itself are NOT recorded at the program point of alias in gen.
• havoc_oracle tries to decide whether to havoc r1->*!len at the program point of alias(, and a->!len similarly).
  • As explained above, the ownership of r1 itself determines it, not r1->*.
  • However, information of r1 itself is not recorded at this point (because it does not change in alias(*r1 = a)).
  • Then, GenMap.find _ gen raises Not_found when it searches for information of r1.

(* flowInference.ml *)

let rec havoc_oracle ctxt ml p =
  ...
  let from_path p_ =
    let o = OI.GenMap.find (ml, p_) ctxt.o_hints.OI.gen in (* The error occurs HERE *)

How to fix

There are several options to solve this problem:

• Use the results of ownership inference
  • After ownership inference, we know the ownership of r1 in alias(*r1 = a).
  • This method may require many modifications.
• Havoc the integer value representing the length of an array a if the ownership of a itself is 0.
  • This is sound.
  • However, fewer programs can be verified:
    • For example, the first example will not be verified.
  • This method requires the following modifications:

    let rec havoc_oracle ctxt ml p =
    ...
        match P.tail p with
        | Some `Deref
        | Some `Ind
    -   | Some `Elem -> from_path @@ P.parent p
    +   | Some `Elem 
    +   | Some `Len -> from_path @@ P.parent p
    ...
    
    let%lq split_oracle sl ctxt =
    ...
        match (P.tail p1),(P.tail p2) with
        ...
        | Some a,Some b ->
          let () =  assert (a = b) in
    -     if a = `Deref || a = `Ind || a = `Elem then
    +     if a = `Deref || a = `Ind || a = `Elem || a = `Len then
            from_path @@ P.parent p1