Skip to content
This repository has been archived by the owner on Jun 11, 2024. It is now read-only.

Commit

Permalink
Enable floating point functions and implement required logic througho…
Browse files Browse the repository at this point in the history 
…ut borealis
  • Loading branch information
@fmckeogh
fmckeogh committed May 20, 2024
1 parent ce6a3db commit f600821
Show file tree
Hide file tree
Showing 9 changed files with 213 additions and 138 deletions.
103 changes: 0 additions & 103 deletions borealis/src/brig/denylist.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,31 +30,6 @@ const DENYLIST: &[&'static str] = &[
"_shl_int_general",
"_shr_int_general",
"fmod_int",
"subrange_subrange_eq",
"subrange_subrange_concat",
"zext_slice",
"zext_subrange",
"sext_slice",
"sext_subrange",
"place_slice_signed",
"place_subrange_signed",
"unsigned_subrange",
"vector_update_subrange_from_subrange",
"vector_update_subrange_from_integer_subrange",
"mem_read_request_is_exclusive<Uarm_acc_type<>,b,O<RTranslationInfo>>",
"mem_read_request_is_ifetch<Uarm_acc_type<>,b,O<RTranslationInfo>>",
"mem_write_request_is_exclusive<Uarm_acc_type<>,b,O<RTranslationInfo>>",
"Replicate__1",
"Ones",
"IsOnes",
"integer_access",
"integer_update_subrange",
"ZeroExtend1",
"RoundTowardsZero",
"IsUNDEFINED",
"IsUNPREDICTABLE",
"IsSEE",
"IsExceptionTaken",
"ThrowSError",
"ReservedEncoding",
"__UNKNOWN_integer",
Expand All @@ -68,12 +43,6 @@ const DENYLIST: &[&'static str] = &[
"Elem_read",
"write_gpr_bits",
"set_R_bits",
"PMUCounterIsHyp",
"PMUOverflowCondition",
"HiLoPMUOverflow",
"PhysicalCountInt",
"EffectiveSCR_EL3_RW",
"PhysicalOffsetIsValid",
"GetTimestamp",
"ELIsInHost",
"IsInHost",
Expand Down Expand Up @@ -120,20 +89,6 @@ const DENYLIST: &[&'static str] = &[
"FFmul0B",
"FFmul0D",
"FFmul0E",
"AESMixColumns",
"AESInvMixColumns",
"SHAchoose",
"SHAparity",
"SHAmajority",
"SHAhashSIGMA0",
"SHAhashSIGMA1",
"SHA256hash",
"Sbox",
"TargetSecurityState",
"RESTRICT_PREDICTIONS",
"EAEisOne",
"CONTEXTIDR_NS_read",
"CONTEXTIDR_read",
"RecipEstimate",
"UnsignedRecipEstimate",
"RecipSqrtEstimate",
Expand Down Expand Up @@ -238,64 +193,6 @@ const DENYLIST: &[&'static str] = &[
"DecodeLDFAttr",
"S2DecodeCacheability",
"S2CombineS1AttrHints",
"WalkMemAttrs",
"NormalNCMemAttr",
"S1DecodeMemAttrs",
"S2MemTagType",
"S2DecodeMemAttrs",
"S2CombineS1MemAttrs",
"DecodePPS",
"AbovePPS",
"GPCFault",
"GPCRegistersConsistent",
"GPICheck",
"GPIValid",
"GPTL0Size",
"GPIIndex",
"GPTLevel0Index",
"GPTLevel1Index",
"GPTWalk",
"GranuleProtectionCheck",
"FetchDescriptor",
"ContiguousSize",
"TGxGranuleBits",
"TranslationSize",
"StageOA",
"CheckValidStateMatch",
"ContextMatchingBreakpointRange",
"IsContextMatchingBreakpoint",
"SPEStartCounter",
"SPEStopCounter",
"MemAtomic",
"RCWCheck",
"MemAtomicRCW",
"NVMem_read",
"NVMem_read__1",
"NVMem_set__1",
"MemStore64B",
"MemStore64BWithRet",
"MemLoad64B",
"FPRecipStepFused",
"FPRSqrtStepFused",
"SVEAccessTrap",
"SMEAccessTrap",
"ResetSMEState",
"SetPSTATE_SM",
"SetPSTATE_ZA",
"SetPSTATE_SVCR",
"Z_read",
"P_read",
"FFR_read",
"MemSingleNF_read",
"MemNF_read",
"ActivePredicateElement",
"PredicateElement",
"FirstActive",
"LastActive",
"NoneActive",
"ElemFFR_read",
"LastActiveElement",
"AnyActiveElement",
"FPCompareUN",
"FPCompareNE",
"FPOne",
Expand Down
23 changes: 19 additions & 4 deletions borealis/src/brig/functions_interpreter.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,8 @@ pub fn codegen_stmt(stmt: Statement) -> TokenStream {
UnaryOperationKind::Complement => quote! {!#value},
UnaryOperationKind::Power2 => quote! { (#value).pow(2) },
UnaryOperationKind::Absolute => quote! { (#value).abs() },
UnaryOperationKind::Ceil => quote! { (#value).ceil() },
UnaryOperationKind::Floor => quote! { (#value).floor() },
}
}
StatementKind::ShiftOperation {
Expand Down Expand Up @@ -630,10 +632,23 @@ fn codegen_cast(typ: Arc<Type>, value: Statement, kind: CastOperationKind) -> To
}
}

(Type::Primitive(_), Type::ArbitraryLengthInteger, CastOperationKind::ZeroExtend) => {
let target = codegen_type(target_type);
quote! {
(#target::try_from(#ident).unwrap())
(Type::Primitive(pt), Type::ArbitraryLengthInteger, CastOperationKind::ZeroExtend) => {
match pt.tc {
PrimitiveTypeClass::Void | PrimitiveTypeClass::Unit => {
panic!("cannot cast from void or unit")
}
PrimitiveTypeClass::UnsignedInteger | PrimitiveTypeClass::SignedInteger => {
let target = codegen_type(target_type);
quote! {
(#target::try_from(#ident).unwrap())
}
}
PrimitiveTypeClass::FloatingPoint => {
let target = codegen_type(target_type);
quote! {
(#ident as #target)
}
}
}
}

Expand Down
2 changes: 2 additions & 0 deletions borealis/src/brig/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -535,6 +535,7 @@ fn codegen_workspace(rudder: &Context) -> (HashMap<PathBuf, String>, HashSet<Pat
#header

extern crate alloc;
use micromath::F32Ext;
#imports

#contents
Expand Down Expand Up @@ -622,6 +623,7 @@ fn codegen_header() -> TokenStream {
#![allow(unused_mut)]
#![allow(unused_parens)]
#![allow(unused_variables)]
#![allow(unused_imports)]
#![allow(dead_code)]
#![allow(unreachable_code)]
#![allow(unused_doc_comments)]
Expand Down
14 changes: 10 additions & 4 deletions borealis/src/brig/workspace.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,10 +181,16 @@ pub fn create_manifest(
)),
)
})
.chain([(
PackageName::new("log".to_owned()).unwrap(),
InheritableDependency::Value(TomlDependency::Simple("0.4.21".to_owned())),
)])
.chain([
(
PackageName::new("log".to_owned()).unwrap(),
InheritableDependency::Value(TomlDependency::Simple("0.4.21".to_owned())),
),
(
PackageName::new("micromath".to_owned()).unwrap(),
InheritableDependency::Value(TomlDependency::Simple("2.1.0".to_owned())),
),
])
.collect(),
),
dev_dependencies: None,
Expand Down
105 changes: 86 additions & 19 deletions borealis/src/rudder/build.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -550,6 +550,23 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
)
}

"%string->%real" => {
let StatementKind::Constant { value, .. } = args[0].kind() else {
panic!();
};

let ConstantValue::String(str) = value else {
panic!();
};

let f = str.as_ref().parse().unwrap();

Some(self.builder.build(StatementKind::Constant {
typ: Arc::new(Type::f32()),
value: ConstantValue::FloatingPoint(f),
}))
}

"make_the_value" | "size_itself_int" => Some(args[0].clone()),
// %bv, %i, %i -> %bv
"subrange_bits" => {
Expand Down Expand Up @@ -577,7 +594,7 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}))
}

"eq_bit" | "eq_bits" | "eq_int" | "eq_bool" | "eq_string" => {
"eq_bit" | "eq_bits" | "eq_int" | "eq_bool" | "eq_string" | "eq_real" => {
Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::CompareEqual,
lhs: args[0].clone(),
Expand All @@ -595,7 +612,8 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {

// val add_atom : (%i, %i) -> %i
// val add_bits : (%bv, %bv) -> %bv
"add_atom" | "add_bits" => {
// val add_real : (%real, %real) -> %real
"add_atom" | "add_bits" | "add_real" => {
assert!(args[0].typ() == args[1].typ());
Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::Add,
Expand Down Expand Up @@ -636,11 +654,13 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}))
}

"mult_atom" => Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::Multiply,
lhs: args[0].clone(),
rhs: args[1].clone(),
})),
"mult_atom" | "mult_real" => {
Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::Multiply,
lhs: args[0].clone(),
rhs: args[1].clone(),
}))
}

"tdiv_int" | "ediv_int" | "ediv_nat" | "div_real" => {
Some(self.builder.build(StatementKind::BinaryOperation {
Expand All @@ -650,11 +670,14 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}))
}

"emod_nat" => Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::Modulo,
lhs: args[0].clone(),
rhs: args[1].clone(),
})),
"emod_nat" | "_builtin_mod_nat" => {
Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::Modulo,
lhs: args[0].clone(),
rhs: args[1].clone(),
}))
}

"negate_atom" => Some(self.builder.build(StatementKind::UnaryOperation {
kind: UnaryOperationKind::Negate,
value: args[0].clone(),
Expand Down Expand Up @@ -697,17 +720,44 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}))
}

// val ceil : (%real) -> %i
"ceil" => {
let ceil = self.builder.build(StatementKind::UnaryOperation {
kind: UnaryOperationKind::Ceil,
value: args[0].clone(),
});
Some(
self.builder
.generate_cast(ceil, Arc::new(Type::ArbitraryLengthInteger)),
)
}

// val floor : (%real) -> %i
"floor" => {
let floor = self.builder.build(StatementKind::UnaryOperation {
kind: UnaryOperationKind::Floor,
value: args[0].clone(),
});
Some(
self.builder
.generate_cast(floor, Arc::new(Type::ArbitraryLengthInteger)),
)
}

// val to_real : (%i) -> %real
"to_real" => Some(
self.builder
.generate_cast(args[0].clone(), Arc::new(Type::f64())),
),

"pow2" => Some(self.builder.build(StatementKind::UnaryOperation {
kind: UnaryOperationKind::Power2,
value: args[0].clone(),
})),
"lt_int" => Some(self.builder.build(StatementKind::BinaryOperation {
"pow2" | "_builtin_pow2" => {
Some(self.builder.build(StatementKind::UnaryOperation {
kind: UnaryOperationKind::Power2,
value: args[0].clone(),
}))
}

"lt_int" | "lt_real" => Some(self.builder.build(StatementKind::BinaryOperation {
kind: BinaryOperationKind::CompareLessThan,
lhs: args[0].clone(),
rhs: args[1].clone(),
Expand Down Expand Up @@ -871,7 +921,7 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}

// %bv -> %i
"UInt0" | "unsigned" => {
"UInt0" | "unsigned" | "_builtin_unsigned" => {
// just copy bits

Some(self.builder.build(StatementKind::Cast {
Expand Down Expand Up @@ -1067,6 +1117,22 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}

"bitvector_concat" => Some(self.generate_concat(args[0].clone(), args[1].clone())),

// val set_slice_int : (%i, %i, %i, %bv) -> %i
"set_slice_int" => {
// const sail_int len, const sail_int n, const sail_int start, const lbits slice
let len = args[0].clone();
let n = args[1].clone();
let start = args[2].clone();
let slice = args[3].clone();

// destination[start..] = source[0..source.len()]
// todo: check correctness and write some unit tests for this

Some(self.generate_set_slice(n, slice, len, start))
}

//val get_slice_int : (%i, %i, %i) -> %bv
"get_slice_int" => {
let extract = self.builder.build(StatementKind::BitExtract {
value: args[1].clone(),
Expand All @@ -1086,8 +1152,8 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
)
}

// val set_slice_bits : (%i, %i, %bv, %i, %bv) -> %bv
"set_slice_bits" => {
//val set_slice_bits : (%i, %i, %bv, %i, %bv) -> %bv
// len, slen, x, pos, y
let _len = args[0].clone();
let slen = args[1].clone();
Expand Down Expand Up @@ -1640,6 +1706,7 @@ impl<'ctx: 'fn_ctx, 'fn_ctx> BlockBuildContext<'ctx, 'fn_ctx> {
}

/// Copies source[0..source_length] into dest[start..start + source_length]
/// Output statement type should be same as destination
fn generate_set_slice(
&mut self,
destination: Statement,
Expand Down
Loading

0 comments on commit f600821

Please sign in to comment.