search

rems-project / sail

Sail architecture definition language
Other
621 stars 114 forks source link

SMT generation type checker bug/todo? #781

Closed nwf closed 3 days ago

nwf commented 3 days ago

This example, lightly minimized from https://github.com/CHERIoT-Platform/cheriot-sail/blob/main/properties/props.sail,

$include "../sail-riscv/model/prelude.sail"
$include "../sail-riscv/model/riscv_xlen32.sail"
$include "../src/cheri_prelude.sail"
$include "../src/cheri_types.sail"
$include "../src/cheri_cap_common.sail"

function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag, capToBits(c))

function capEncodable(c : Capability) -> bool = c == encodeDecode(c)

$property
function prop_nullzero() -> bool = {
    capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false)
}

dies with

Todo:
eq_anything : (%bool, %bool)

To reproduce, have a checkout of CHERIoT-sail (and its submodule) handy, place the example above in properties/test.sail and run, in properties, sail -dtc_verbose 1 -smt ./test.sail). In case it's useful to have without running anything, the typechecker sayeth the following:

``` Check function prop_nullzero Binding _ to unit | Check { sail_assume(true); { and_bool(capEncodable(null_cap), and_bool(zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)), eq_bool(null_cap.tag, false))) } } <= bool | | Check sail_assume(true) <= unit | | Function sail_assume | | Adding type variable 'ex0# : Bool | | Unify unit and unit for 'ex0# | | | Infer true => bool(true) | | Unify bool('ex0#) and bool(true) for 'ex0# | | Unify unit and unit for | | Subtype unit and unit | | Check { and_bool(capEncodable(null_cap), and_bool(zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)), eq_bool(null_cap.tag, false))) } <= bool | | | Check and_bool(capEncodable(null_cap), and_bool(zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)), eq_bool(null_cap.tag, false))) <= bool | | | | | Function eq_bool | | | | | Adding type variable 'ex3950# : Bool | | | | | Adding type variable 'ex3949# : Bool | | | | | | | Infer null_cap => Capability | | | | | | Function tag | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Infer null_cap.tag => bool | | | | | Adding type variable 'ex4126# : Bool | | | | | Unify bool('ex3949#) and bool('ex4126#) for 'ex3949#, 'ex3950# | | | | | | Infer false => bool(false) | | | | | Unify bool('ex3950#) and bool(false) for 'ex3950# | | | | | Infer eq_bool(null_cap.tag, false) => bool | | | | Function and_bool | | | | Adding type variable 'p : Bool | | | | Adding type variable 'q : Bool | | | | | Function zz7nzJzK64#eq_bits | | | | | | Check capToBits(null_cap) <= bitvector(64) | | | | | | Function capToBits | | | | | | Unify bitvector(64) and bitvector(64) for | | | | | | Prove |- 64 == 64 | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Subtype bitvector(64) and bitvector(64) | | | | | | Check zz7nzJzK64#zeros_implicit(64) <= bitvector(64) | | | | | | Function zz7nzJzK64#zeros_implicit | | | | | | Unify bitvector(64) and bitvector(64) for | | | | | | Prove |- 64 == 64 | | | | | | | Check 64 <= int(64) | | | | | | | | Infer 64 => int(64) | | | | | | | Subtype int(64) and int(64) | | | | | | Subtype bitvector(64) and bitvector(64) | | | | | Infer zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)) => bool | | | | Adding type variable 'ex4128# : Bool | | | | Unify bool('p) and bool('ex4128#) for 'p, 'q | | | | | Function eq_bool | | | | | Adding type variable 'ex3950# : Bool | | | | | Adding type variable 'ex3949# : Bool | | | | | | | Infer null_cap => Capability | | | | | | Function tag | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Infer null_cap.tag => bool | | | | | Adding type variable 'ex4129# : Bool | | | | | Unify bool('ex3949#) and bool('ex4129#) for 'ex3949#, 'ex3950# | | | | | | Infer false => bool(false) | | | | | Unify bool('ex3950#) and bool(false) for 'ex3950# | | | | | Infer eq_bool(null_cap.tag, false) => bool | | | | Adding type variable 'ex4130# : Bool | | | | Unify bool('q) and bool('ex4130#) for 'q | | | | Infer and_bool(zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)), eq_bool(null_cap.tag, false)) => bool | | | Function and_bool | | | Adding type variable 'p : Bool | | | Adding type variable 'q : Bool | | | Unify bool(('p & 'q)) and bool for | | | | Function capEncodable | | | | | Check null_cap <= Capability | | | | | | Infer null_cap => Capability | | | | | Subtype Capability and Capability | | | | Infer capEncodable(null_cap) => bool | | | Adding type variable 'ex4132# : Bool | | | Unify bool('p) and bool('ex4132#) for 'p, 'q | | | Unify bool(('ex4132# & 'q)) and bool for | | | | | Function eq_bool | | | | | Adding type variable 'ex3950# : Bool | | | | | Adding type variable 'ex3949# : Bool | | | | | | | Infer null_cap => Capability | | | | | | Function tag | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Infer null_cap.tag => bool | | | | | Adding type variable 'ex4133# : Bool | | | | | Unify bool('ex3949#) and bool('ex4133#) for 'ex3949#, 'ex3950# | | | | | | Infer false => bool(false) | | | | | Unify bool('ex3950#) and bool(false) for 'ex3950# | | | | | Infer eq_bool(null_cap.tag, false) => bool | | | | Function and_bool | | | | Adding type variable 'p : Bool | | | | Adding type variable 'q : Bool | | | | | Function zz7nzJzK64#eq_bits | | | | | | Check capToBits(null_cap) <= bitvector(64) | | | | | | Function capToBits | | | | | | Unify bitvector(64) and bitvector(64) for | | | | | | Prove |- 64 == 64 | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Subtype bitvector(64) and bitvector(64) | | | | | | Check zz7nzJzK64#zeros_implicit(64) <= bitvector(64) | | | | | | Function zz7nzJzK64#zeros_implicit | | | | | | Unify bitvector(64) and bitvector(64) for | | | | | | Prove |- 64 == 64 | | | | | | | Check 64 <= int(64) | | | | | | | | Infer 64 => int(64) | | | | | | | Subtype int(64) and int(64) | | | | | | Subtype bitvector(64) and bitvector(64) | | | | | Infer zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)) => bool | | | | Adding type variable 'ex4135# : Bool | | | | Unify bool('p) and bool('ex4135#) for 'p, 'q | | | | | Function eq_bool | | | | | Adding type variable 'ex3950# : Bool | | | | | Adding type variable 'ex3949# : Bool | | | | | | | Infer null_cap => Capability | | | | | | Function tag | | | | | | | Check null_cap <= Capability | | | | | | | | Infer null_cap => Capability | | | | | | | Subtype Capability and Capability | | | | | | Infer null_cap.tag => bool | | | | | Adding type variable 'ex4136# : Bool | | | | | Unify bool('ex3949#) and bool('ex4136#) for 'ex3949#, 'ex3950# | | | | | | Infer false => bool(false) | | | | | Unify bool('ex3950#) and bool(false) for 'ex3950# | | | | | Infer eq_bool(null_cap.tag, false) => bool | | | | Adding type variable 'ex4137# : Bool | | | | Unify bool('q) and bool('ex4137#) for 'q | | | | Infer and_bool(zz7nzJzK64#eq_bits(capToBits(null_cap), zz7nzJzK64#zeros_implicit(64)), eq_bool(null_cap.tag, false)) => bool | | | Adding type variable 'ex4138# : Bool | | | Unify bool('q) and bool('ex4138#) for 'q | | | Unify bool(('ex4132# & 'ex4138#)) and bool for | | | Subtype bool and bool Check val spec sail_assert : . (bool, string) -> unit Adding val sail_assert : forall ('ex4139# : Bool). (bool('ex4139#), string) -> unit Check val spec sail_exit : . unit -> unit Adding val sail_exit : . unit -> unit Check val spec sail_cons : forall ('a : Type). ('a, list('a)) -> list('a) Adding type variable 'a : Type Adding type variable 'a : Type Adding type variable 'a : Type Adding val sail_cons : forall ('a : Type). ('a, list('a)) -> list('a) Adding type variable 'a : Type Adding type variable 'p : Bool Adding type variable 'q : Bool Adding type variable 'p : Bool Adding type variable 'q : Bool Adding type variable 'ex3950# : Bool Adding type variable 'ex3949# : Bool Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'ex3952# : Int Adding type variable 'ex3951# : Int Adding type variable 'w : Int Prove |- -9223372036854775808 <= 'w Prove |- -9223372036854775808 <= 'ex3951# Prove |- -9223372036854775808 <= 'ex3952# Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Prove 'ex3955# |- false Prove not('ex3955#) |- false Prove |- false Prove |- false Adding type variable 'ex3956# : Int Adding type variable 'l : Int Adding constraint 'l >= 0 Prove 'l >= 0 |- -9223372036854775808 <= 'l Prove 'l >= 0 |- 'l <= 9223372036854775807 Prove 'l >= 0 |- -9223372036854775808 <= 'ex3956# Adding type variable 'ex3956# : Int Adding type variable 'l : Int Adding constraint 'l >= 0 Prove 'l >= 0 |- -9223372036854775808 <= 'l Prove 'l >= 0 |- 'l <= 9223372036854775807 Prove 'l >= 0 |- -9223372036854775808 <= 'ex3956# Adding type variable 'ex3952# : Int Adding type variable 'ex3951# : Int Adding type variable 'w : Int Prove |- -9223372036854775808 <= 'w Prove |- -9223372036854775808 <= 'ex3951# Prove |- -9223372036854775808 <= 'ex3952# Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'm : Int Adding type variable 'ex3956# : Int Adding type variable 'l : Int Adding constraint 'l >= 0 Prove 'l >= 0 |- -9223372036854775808 <= 'l Prove 'l >= 0 |- 'l <= 9223372036854775807 Prove 'l >= 0 |- -9223372036854775808 <= 'ex3956# Adding type variable 'ex3956# : Int Adding type variable 'l : Int Adding constraint 'l >= 0 Prove 'l >= 0 |- -9223372036854775808 <= 'l Prove 'l >= 0 |- 'l <= 9223372036854775807 Prove 'l >= 0 |- -9223372036854775808 <= 'ex3956# Adding type variable 'ex3959# : Bool Adding type variable 'ex3959# : Bool Prove |- false Prove |- false Prove |- false Prove |- false Prove |- false Prove |- false Prove ('ex3966# | 'ex3967#) |- false Prove not(('ex3966# | 'ex3967#)) |- false Prove |- false Prove |- false Adding type variable 'ex3968# : Bool Adding type variable 'ex3968# : Bool Adding type variable 'ex3959# : Bool Adding type variable 'ex4156# : Bool Adding type variable 'ex4157# : Bool Adding type variable 'ex3955# : Bool Prove 'ex3989# |- false Prove not('ex3989#) |- false Prove 'ex4022#, not('ex3989#) |- false Prove not('ex4022#), not('ex3989#) |- false Prove 'ex4049#, not('ex4022#), not('ex3989#) |- false Prove not('ex4049#), not('ex4022#), not('ex3989#) |- false Prove 'ex4070#, not('ex4049#), not('ex4022#), not('ex3989#) |- false Prove not('ex4070#), not('ex4049#), not('ex4022#), not('ex3989#) |- false Adding type variable 'ex4161# : Bool Adding type variable 'ex4162# : Bool Prove ('ex4081# | 'ex4082#), not('ex4070#), not('ex4049#), not('ex4022#), not('ex3989#) |- false Prove not(('ex4081# | 'ex4082#)), not('ex4070#), not('ex4049#), not('ex4022#), not('ex3989#) |- false Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Adding type variable 'ex3955# : Bool Prove 'ex4124# |- false Prove not('ex4124#) |- false Adding type variable 'ex3968# : Bool Adding type variable 'ex0# : Bool Adding type variable 'ex3950# : Bool Adding type variable 'ex3949# : Bool Todo: eq_anything : (%bool, %bool) ```
Alasdair commented 3 days ago

Should be fixed by https://github.com/rems-project/sail/pull/782

Usually equality between booleans would be special-cased already, but I think here it's because we are comparing booleans within another data-structure. That error message just means that a primtive hasn't been implemented (for some combination of types) in the SMT generation, it's usually enough information by itself to fix the issue so if you get it again you can probably avoid minimizing the test case (although I appreciate the effort, it's usually very helpful for me!)