E8013

Error · Contract/Verification

E8013 — A type invariant that is not well formed. An invariant of a struct can use self, the fields of self at any depth, numbers, operators and the pointer clauses valid, initialized and overlaps. It calls no other function.

What the compiler reports

Error[E8013] at {{.*}}.vx:[[@LINE+1]]:21: this invariant of `Holder` is not well formed: `Pair` has no field `c`{{$}}
Error[E8013] at {{.*}}.vx:[[@LINE+1]]:23: this invariant of `Holder` is not well formed: it names `LIMIT`, and an invariant can name only `self` and its fields{{$}}
Error[E8013] at {{.*}}.vx:[[@LINE+1]]:21: this invariant of `Holder` is not well formed: `i64` is not a struct, so it has no field `bits`{{$}}
Error[E8013] at {{.*}}.vx:[[@LINE+1]]:21: this invariant of `Holder` is not well formed: it calls the method `sum`, and an invariant can call only `valid`, `initialized` and `overlaps`{{$}}
Error[E8013] at {{.*}}.vx:[[@LINE+1]]:11: this invariant of `Holder` is not well formed: it calls `positive`, and an invariant can call only `valid`, `initialized` and `overlaps`{{$}}
Error[E8013] at {{.*}}.vx:[[@LINE+1]]:11: this invariant of `Holder` is not well formed: `valid` takes 2 arguments{{$}}

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
//
//
// An invariant of a struct can use `self`, its fields at any depth, numbers, operators and the
// pointer clauses. The first and the last invariant of `Holder` are well formed. Each other one
// gets E8013.

const LIMIT : i64 = 10;

struct Pair {
  a : i64,
  b : i64,
}

impl Pair {
  fn sum(self : &Pair) -> i64 {
    return self.a + self.b;
  }
}

fn positive(n : i64) -> bool {
  return n > 0i64;
}

struct Holder
invariant self.pair.a <= self.pair.b && self.size >= 0i64
invariant self.pair.c > 0i64
invariant self.size < LIMIT
invariant self.size.bits > 0i64
invariant self.pair.sum() > 0i64
invariant positive(self.size)
invariant valid(self.data)
invariant valid(self.data, self.size) && initialized(self.data, self.size)
{
  pair : Pair,
  size : i64,
  data : *mut i64,
}

fn main() -> i32 {
  return 0;
}

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

Contracts and verificationThe chapter covering the rule this code enforces. All diagnosticsEvery code the compiler can emit, grouped by stage. E8012A body that breaks a pointer ensures of its function. The facts at a return, or at the end of the body, do not prove a clause such as ensures valid(return, n). Or the body changes a parameter that such a clause names. Or the function says ensures !frees(p), and its 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. E8014Code outside the module of a type with an invariant changes a field of the type. Only the module (the .vx file) that declares the type can write a field, take a &mut to a field, call a method that takes &mut self on a field, move a field out of the value, or build the type with a struct literal. Other code calls a function of the module to change a value of the type. Then the invariant holds for each value of the type outside its module.

E8013

What the compiler reports

A program that triggers it

Related