diff --git a/pintc/src/error/compile_error.rs b/pintc/src/error/compile_error.rs index c21ec3a3..f721e7dc 100644 --- a/pintc/src/error/compile_error.rs +++ b/pintc/src/error/compile_error.rs @@ -222,6 +222,13 @@ pub enum CompileError { arity: &'static str, large_err: Box, }, + #[error("operator invalid type error")] + OperatorInvalidType { + op: &'static str, + ty_kind: &'static str, + bad_ty: String, + span: Span, + }, #[error("{init_kind} initialization type error")] InitTypeError { init_kind: &'static str, @@ -981,6 +988,17 @@ impl ReportableError for CompileError { } }, + OperatorInvalidType { + op, + ty_kind, + bad_ty, + span, + } => vec![ErrorLabel { + message: format!("invalid {ty_kind} type `{bad_ty}` for operator `{op}`"), + span: span.clone(), + color: Color::Red, + }], + BadCastTo { ty, span } => vec![ErrorLabel { message: format!("illegal cast to a `{ty}`"), span: span.clone(), @@ -1363,6 +1381,7 @@ impl ReportableError for CompileError { | SelectBranchesTypeMismatch { .. } | ConstraintExpressionTypeError { .. } | OperatorTypeError { .. } + | OperatorInvalidType { .. } | InitTypeError { .. } | StateVarInitTypeError { .. } | IndexExprNonIndexable { .. } @@ -1614,7 +1633,8 @@ impl Spanned for CompileError { | UnknownUnionVariant { span, .. } | SuperfluousUnionExprValue { span, .. } | MissingUnionExprValue { span, .. } - | UnionVariantTypeMismatch { span, .. } => span, + | UnionVariantTypeMismatch { span, .. } + | OperatorInvalidType { span, .. } => span, DependencyCycle { spans } => &spans[0], diff --git a/pintc/src/predicate/analyse/type_check.rs b/pintc/src/predicate/analyse/type_check.rs index 93da25d8..6afb2d00 100644 --- a/pintc/src/predicate/analyse/type_check.rs +++ b/pintc/src/predicate/analyse/type_check.rs @@ -1963,34 +1963,26 @@ impl Contract { rhs_expr_key: ExprKey, span: &Span, ) -> Inference { - let check_numeric_args = |lhs_ty: &Type, rhs_ty: &Type, ty_str: &str| { + let check_numeric_args = |lhs_ty: &Type, rhs_ty: &Type| { if !lhs_ty.is_num() { if !lhs_ty.is_error() { handler.emit_err(Error::Compile { - error: CompileError::OperatorTypeError { - arity: "binary", - large_err: Box::new(LargeTypeError::OperatorTypeError { - op: op.as_str(), - expected_ty: ty_str.to_string(), - found_ty: self.with_ctrct(lhs_ty).to_string(), - span: self.expr_key_to_span(lhs_expr_key), - expected_span: None, - }), + error: CompileError::OperatorInvalidType { + op: op.as_str(), + ty_kind: "non-numeric", + bad_ty: self.with_ctrct(lhs_ty).to_string(), + span: span.clone(), }, }); } } else if !rhs_ty.is_num() { if !rhs_ty.is_error() { handler.emit_err(Error::Compile { - error: CompileError::OperatorTypeError { - arity: "binary", - large_err: Box::new(LargeTypeError::OperatorTypeError { - op: op.as_str(), - expected_ty: ty_str.to_string(), - found_ty: self.with_ctrct(rhs_ty).to_string(), - span: self.expr_key_to_span(rhs_expr_key), - expected_span: None, - }), + error: CompileError::OperatorInvalidType { + op: op.as_str(), + ty_kind: "non-numeric", + bad_ty: self.with_ctrct(rhs_ty).to_string(), + span: span.clone(), }, }); } @@ -2044,7 +2036,7 @@ impl Contract { | BinaryOp::Mod => { // Both args must be numeric, i.e., ints or reals; binary op type is same // as arg types. - check_numeric_args(&lhs_ty, rhs_ty, "numeric"); + check_numeric_args(&lhs_ty, rhs_ty); Inference::Type(lhs_ty) } BinaryOp::Equal | BinaryOp::NotEqual => { @@ -2074,27 +2066,44 @@ impl Contract { is_init_constraint = true; } - // Both args must be equatable, which at this stage is any type; binary op - // type is bool. - if !lhs_ty.eq(&self.new_types, rhs_ty) - && !lhs_ty.is_nil() - && !rhs_ty.is_nil() - && !is_init_constraint - && !lhs_ty.is_error() - && !rhs_ty.is_error() - { + // Both args must be equatable, which at this stage is any type *except* + // unions; binary op type is bool. + let lhs_ty_is_union = lhs_ty.is_union(&self.unions); + if lhs_ty_is_union || rhs_ty.is_union(&self.unions) { handler.emit_err(Error::Compile { - error: CompileError::OperatorTypeError { - arity: "binary", - large_err: Box::new(LargeTypeError::OperatorTypeError { - op: op.as_str(), - expected_ty: self.with_ctrct(lhs_ty).to_string(), - found_ty: self.with_ctrct(rhs_ty).to_string(), - span: self.expr_key_to_span(rhs_expr_key), - expected_span: Some(self.expr_key_to_span(lhs_expr_key)), - }), + error: CompileError::OperatorInvalidType { + op: op.as_str(), + ty_kind: "union", + bad_ty: self + .with_ctrct(if lhs_ty_is_union { &lhs_ty } else { rhs_ty }) + .to_string(), + span: span.clone(), }, }); + } else if !lhs_ty.eq(&self.new_types, rhs_ty) { + // Only emit an error if neither side is nil nor error, nor an + // initialiser constraint as per above. + if !lhs_ty.is_nil() + && !rhs_ty.is_nil() + && !lhs_ty.is_error() + && !rhs_ty.is_error() + && !is_init_constraint + { + handler.emit_err(Error::Compile { + error: CompileError::OperatorTypeError { + arity: "binary", + large_err: Box::new(LargeTypeError::OperatorTypeError { + op: op.as_str(), + expected_ty: self.with_ctrct(lhs_ty).to_string(), + found_ty: self.with_ctrct(rhs_ty).to_string(), + span: self.expr_key_to_span(rhs_expr_key), + expected_span: Some( + self.expr_key_to_span(lhs_expr_key), + ), + }), + }, + }); + } } Inference::Type(Type::Primitive { @@ -2108,7 +2117,7 @@ impl Contract { | BinaryOp::GreaterThanOrEqual | BinaryOp::GreaterThan => { // Both args must be ordinal, i.e., ints, reals; binary op type is bool. - check_numeric_args(&lhs_ty, rhs_ty, "numeric"); + check_numeric_args(&lhs_ty, rhs_ty); Inference::Type(Type::Primitive { kind: PrimitiveKind::Bool, span: span.clone(), diff --git a/pintc/tests/basic_tests/bad_nil.pnt b/pintc/tests/basic_tests/bad_nil.pnt index 209cc591..1c758858 100644 --- a/pintc/tests/basic_tests/bad_nil.pnt +++ b/pintc/tests/basic_tests/bad_nil.pnt @@ -22,10 +22,10 @@ predicate test { // binary operator type error // @25..26: unexpected argument for operator `==` // only state variables and next state expressions can be compared to `nil` -// binary operator type error -// @60..63: operator `+` argument has unexpected type `nil` -// binary operator type error -// @100..103: operator `<` argument has unexpected type `nil` +// operator invalid type error +// @56..63: invalid non-numeric type `nil` for operator `+` +// operator invalid type error +// @96..103: invalid non-numeric type `nil` for operator `<` // variable initialization type error // @34..37: variable initializer has unexpected type `nil` // @28..31: expecting type `int` diff --git a/pintc/tests/basic_tests/if_statement_body_type_error.pnt b/pintc/tests/basic_tests/if_statement_body_type_error.pnt index 1719778b..fb661fc2 100644 --- a/pintc/tests/basic_tests/if_statement_body_type_error.pnt +++ b/pintc/tests/basic_tests/if_statement_body_type_error.pnt @@ -67,8 +67,8 @@ predicate test { // binary operator type error // @185..186: operator `&&` argument has unexpected type `int` // @174..186: expecting type `bool` -// binary operator type error -// @271..275: operator `+` argument has unexpected type `bool` -// binary operator type error -// @533..544: operator `+` argument has unexpected type `{int, bool}` +// operator invalid type error +// @267..275: invalid non-numeric type `bool` for operator `+` +// operator invalid type error +// @528..544: invalid non-numeric type `{int, bool}` for operator `+` // >>> diff --git a/pintc/tests/interfaces/bad_address.pnt b/pintc/tests/interfaces/bad_address.pnt index c1a2c257..41b16065 100644 --- a/pintc/tests/interfaces/bad_address.pnt +++ b/pintc/tests/interfaces/bad_address.pnt @@ -45,16 +45,16 @@ predicate Simple { // >>> // typecheck_failure <<< -// binary operator type error -// @202..206: operator `+` argument has unexpected type `bool` +// operator invalid type error +// @198..206: invalid non-numeric type `bool` for operator `+` // address expression type error // @198..206: address expression has unexpected type `int` // @198..206: expecting type `b256` // address expression type error // @242..248: address expression has unexpected type `{int, int}` // @242..248: expecting type `b256` -// binary operator type error -// @359..363: operator `+` argument has unexpected type `bool` +// operator invalid type error +// @355..363: invalid non-numeric type `bool` for operator `+` // address expression type error // @355..363: address expression has unexpected type `int` // @355..363: expecting type `b256` diff --git a/pintc/tests/types/binary_ops.pnt b/pintc/tests/types/binary_ops.pnt index 397db3f3..ea9cf71f 100644 --- a/pintc/tests/types/binary_ops.pnt +++ b/pintc/tests/types/binary_ops.pnt @@ -24,7 +24,7 @@ predicate test { // parsed <<< // enum ::T = FortyTwo | FleventyFive; -// +// // predicate ::test { // var ::a; // var ::b; @@ -54,28 +54,28 @@ predicate test { // >>> // typecheck_failure <<< -// binary operator type error -// @69..74: operator `+` argument has unexpected type `bool` -// binary operator type error -// @93..97: operator `-` argument has unexpected type `bool` -// binary operator type error -// @111..116: operator `*` argument has unexpected type `int[2]` -// binary operator type error -// @135..201: operator `/` argument has unexpected type `b256` -// binary operator type error -// @226..237: operator `%` argument has unexpected type `::T` +// operator invalid type error +// @64..74: invalid non-numeric type `bool` for operator `+` +// operator invalid type error +// @88..97: invalid non-numeric type `bool` for operator `-` +// operator invalid type error +// @111..121: invalid non-numeric type `int[2]` for operator `*` +// operator invalid type error +// @135..206: invalid non-numeric type `b256` for operator `/` +// operator invalid type error +// @221..237: invalid non-numeric type `::T` for operator `%` // binary operator type error // @322..337: operator `==` argument has unexpected type `::T` // @316..318: expecting type `int` // binary operator type error // @357..361: operator `!=` argument has unexpected type `bool` // @351..353: expecting type `int` -// binary operator type error -// @376..380: operator `>` argument has unexpected type `bool` -// binary operator type error -// @407..473: operator `<` argument has unexpected type `b256` -// binary operator type error -// @493..501: operator `<=` argument has unexpected type `int[2]` +// operator invalid type error +// @376..388: invalid non-numeric type `bool` for operator `>` +// operator invalid type error +// @402..473: invalid non-numeric type `b256` for operator `<` +// operator invalid type error +// @487..501: invalid non-numeric type `int[2]` for operator `<=` // binary operator type error // @524..526: operator `&&` argument has unexpected type `int` // @516..526: expecting type `bool` diff --git a/pintc/tests/unions/bad_conditional.pnt b/pintc/tests/unions/bad_conditional.pnt new file mode 100644 index 00000000..2c02bbe8 --- /dev/null +++ b/pintc/tests/unions/bad_conditional.pnt @@ -0,0 +1,29 @@ +union pet = cats(int) | dogs(int) | emu; + +predicate test { + var a: pet; + + constraint pet::cats(11) == a; + constraint a > pet::cats(11); + constraint pet::dogs(22) <= pet::emu; +} + +// parsed <<< +// union ::pet = cats(int) | dogs(int) | emu; +// +// predicate ::test { +// var ::a: ::pet; +// constraint (::pet::cats(11) == ::a); +// constraint (::a > ::pet::cats(11)); +// constraint (::pet::dogs(22) <= ::pet::emu); +// } +// >>> + +// typecheck_failure <<< +// operator invalid type error +// @91..109: invalid union type `::pet` for operator `==` +// operator invalid type error +// @126..143: invalid non-numeric type `::pet` for operator `>` +// operator invalid type error +// @160..185: invalid non-numeric type `::pet` for operator `<=` +// >>> diff --git a/pintc/tests/unions/no_value_union.pnt b/pintc/tests/unions/no_value_union.pnt index 23a551c8..46306914 100644 --- a/pintc/tests/unions/no_value_union.pnt +++ b/pintc/tests/unions/no_value_union.pnt @@ -1,7 +1,7 @@ union either = left | right; predicate test { - var x: either = either::right; + var x: either; // DISABLED until we 'fix' initialisers. = either::right; constraint match x { either::left => true, either::right => false, @@ -9,7 +9,7 @@ predicate test { } predicate decl_test { - var x: either = either::right; + var x: either; // DISABLED until we 'fix' initialisers. = either::right; match x { either::left => { constraint true; @@ -25,13 +25,11 @@ predicate decl_test { // // predicate ::test { // var ::x: ::either; -// constraint (::x == ::either::right); // constraint match ::x { ::either::left => true, ::either::right => false }; // } // // predicate ::decl_test { // var ::x: ::either; -// constraint (::x == ::either::right); // match ::x { // ::either::left => { // constraint true @@ -48,14 +46,12 @@ predicate decl_test { // // predicate ::test { // var ::x: ::either; -// constraint (::x == ::either::right); // constraint ((UnTag(::x) == 0) ? true : false); // constraint __eq_set(__mut_keys(), {0}); // } // // predicate ::decl_test { // var ::x: ::either; -// constraint (::x == ::either::right); // constraint (!(UnTag(::x) == 0) || true); // constraint ((UnTag(::x) == 0) || (!(UnTag(::x) == 1) || false)); // constraint __eq_set(__mut_keys(), {0}); diff --git a/pintc/tests/unions/simple.pnt b/pintc/tests/unions/simple.pnt index 26b6339d..94989661 100644 --- a/pintc/tests/unions/simple.pnt +++ b/pintc/tests/unions/simple.pnt @@ -49,19 +49,17 @@ predicate test { } // Constraining an address to either zero or something. - var no_base_addr: maydr = maybe_addr::no_addr; - var a_base_addr: maydr = maybe_addr::addr(0x1111111111111111111111111111111111111111111111111111111111111111); + // + // DISABLED until we 'fix' initialisers. These initialisers would generate constraints like + // `no_bad_addr == maybe_addr::no_bad_addr` but `==` is illegal for unions. + // + //var no_base_addr: maydr = maybe_addr::no_addr; + //var a_base_addr: maydr = maybe_addr::addr(0x1111111111111111111111111111111111111111111111111111111111111111); - var actual_addr = match no_base_addr { - maybe_addr::no_addr => 0x0000000000000000000000000000000000000000000000000000000000000000, - maybe_addr::addr(a) => a, - }; - - // Direct comparisons. - constraint no_base_addr != a_base_addr; - constraint no_base_addr == maybe_addr::no_addr; - constraint thing::b(77) == thing::b(77); - constraint thing::b(88) != thing::b(99); + //var actual_addr = match no_base_addr { + // maybe_addr::no_addr => 0x0000000000000000000000000000000000000000000000000000000000000000, + // maybe_addr::addr(a) => a, + //}; } // parsed <<< @@ -73,19 +71,9 @@ predicate test { // predicate ::test { // var ::x: ::thing; // var ::d: int; -// var ::no_base_addr: ::maydr; -// var ::a_base_addr: ::maydr; -// var ::actual_addr; // constraint match ::x { ::thing::a(b) => ::b, ::thing::b(n) => (::n > 0), ::thing::c(t) => ((::t.0 + ::t.1) == 11) }; // constraint (match ::x { ::thing::b(b) => ::b, else => 22 } > 0); // constraint match ::x { ::thing::a(b) => ::b, ::thing::b(n) => constraint (::n > 0); ((::n * 2) < 10), ::thing::c(t) => constraint (::t.0 == 33); constraint (::t.1 != 44); true }; -// constraint (::no_base_addr == ::maybe_addr::no_addr); -// constraint (::a_base_addr == ::maybe_addr::addr(0x1111111111111111111111111111111111111111111111111111111111111111)); -// constraint (::actual_addr == match ::no_base_addr { ::maybe_addr::no_addr => 0x0000000000000000000000000000000000000000000000000000000000000000, ::maybe_addr::addr(a) => ::a }); -// constraint (::no_base_addr != ::a_base_addr); -// constraint (::no_base_addr == ::maybe_addr::no_addr); -// constraint (::thing::b(77) == ::thing::b(77)); -// constraint (::thing::b(88) != ::thing::b(99)); // match ::x { // ::thing::a(b) => { // } @@ -109,19 +97,9 @@ predicate test { // predicate ::test { // var ::x: ::thing; // var ::d: int; -// var ::no_base_addr: ::maybe_addr; -// var ::a_base_addr: ::maybe_addr; -// var ::actual_addr: b256; // constraint ((UnTag(::x) == 0) ? UnVal(::x, bool) : ((UnTag(::x) == 1) ? (UnVal(::x, int) > 0) : ((UnVal(::x, {int, int}).0 + UnVal(::x, {int, int}).1) == 11))); // constraint (((UnTag(::x) == 1) ? UnVal(::x, int) : 22) > 0); // constraint ((UnTag(::x) == 0) ? UnVal(::x, bool) : ((UnTag(::x) == 1) ? ((UnVal(::x, int) * 2) < 10) : true)); -// constraint (::no_base_addr == ::maybe_addr::no_addr); -// constraint (::a_base_addr == ::maybe_addr::addr(0x1111111111111111111111111111111111111111111111111111111111111111)); -// constraint (::actual_addr == ((UnTag(::no_base_addr) == 0) ? 0x0000000000000000000000000000000000000000000000000000000000000000 : UnVal(::no_base_addr, b256))); -// constraint (::no_base_addr != ::a_base_addr); -// constraint (::no_base_addr == ::maybe_addr::no_addr); -// constraint (::thing::b(77) == ::thing::b(77)); -// constraint (::thing::b(88) != ::thing::b(99)); // constraint ((UnTag(::x) == 0) || (!(UnTag(::x) == 2) || ((UnVal(::x, {int, int}).0 * UnVal(::x, {int, int}).1) == 66))); // constraint ((UnTag(::x) == 0) || (!(UnTag(::x) == 2) || (::d == (UnVal(::x, {int, int}).0 - UnVal(::x, {int, int}).1)))); // constraint ((UnTag(::x) == 0) || ((UnTag(::x) == 2) || (::d == 55)));