ICE using literal bytes

[niooss-ledger]

Hello,

This Rust program triggers an internal compiler error (ICE) when using Creusot:

use creusot_std::prelude::*;

pub fn use_bytes() -> u8 {
    b"A"[0]
}

cargo creusot reports:

thread 'rustc' (65308) panicked at creusot/src/backend/term.rs:546:43:
not yet implemented

and there indeed is a todo!() in

creusot/creusot/src/backend/term.rs

Line 546 in 9e8aa17

Literal::Bytes(ref _bytes) => todo!(),

Using the array notation works (cargo creusot succeeds and manages to proves everything):

use creusot_std::prelude::*;

const A: &[u8] = &[b'A']; // Using b"A" here triggers the ICE

#[ensures(result@ == 0x41)]
pub fn use_bytes() -> u8 {
    A[0]
}

(For context, I stumbled upon this while trying to add contracts to crate hex, which uses:

const HEX_CHARS_LOWER: &[u8; 16] = b"0123456789abcdef";

)

[Lysxia]

I was hoping to fix this before someone ran into it!

[niooss-ledger]

Hello,
I tried working on a fix for this issue, as it seemed simple. But it actually feels like the code I am writing does things against the abstractions built in Creusot.

More precisely, since PR #2140, literal bytes are parsed as Term with kind = TermKind::Lit(Literal::Bytes(bytes)). Such a term is lowered into Why using function lower_literal (in creusot/creusot/src/backend/term.rs), which seems to be expected to product a pure Why3 expression.
In Rust, literal bytes use slice type &[u8; N], which gets mapped to Coma's type Slice$bits_count$.slice:

creusot/prelude-generator/slice.in.coma

Lines 7 to 9 in c37b717

	type slice 'a =
	{ elts : seq 'a }
	invariant { UInt$bits_count$.in_bounds (Seq.length elts) }

Because of the invariant, it is impossible to directly construct a slice in a pure Why3 term (if I correctly understand how Why3 and Coma work). Introducing a new function and an axiom in the prelude works, but it does not seem to be a good way to fix this.

Example of patch to translate literal byes

diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
index 9250f2b349d5..121532b8d4f8 100644
--- a/creusot/src/backend/term.rs
+++ b/creusot/src/backend/term.rs
@@ -27,7 +27,7 @@ use rustc_middle::{
     ty::{self, Ty, TyCtxt, TyKind},
 };
 use rustc_span::Span;
-use rustc_type_ir::IntTy;
+use rustc_type_ir::{IntTy, UintTy};
 use why3::{
     Ident, Name,
     declaration::Condition as WCondition,
@@ -550,7 +550,18 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 Exp::unit()
             }
             Literal::String(ref string) => Constant::String(string.clone()).into(),
-            Literal::Bytes(ref _bytes) => todo!(),
+            Literal::Bytes(ref bytes) => {
+                let why_ty = Type::qconstructor(
+                    self.names.in_pre(uty_to_prelude(self.tcx(), UintTy::U8), "t"),
+                );
+                let byte_exps: Box<[Exp]> = bytes
+                    .iter()
+                    .map(|&b| Constant::Uint(u128::from(b), Some(why_ty.clone())).into())
+                    .collect();
+                let seq_exp = Exp::qvar(name::seq_create())
+                    .app([Exp::int(bytes.len() as i128), Exp::FunLiteral(byte_exps)]);
+                Exp::qvar(self.names.in_pre(PreMod::Slice, "of_seq")).app([seq_exp])
+            }
         }
     }
 }
diff --git a/prelude-generator/slice.in.coma b/prelude-generator/slice.in.coma
index 68166bef7177..f8e46780f5d3 100644
--- a/prelude-generator/slice.in.coma
+++ b/prelude-generator/slice.in.coma
@@ -13,6 +13,9 @@ module Slice$bits_count$
   type array 'a = slice 'a
 
   function view (s : slice 'a) : seq 'a = s.elts
+
+  function of_seq (s : seq 'a) : slice 'a
+  axiom of_seq_elts : forall s : seq 'a . (of_seq s).elts = s
 end
 
 module Slice$bits_count$Ops

One of the reason I believe it does not seem to be a good way is that translating Rust expressions such as &[b'A', b'B'] currently works. It would make better sense to translate b"AB" in exactly the same way. Trying to do so leads to generating intermediate statements in creusot/src/backend/program.rs, to copy:

creusot/creusot/src/backend/program.rs

Lines 812 to 840 in c37b717

	RValue::Array(fields) => {
	let id = Ident::fresh_local("__arr_temp");
	let ty = lower.ty(ty);
	let len = fields.len();
	let record = Exp::var(id).boxed();
	let label = Name::Global(lower.names.in_pre(PreMod::Slice, "elts"));
	let arr_elts = Exp::RecField { record, label };
	istmts.push(IntermediateStmt::Any(id, ty.clone()));
	let mut assumptions = fields
	.into_iter()
	.enumerate()
	.map(|(ix, f)| {
	Exp::qvar(name::seq_get())
	.app([arr_elts.clone(), Exp::Const(Constant::Int(ix as i128, None))])
	.eq(f.into_why(lower, istmts, span))
	})
	.chain([Exp::qvar(name::seq_length())
	.app([arr_elts.clone()])
	.eq(Exp::Const(Constant::Int(len as i128, None)))])
	.reduce(Exp::log_and)
	.expect("array literal missing assumption");
	assumptions.reassociate();
	istmts.push(IntermediateStmt::Assume(assumptions));
	Exp::var(id)
	}

Other possible patch to translate literal bytes

diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index a42e331ccddd..98a0ee4a8dab 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -34,7 +34,7 @@ use crate::{
             Block, Body, BorrowKind, Branches, LocalDecls, LocalKind, Operand, Place, RValue,
             Statement, StatementKind, Terminator,
         },
-        pearlite::Term,
+        pearlite::{Literal, Term, TermKind},
     },
 };
 use indexmap::IndexMap;
@@ -529,7 +529,43 @@ impl<'tcx> Operand<'tcx> {
         match self {
             Operand::Place(pl) => lower.rplace_to_expr(&pl, istmts, span),
             Operand::ShrBorrow(op) => op.into_why(lower, istmts, span),
-            Operand::Term(c, _) => lower_pure(lower.ctx, lower.names, &c.spanned()),
+            Operand::Term(c, _) => {
+                if let TermKind::Lit(Literal::Bytes(ref bytes)) = c.kind {
+                    // Translate b"abc" as &[b'a', b'b', b'c']: introduce a fresh array variable
+                    // and assume the element values, mirroring the RValue::Array translation.
+                    let id = Ident::fresh_local("__arr_temp");
+                    let arr_ty = lower.ty(c.ty);
+                    let record = Exp::var(id).boxed();
+                    let label = Name::Global(lower.names.in_pre(PreMod::Slice, "elts"));
+                    let arr_elts = Exp::RecField { record, label };
+                    let len = bytes.len();
+                    let u8_ty = Type::qconstructor(
+                        lower.names.in_pre(uty_to_prelude(lower.ctx.tcx, ty::UintTy::U8), "t"),
+                    );
+                    istmts.push(IntermediateStmt::Any(id, arr_ty));
+                    let mut assumptions = bytes
+                        .iter()
+                        .enumerate()
+                        .map(|(ix, &b)| {
+                            Exp::qvar(name::seq_get())
+                                .app([
+                                    arr_elts.clone(),
+                                    Exp::Const(Constant::Int(ix as i128, None)),
+                                ])
+                                .eq(Exp::Const(Constant::Uint(b as u128, Some(u8_ty.clone()))))
+                        })
+                        .chain([Exp::qvar(name::seq_length())
+                            .app([arr_elts.clone()])
+                            .eq(Exp::Const(Constant::Int(len as i128, None)))])
+                        .reduce(Exp::log_and)
+                        .expect("bytes literal missing assumption");
+                    assumptions.reassociate();
+                    istmts.push(IntermediateStmt::Assume(assumptions));
+                    Exp::var(id)
+                } else {
+                    lower_pure(lower.ctx, lower.names, &c.spanned())
+                }
+            }
             Operand::InlineConst(def_id, promoted, subst, ty) => {
                 let ret = Ident::fresh_local("_const_ret");
                 let result = Ident::fresh_local("_const");

This means that Operand::into_why would have a specific case for literal bytes constants, to bypass the call to lower_pure. This second approach does not seem so good either.

A third approach would be to modify function translate_assign in creusot/creusot/src/translation/function/statement.rs to produce RValue::Array(...) instead of RValue::Operand(Operand::Term(term) with term.kind = TermKind::Lit(Literal::Bytes(bytes)). This however seems to defeat the purpose of PR #2140 which introduced Literal::Bytes.

What do you think?

[Lysxia]

I think your first patch is the right way to fix it. And unless I'm missing a good reason why the translation of arrays is the way it is, it should be fixed to work similarly as well.

[jhjourdan]

I agree that adding a function Slice.of_seq in the prelude seems like the way to go, and that we could do similarly for arrays.

There is one important thing to take care, however. As it is, the axiom axiom of_seq_elts : forall s : seq 'a . (of_seq s).elts = s is unsound. Indeed, if s is longer than usize::MAX, then (of_seq s).elts is longer than usize::MAX, which it should not because of the invariant.

To fix this issue, you should add an assumption to the axiom: axiom of_seq_elts : forall s : seq 'a . UInt$bits_count$.in_bounds (Seq.length s) -> (of_seq s).elts = s. Also, it is a good idea to add a trigger to the axiom, to make sure that SMT solvers are not going to instantiate it with irrelevant values:

`axiom of_seq_elts : forall s : seq 'a [(of_seq s).elts] . UInt$bits_count$.in_bounds (Seq.length s) -> (of_seq s).elts = s`

[niooss-ledger]

Thanks for your quick feedbacks!

I will go with the first patch and the fixed axiom (you are right about the soundness issue and it was also part of my uneasiness about this approach). And now that axiom of_seq_elts is using UInt$bits_count$.in_bounds, I think it should be moved to module Slice$bits_count$Ops and copied to module Slice$bits_count$OpsBW (using UInt$bits_count$BW.in_bounds).

By the way, I did not know the trigger syntax in WhyML and the only reference I found in the documentation was in the term grammar (https://why3.org/doc/syntaxref.html#terms-and-formulas):

term0      ::=
...
                | quantifier quant_vars triggers? "." term   ; quantifier

triggers   ::=  "[" trigger ("|" trigger)* "]"
trigger    ::=  term ("," term)*

Is this explained somewhere in the documentation?

I am trying to find a way to tell Why3 when it should use the axiom with UInt$bits_count$.in_bounds and when it should use the one with UInt$bits_count$BW.in_bounds. Would you know how to do this?
Or I can also duplicate function of_seq in the Ops modules and rely on self.names.in_pre(PreMod::SliceOps, "of_seq") to select which module to use. Doing so feels a bit weird because function of_seq does not use integers, but it could make reasoning easier.

And unless I'm missing a good reason why the translation of arrays is the way it is, it should be fixed to work similarly as well.

I can try to modify the way RValue::Array is handled in RValue::into_why (in creusot/src/backend/program.rs) and see what breaks. I think I will open a proper Pull Request tomorrow.

[Lysxia]

IIRC the translation of array looks weird because that was still easier than figuring out the syntax for constructing sequences.

[jhjourdan]

I will go with the first patch and the fixed axiom (you are right about the soundness issue and it was also part of my uneasiness about this approach). And now that axiom of_seq_elts is using UInt$bits_count$.in_bounds, I think it should be moved to module Slice$bits_count$Ops and copied to module Slice$bits_count$OpsBW (using UInt$bits_count$BW.in_bounds).

See #2195. The modules Slice$bits_count$Ops and Slice$bits_count$ are now the same.

By the way, I did not know the trigger syntax in WhyML and the only reference I found in the documentation was in the term grammar (https://why3.org/doc/syntaxref.html#terms-and-formulas):

term0      ::=
...
                | quantifier quant_vars triggers? "." term   ; quantifier

triggers   ::=  "[" trigger ("|" trigger)* "]"
trigger    ::=  term ("," term)*

Is this explained somewhere in the documentation?

Unfortunately there is nothing else in the documentation. Triggers are not very idiomatic in Why3.

I am trying to find a way to tell Why3 when it should use the axiom with UInt$bits_count$.in_bounds and when it should use the one with UInt$bits_count$BW.in_bounds. Would you know how to do this? Or I can also duplicate function of_seq in the Ops modules and rely on self.names.in_pre(PreMod::SliceOps, "of_seq") to select which module to use. Doing so feels a bit weird because function of_seq does not use integers, but it could make reasoning easier.

Please duplicate the axiom. All this depends on integers, because the invariant of the slice module depends on the notion of integers. We should not import UInt16 in the context if we are in the bitwise mode.

And unless I'm missing a good reason why the translation of arrays is the way it is, it should be fixed to work similarly as well.

I can try to modify the way RValue::Array is handled in RValue::into_why (in creusot/src/backend/program.rs) and see what breaks. I think I will open a proper Pull Request tomorrow.

Thanks!

[niooss-ledger]

I opened PR #2198 but there is a strong performance regression with the chosen approach, caused by the modifications in the Coma prelude (I wrote some details in the PR description).