E8012

Error · Contract/Verification

E8012 — A function that says ensures !frees(p), when its body can free memory through p: the body gives p, or a value that it gets from p, to code that can free memory, such as a call without !frees for that parameter, a store or an mlir! block.

What the compiler reports

E8012] at {{.*}}frees_clause_that_a_body_breaks.vx:[[@LINE+4]]:11: `frees_it` says `!frees(p)`, but its body can free memory through `p`: it gives `p` to 'dealloc', which has no `!frees` for that parameter

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

//
// Part of the Vx Project, under the Apache License v2.0 with LLVM Exceptions.
// See LICENSE for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
// Each function here says `ensures !frees(p)`, and its body does one thing that can free the
// memory of `p`. So each one gets E8012 on the line of that thing. A function that gets a value
// with a drop by value always drops it or moves it, so it cannot say `!frees` for it. An impl
// of a trait method must keep the `!frees` of the trait.
//

import core::ptr;
import std::alloc;
import std::vec;

struct Noisy {
  id : i32,
}

impl Drop for Noisy {
  fn drop(self : &mut Noisy) -> void {
    print!("d{} ", self.id);
  }
}

struct Holder {
  p : *const i64,
}

fn frees_it(p : *mut i8) -> void
ensures !frees(p)
{
  dealloc(p, 8i64);
}

fn frees_a_moved_pointer(p : *mut i8) -> void
ensures !frees(p)
{
  let q = offset_mut(p, 0i64);
  dealloc(q, 8i64);
}

fn stores_it(h : &mut Holder, p : *const i64) -> void
ensures !frees(p)
{
  h.p = p;
}

fn puts_it_in_a_value(p : *const i64) -> i64
ensures !frees(p)
{
  let h = Holder {
    p: p
  };
  return 0i64;
}

unsafe fn moves_a_value_out(p : *const Noisy) -> i32
ensures !frees(p)
{
  let v = unsafe { *p };
  return v.id;
}

fn writes_a_value(p : *mut Noisy) -> void
ensures !frees(p)
{
  unsafe { *p = Noisy { id: 2 }; }
}

fn gives_it_to_a_method(p : *const i64) -> void
ensures !frees(p)
{
  let mut v : Vec<*const i64> = Vec::new();
  v.push(p);
}

fn frees_a_name_that_a_match_binds(o : Option<*mut i8>) -> void
ensures !frees(o)
{
  match o {
    Option::Some(q) => {
      dealloc(q, 8i64);
    }
    Option::None => {}
  }
}

fn gives_it_to_a_function_value(f : fn(*const i64) -> i64, p : *const i64) -> i64
ensures !frees(p)
{
  return f(p);
}

fn gives_it_to_an_mlir_block(p : *const i64) -> i64
ensures !frees(p)
{
  return mlir!( inputs : (%p = p : !llvm.ptr), returns : i64, dialects : ["llvm"]) {
    %v = llvm.load %p : !llvm.ptr -> i64
    macro.yield %v : i64
  };
}

fn gets_a_vector(v : Vec<i64>) -> i64
ensures !frees(v)
{
  return 0i64;
}

trait Reads {
  fn read_one(self : &Self, p : *const i64) -> i64
  ensures !frees(p);
}

struct Keeps {
  k : i64,
}

impl Reads for Keeps {
  fn read_one(self : &Keeps, p : *const i64) -> i64 {
    let h = Holder {
      p: p
    };
    return self.k;
  }
}

fn main() -> i32 {
  let x = 5i64;
  let k = Keeps {
    k: 1i64
  };
  return k.read_one(&x) as i32;
}

From tests/frontend/fail/frees_clause_that_a_body_breaks.vx, which asserts this diagnostic on every commit.

Related