Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support constant sorts that are not integers #932

Open
vrindisbacher opened this issue Dec 9, 2024 · 19 comments
Open

Support constant sorts that are not integers #932

vrindisbacher opened this issue Dec 9, 2024 · 19 comments
Assignees
@ranjitjhala

Comments

@vrindisbacher
Copy link
Collaborator

I have some constants that define the location of memory mapped registers.

pub const ISER_START: u32 = 0xE000E100;
pub const ISER_END: u32 = 0xE000E13C;
//
pub const ICER_START: u32 = 0xE000E180;
pub const ICER_END: u32 = 0xE000E1BC;
//
pub const ISPR_START: u32 = 0xE000E200;
pub const ISPR_END: u32 = 0xE000E23C;
//
pub const ICPR_START: u32 = 0xE000E280;
pub const ICPR_END: u32 = 0xE000E2BC;
//
pub const IABR_START: u32 = 0xE000E300;
pub const IABR_END: u32 = 0xE000E37C;
//
pub const IPR_START: u32 = 0xE000E400;
pub const IPR_END: u32 = 0xE000E7EC;

I then use these constants in a flux definition:

fn is_valid_nvic_addr(address: int) -> bool {
    if (address >= ISER_START && address <= ISER_END) {
       (address - ISER_START) % 4 == 0
    } else if (address >= ICER_START && address <= ICER_END) {
        (address - ICER_START) % 4 == 0
    } else if (address >= ISPR_START && address <= ISPR_END) {
        (address - ISPR_START) % 4 == 0
    } else if (address >= ICPR_START && address <= ICPR_END) {
        (address - ICPR_START) % 4 == 0
    } else if (address >= IABR_START && address <= IABR_END) {
        (address - IABR_START) % 4 == 0
    } else if (address >= IPR_START && address <= IPR_END) {
        (address - IPR_START) % 4 == 0
    } else {
        false
    }
}

I'd like to make all of these constants of type BV32, which looks like:

#[opaque]
#[refined_by(x: bitvec<32>)]
pub struct BV32(u32);

Unfortunately, this is not possible atm because const sorts are restricted to int. It would be great if we could allow something like:

#[sig(fn (u32[@x]) -> bv_int_to_bv32(x))]
const fn into_bv32(x: u32) -> BV32 {
    BV32(x)
}

pub const ICER_START: BV32 = into_bv32(0xE000E180);
@ranjitjhala ranjitjhala self-assigned this Dec 10, 2024
@ranjitjhala ranjitjhala mentioned this issue Dec 12, 2024
Merged
@ranjitjhala
Copy link
Contributor

@vrindisbacher -- see this PR #941 which should get you unblocked (?) in particular, it lets you write stuff like

#![flux::defs(
    fn is_start(x:bitvec<32>) -> bool { x == START }
)]

#[flux::opaque]
#[flux::refined_by(val: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux::trusted]
    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
    const fn new(val: u32) -> Self {
        BV32(val)
    }
}

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

#[flux_rs::sig(fn () -> BV32[START])]
pub fn test1() -> BV32 {
    BV32::new(0x4567)
}

#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
pub fn test2() -> BV32 {
    BV32::new(0x4567)
}

@ranjitjhala
Copy link
Contributor

The missing bit is that right now the specification

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

is completely trusted. i.e. not checked -- you can make up whatever random constant you like in the flux_rs::constant which describes the (alleged) value of the constant. I think its better to handle that in a separate PR...

@vrindisbacher
Copy link
Collaborator Author

Yes I think that should do the trick. I will checkout that branch and give it a try now. btw, what happens if I have something like this:

#[flux_rs::sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
const fn into_bv32(val: u32) -> BV32 {
    BV32(val)
}

pub const START: BV32 = into_bv32(0xFFFF_FFFF);

This is a way to circumvent the fact that the constant specification isn't checked right? Or do you have to use flux_rs::constant?

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 12, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

Ya - I guess my question is would I get an error or is it ok to just rely on the function annotation that converts it to BV32?

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 12, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

Ok so I was able to convert all constants to bitvec<32>, but now some seemingly trivial postconditions cannot be proved. Here's an example:

This function's postcondition cannot be proved. Here's the definition of is_valid_sys_tick_write_addr. This seems to be the case for all the other annotations that follow this style (i.e. where all the functions do is equality checks on bitvec constants and the refinement is identical to the actual implementation)

@nilehmann
Copy link
Member

nilehmann commented Dec 12, 2024 •
edited
Loading

@ranjitjhala it's silly that we didn't anticipate this but if we write

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

we need to make sure we give START type BV32[bv_int_to_bv32(0x4567)] when used inside a function.

Right now we lower START as an opaque constant in mir bodies which we don't give a type specific enough.

@nilehmann
Copy link
Member

concretely, the following should work

#[flux::opaque]
#[flux::refined_by(val: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux::trusted]
    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
    const fn new(val: u32) -> Self {
        BV32(val)
    }
}

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

#[flux_rs::sig(fn () -> BV32[START])]
pub fn test1() -> BV32 {
    START
}

@vrindisbacher
Copy link
Collaborator Author

vrindisbacher commented Dec 17, 2024 •
edited
Loading

I'm having a bit of trouble with inequalities on constants. Here's a minimal example....

#[flux_rs::constant(bv_int_to_bv32(0xE000E200))]
pub const ISPR_START: BV32 = BV32::new(0xE000_E200);
#[flux_rs::constant(bv_int_to_bv32(0xE000_E23C))]
pub const ISPR_END: BV32 = BV32::new(0xE000_E23C);

flux_rs::defs! {
    fn bv32(x: int) -> bitvec<32> { bv_int_to_bv32(x) }
    fn mod_is_valid_nvic(x: BV32) -> bool {
       x >= ISPR_START && x <= ISPR_END
    }
}

#[flux_rs::sig(fn () -> bool[mod_is_valid_nvic(bv32(0xe000_e200))])]
fn trivial() -> bool {
    true
}

Is this currently expected? The fluxc constraint seems reasonable...

∀ . (true = (BV32 { bv_int_to_bv32(3758154240) } ≥ armv7m::mem::nvic::ISPR_START ∧ BV32 { bv_int_to_bv32(3758154240) } ≤ armv7m::mem::nvic::ISPR_END)) ~ Ret at 51:5: 51:9

So does the smt2 file passed to fixpoint:

(qualif EqZero ((v int)) ((= v 0)))
(qualif GtZero ((v int)) ((> v 0)))
(qualif GeZero ((v int)) ((>= v 0)))
(qualif LtZero ((v int)) ((< v 0)))
(qualif LeZero ((v int)) ((<= v 0)))
(qualif Eq ((a int) (b int)) ((= a b)))
(qualif Gt ((a int) (b int)) ((> a b)))
(qualif Ge ((a int) (b int)) ((>= a b)))
(qualif Lt ((a int) (b int)) ((< a b)))
(qualif Le ((a int) (b int)) ((<= a b)))
(qualif Le1 ((a int) (b int)) ((<= a (- b 1))))
(constant c0 (BitVec Size32))  ;; rust const: armv7m::mem::nvic::ISPR_START Some(BV32 { bv_int_to_bv32(3758154240) })
(constant c1 (BitVec Size32))  ;; rust const: armv7m::mem::nvic::ISPR_END Some(BV32 { bv_int_to_bv32(3758154300) })
(constant gt (func 1 (@(0) @(0) ) bool))
(constant ge (func 1 (@(0) @(0) ) bool))
(constant lt (func 1 (@(0) @(0) ) bool))
(constant le (func 1 (@(0) @(0) ) bool))

(constraint
 (forall ((_$ int) ((= c1 (int_to_bv32 3758154300))))
  (forall ((_$ int) ((= c0 (int_to_bv32 3758154240))))
   (tag ((= true (and (and (ge (int_to_bv32 3758154240) c0)) (and (le (int_to_bv32 3758154240) c1))))) "0"))))

Not sure where things are going wrong here.

@vrindisbacher
Copy link
Collaborator Author

An even simpler and pretty surprising example is:

#[flux_rs::constant(bv_int_to_bv32(0xE000E200))]
pub const ISPR_START: BV32 = BV32::new(0xE000_E200);

#[flux_rs::sig(fn () -> bool[ISPR_START >= ISPR_START])]
fn trivial() -> bool {
    true
}

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

Ya - postcondition cannot be proved

error[E0999]: refinement type error
  --> src/armv7m/mem/nvic.rs:44:5
   |
44 |     true
   |     ^^^^ a postcondition cannot be proved
   |
note: this is the condition that cannot be proved
  --> src/armv7m/mem/nvic.rs:42:30
   |
42 | #[flux_rs::sig(fn () -> bool[ISPR_START >= ISPR_START])]
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^

error: could not compile `veri-asm` (lib) due to 1 previous error

@nilehmann
Copy link
Member

nilehmann commented Dec 17, 2024 •
edited
Loading

binary relations behave differently depending on the sort. For integers binary relations are interpreted, meaning that if you write 1 <= 2 in a refinement, that <= is interpreted as less than or equal in the theory of integers. The same for reals. For tuples, binary relations are interpreted pointwise which we encode, e.g., by translating (1, 3) <= (2, 3) into 1 <= 2 && 3 <= 3. For other sorts relations are uninterpreted, i.e., we define an uninterpreted function le.

The encoding for integers and reals is easy because there's only one meaning for <= and because the symbol <= is overloaded so we can use it directly to encode the relation for reals and integers and z3 would do the rest.

The symbol <= does not work for bit-vectors, so we need to pick a meaning for it. I think we could hardcode the meaning and pick either bvule or bvsle. You can also explicitly use one of those instead of <=.

The confusion arises because flux doesn't complain about using <= for bit-vectors. Using <= is technically correct, but has surprising behavior.

(the same applies for bool, although <= has an obvious interpretation for bool so we could just implement that)

edit: this is implemented here https://github.com/flux-rs/flux/blob/nico/move-checker-config-to-infer/crates/flux-infer/src/fixpoint_encoding.rs/#L1155

@vrindisbacher
Copy link
Collaborator Author

Ah ok. Looking at the SMT-LIB docs, they actually implement bv_ule via equality over integers: https://smt-lib.org/theories-FixedSizeBitVectors.shtml

@vrindisbacher
Copy link
Collaborator Author

vrindisbacher commented Dec 17, 2024 •
edited
Loading

@nilehmann perhaps the simplest thing to do for now is add bvule etc. here:

flux/crates/flux-middle/src/lib.rs

Line 78 in 7073381

pub static THEORY_FUNCS: LazyLock<UnordMap<Symbol, TheoryFunc>> = LazyLock::new(|| {
?

I can use those direclty instead of <= and >= in my refinement annotations.

@nilehmann
Copy link
Member

@vrindisbacher yes, that sound like the easiest (and in a sense the most correct)

@ranjitjhala
Copy link
Contributor

Looks like these are already in fixpoint so you'll just have to translate them to the appropriate name there (see bvULeName ...)

@vrindisbacher
Copy link
Collaborator Author

Yep openening a pr for it

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ranjitjhala ranjitjhala

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ranjitjhala @nilehmann @vrindisbacher