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.

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

Add support for f16 and f128 for toolchain upgrade to 6/28 #3306

Merged
merged 17 commits into from
Jul 1, 2024
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,11 @@ pub enum ExprValue {
// {}
EmptyUnion,
/// `1.0f`
Float16Constant(f16),
/// `1.0f`
FloatConstant(f32),
/// `Float 128 example`
Float128Constant(f128),
/// `function(arguments)`
FunctionCall {
function: Expr,
Expand Down Expand Up @@ -581,6 +585,28 @@ impl Expr {
expr!(EmptyUnion, typ)
}

/// `3.14f`
pub fn float16_constant(c: f16) -> Self {
expr!(Float16Constant(c), Type::float16())
}

/// `union {_Float16 f; uint16_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
pub fn float16_constant_from_bitpattern(bp: u16) -> Self {
let c = f16::from_bits(bp);
Self::float16_constant(c)
}

/// `3.14159265358979323846264338327950288L`
pub fn float128_constant(c: f128) -> Self {
expr!(Float128Constant(c), Type::float128())
}

/// `union {_Float128 f; __uint128_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
pub fn float128_constant_from_bitpattern(bp: u128) -> Self {
let c = f128::from_bits(bp);
Self::float128_constant(c)
}

/// `1.0f`
pub fn float_constant(c: f32) -> Self {
expr!(FloatConstant(c), Type::float())
Expand Down
54 changes: 53 additions & 1 deletion cprover_bindings/src/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,10 @@ pub enum Type {
FlexibleArray { typ: Box<Type> },
/// `float`
Float,
/// `_Float16`
Float16,
/// `_Float128`
Float128,
/// `struct x {}`
IncompleteStruct { tag: InternedString },
/// `union x {}`
Expand Down Expand Up @@ -166,6 +170,8 @@ impl DatatypeComponent {
| Double
| FlexibleArray { .. }
| Float
| Float16
| Float128
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
| Integer
| Pointer { .. }
| Signedbv { .. }
Expand Down Expand Up @@ -363,6 +369,8 @@ impl Type {
Double => st.machine_model().double_width,
Empty => 0,
FlexibleArray { .. } => 0,
Float16 => 16,
Float128 => 128,
Float => st.machine_model().float_width,
IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
Expand Down Expand Up @@ -532,6 +540,22 @@ impl Type {
}
}

pub fn is_float_16(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
Float16 => true,
_ => false,
}
}

pub fn is_float_128(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
Float128 => true,
_ => false,
}
}

pub fn is_float(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
Expand All @@ -543,7 +567,7 @@ impl Type {
pub fn is_floating_point(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
Double | Float => true,
Double | Float | Float16 | Float128 => true,
_ => false,
}
}
Expand Down Expand Up @@ -577,6 +601,8 @@ impl Type {
| CInteger(_)
| Double
| Float
| Float16
| Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
Expand Down Expand Up @@ -632,6 +658,8 @@ impl Type {
| Double
| Empty
| Float
| Float16
| Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
Expand Down Expand Up @@ -918,6 +946,8 @@ impl Type {
| CInteger(_)
| Double
| Float
| Float16
| Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
Expand Down Expand Up @@ -1042,6 +1072,14 @@ impl Type {
FlexibleArray { typ: Box::new(self) }
}

pub fn float16() -> Self {
Float16
}

pub fn float128() -> Self {
Float128
}

pub fn float() -> Self {
Float
}
Expand Down Expand Up @@ -1275,6 +1313,10 @@ impl Type {
Expr::c_true()
} else if self.is_float() {
Expr::float_constant(1.0)
} else if self.is_float_16() {
Expr::float16_constant(1.0)
} else if self.is_float_128() {
Expr::float128_constant(1.0)
} else if self.is_double() {
Expr::double_constant(1.0)
} else {
Expand All @@ -1291,6 +1333,10 @@ impl Type {
Expr::c_false()
} else if self.is_float() {
Expr::float_constant(0.0)
} else if self.is_float_16() {
Expr::float16_constant(0.0)
} else if self.is_float_128() {
Expr::float128_constant(0.0)
} else if self.is_double() {
Expr::double_constant(0.0)
} else if self.is_pointer() {
Expand All @@ -1309,6 +1355,8 @@ impl Type {
| CInteger(_)
| Double
| Float
| Float16
| Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
Expand Down Expand Up @@ -1413,6 +1461,8 @@ impl Type {
Type::Empty => "empty".to_string(),
Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
Type::Float => "float".to_string(),
Type::Float16 => "float16".to_string(),
Type::Float128 => "float128".to_string(),
Type::IncompleteStruct { tag } => tag.to_string(),
Type::IncompleteUnion { tag } => tag.to_string(),
Type::InfiniteArray { typ } => {
Expand Down Expand Up @@ -1512,6 +1562,8 @@ mod type_tests {
assert_eq!(type_def.is_unsigned(&mm), src_type.is_unsigned(&mm));
assert_eq!(type_def.is_scalar(), src_type.is_scalar());
assert_eq!(type_def.is_float(), src_type.is_float());
assert_eq!(type_def.is_float_16(), src_type.is_float_16());
assert_eq!(type_def.is_float_128(), src_type.is_float_128());
assert_eq!(type_def.is_floating_point(), src_type.is_floating_point());
assert_eq!(type_def.width(), src_type.width());
assert_eq!(type_def.can_be_lvalue(), src_type.can_be_lvalue());
Expand Down
4 changes: 4 additions & 0 deletions cprover_bindings/src/irep/irep_id.rs
Original file line number Diff line number Diff line change
Expand Up @@ -283,6 +283,8 @@ pub enum IrepId {
Short,
Long,
Float,
Float16,
Float128,
Double,
Byte,
Boolean,
Expand Down Expand Up @@ -1157,6 +1159,8 @@ impl Display for IrepId {
IrepId::Short => "short",
IrepId::Long => "long",
IrepId::Float => "float",
IrepId::Float16 => "float16",
IrepId::Float128 => "float128",
IrepId::Double => "double",
IrepId::Byte => "byte",
IrepId::Boolean => "boolean",
Expand Down
43 changes: 43 additions & 0 deletions cprover_bindings/src/irep/to_irep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,25 @@ impl ToIrep for ExprValue {
)],
}
}
ExprValue::Float16Constant(i) => {
let c: u16 = i.to_bits();
Irep {
id: IrepId::Constant,
sub: vec![],
named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))],
}
}
ExprValue::Float128Constant(i) => {
let c: u128 = i.to_bits();
Irep {
id: IrepId::Constant,
sub: vec![],
named_sub: linear_map![(
IrepId::Value,
Irep::just_bitpattern_id(c, 128, false)
)],
}
}
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
IrepId::FunctionCall,
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
Expand Down Expand Up @@ -695,6 +714,30 @@ impl ToIrep for Type {
(IrepId::CCType, Irep::just_id(IrepId::Float)),
],
},
Type::Float16 => Irep {
id: IrepId::Floatbv,
sub: vec![],
// Fraction bits: 10
// Precision bits: 5
// Sign bit: 1
named_sub: linear_map![
(IrepId::F, Irep::just_int_id(10)),
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
(IrepId::Width, Irep::just_int_id(16)),
(IrepId::CCType, Irep::just_id(IrepId::Float16)),
],
},
Type::Float128 => Irep {
id: IrepId::Floatbv,
sub: vec![],
// Fraction bits: 112
// Precision bits: 52
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
// Sign bit: 1
named_sub: linear_map![
(IrepId::F, Irep::just_int_id(112)),
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
(IrepId::Width, Irep::just_int_id(128)),
(IrepId::CCType, Irep::just_id(IrepId::Float128)),
],
},
Type::IncompleteStruct { tag } => Irep {
id: IrepId::Struct,
sub: vec![],
Expand Down
3 changes: 3 additions & 0 deletions cprover_bindings/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@
//! Speical [irep::Irep::id]s include:
//! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].

#![feature(f128)]
#![feature(f16)]

mod env;
pub mod goto_program;
pub mod irep;
Expand Down
6 changes: 6 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -184,12 +184,18 @@ impl<'tcx> GotocCtx<'tcx> {
// Instead, we use integers with the right width to represent the bit pattern.
{
match k {
FloatTy::F16 => Some(Expr::float16_constant_from_bitpattern(
alloc.read_uint().unwrap() as u16,
)),
FloatTy::F32 => Some(Expr::float_constant_from_bitpattern(
alloc.read_uint().unwrap() as u32,
)),
FloatTy::F64 => Some(Expr::double_constant_from_bitpattern(
alloc.read_uint().unwrap() as u64,
)),
FloatTy::F128 => {
Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap()))
}
}
}
TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _))
Expand Down
2 changes: 2 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,8 @@ impl<'tcx> GotocCtx<'tcx> {
Type::Empty => todo!(),
Type::FlexibleArray { .. } => todo!(),
Type::Float => write!(out, "f32")?,
Type::Float16 => write!(out, "f16")?,
Type::Float128 => write!(out, "f128")?,
Type::IncompleteStruct { .. } => todo!(),
Type::IncompleteUnion { .. } => todo!(),
Type::InfiniteArray { .. } => todo!(),
Expand Down
3 changes: 1 addition & 2 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
.intersperse("::")
.collect::<String>();
KaniAttributeKind::try_from(ident_str.as_str())
.map_err(|err| {
.inspect_err(|&err| {
debug!(?err, "attr_kind_failed");
tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
err
})
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
.ok()
} else {
Expand Down
2 changes: 2 additions & 0 deletions kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@
#![feature(more_qualified_paths)]
#![feature(iter_intersperse)]
#![feature(let_chains)]
#![feature(f128)]
#![feature(f16)]
extern crate rustc_abi;
extern crate rustc_ast;
extern crate rustc_ast_pretty;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-06-27"
channel = "nightly-2024-06-28"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]