Each of the following issues is referred to in Petr4 code with their number for reference.
Petr4 reduces an enum to its underlying type while P4 spec inserts an implicit cast (find it in check_binary_op function).
For example, P4 spec has this example: 16w11 << E.a becomes 16w11 << (bit<8>)E.a where
enum bit<8> E {
a = 5
}
Petr4 inserts an implicit cast for saturating operators and bitwise operations except for concatenation (find it in coerce_binary_op_args). However, P4 spec doesn't explicitly state anything regarding such insertion of cast, it also doesn't have any such example. What's the expected behavior?
Petr4 allows operands of division and modulo be bit<w> or int<w> (find it in check_binary_op function, pattern match for | Div {tags} | Mod {tags} -> ...). However, P4 spec only allows such operands to be integers.
Petr4 inserts implicit cast based on the type of two operands only for integers and it reduces the enums. This doesn't necessarily conflict with P4 spec except for bitstring access but it can be simplified. We should discuss how the formalization is inserting implicit casts in binary operations rules section.
Petr4 code
let type_binary_op (env : CheckerEnv.t) (ctx : ExprContext.t) (op: Op.bin) ((l, r) : (Expression.t * Expression.t)) : Prog.Expression.t =
let typed_l, typed_r = coerce_binary_op_args env ctx op l r in
check_binary_op env op typed_l typed_r
and coerce_binary_op_args env ctx op l r =
let l_typed = type_expression env ctx l in
let r_typed = type_expression env ctx r in
let cast typ (expr : Prog.Expression.t) : Prog.Expression.t =
{ expr = Cast { typ = typ;
expr = expr;
tags = Info.dummy };
typ = typ;
dir = expr.dir;
tags = Info.dummy}
in
let cast_opt = function
| Some typ -> cast typ
| None -> fun e -> e
in
let cast_type_l, cast_type_r = implicit_cast env l_typed r_typed in
let is_shl op =
match op with
| Op.Shl {tags} -> true
| _ -> false
in
let is_shr op =
match op with
| Op.Shr {tags} -> true
| _ -> false
in
let is_pluplus op =
match op with
| Op.PlusPlus {tags} -> true
| _ -> false
in
if not (is_shl op) && not (is_shr op) && not (is_pluplus op) (*ISSUE NUMBER 2: only these operations do not insert implicit casts*)
then cast_opt cast_type_l l_typed, cast_opt cast_type_r r_typed
else l_typed, r_typed
and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
let open Op in
let open Prog.Expression in
let open Typed.Type in
let l_typ = reduce_enums_in_type env typed_l.typ in (*ISSUE NUMBER 1*)
let r_typ = reduce_enums_in_type env typed_r.typ in (*ISSUE NUMBER 1*)
let dir =
match typed_l.dir, typed_r.dir with
| In, In -> In
| _ -> Directionless
in
let typ =
match op with
| And {tags} | Or {tags} ->
begin match l_typ, r_typ with
| Bool, Bool -> Bool
| Bool, r -> raise_mismatch (tags) "Operand must be a bool" r
| l, r -> raise_mismatch (tags) "Operand must be a bool" l
end
(* Basic numeric operations are defined on both arbitrary and fixed-width integers *)
| Plus {tags} | Minus {tags} | Mul {tags} ->
begin match l_typ, r_typ with
| Integer, Integer -> Integer
| Bit { width = l }, Bit { width = r } when l = r -> Bit { width = l }
| Int { width = l }, Int { width = r } when l = r -> Int { width = l }
| _, _ -> raise_s [%message "this binop unimplemented"
~l_typ:(l_typ:Typed.Type.t)
~r_typ:(r_typ:Typed.Type.t)]
end
| Eq {tags} | NotEq {tags} ->
if type_equality env [] l_typ r_typ
then if type_has_equality_tests env l_typ
then Type.Bool
else raise_s [%message "bad error message: type doesn't have equality tests (== and !=)"
~l_typ:(l_typ:Typed.Type.t)
~r_typ:(r_typ:Typed.Type.t)]
else raise_type_error tags (Type_Difference (l_typ, r_typ))
(* Saturating operators are only defined on finite-width signed or unsigned integers *)
| PlusSat {tags} | MinusSat {tags} ->
begin match l_typ, r_typ with
| Bit { width = l }, Bit { width = r } when l = r ->
Bit { width = l }
| Int { width = l }, Int { width = r } when l = r ->
Int { width = l }
| Bit _, r | Int _, r ->
raise_mismatch (tags) "Operand must have type int<w> or bit<w>" r
| l, r ->
raise_mismatch (tags) "Operand must have type int<w> or bit<w>" l
end
(* Bitwise operators are only defined on bitstrings of the same width *)
| BitAnd {tags} | BitXor {tags} | BitOr {tags} ->
begin match l_typ, r_typ with
| Bit { width = l }, Bit { width = r } when l = r -> Bit { width = l }
| Int { width = l }, Int { width = r } when l = r -> Int { width = l }
| Bit { width = _ }, _ -> raise_mismatch (typed_r.tags) "unsigned int" r_typ
| _, _ -> raise_mismatch (typed_l.tags) "unsigned int" l_typ
end
(* Bitstring concatentation is defined on any two bitstrings *)
| PlusPlus {tags} ->
begin match l_typ, r_typ with
| Bit { width = l }, Bit { width = r }
| Bit { width = l }, Int { width = r } -> Bit { width = l + r }
| Int { width = l }, Bit { width = r }
| Int { width = l }, Int { width = r } -> Int { width = l + r }
| Int { width = _ }, _
| Bit { width = _ }, _ -> raise_mismatch (typed_r.tags) "bit<> or int<>" r_typ
| _, _ -> raise_mismatch (typed_l.tags) "bit<> or int<>" l_typ
end
(* Comparison is defined on both arbitrary and fixed-width integers *)
| Le {tags} | Ge {tags} | Lt {tags} | Gt {tags} ->
begin match l_typ, r_typ with
| Integer, Integer -> Bool
| Bit { width = l }, Bit { width = r } when l = r -> Bool
| Int { width = l }, Int { width = r } when l = r -> Bool
| _, _ -> raise_type_error tags (Type_Difference (l_typ, r_typ))
end
(* Division is only defined on compile-time known arbitrary-precision positive integers *)
(* ISSUE NUMBER 3*)
| Div {tags} | Mod {tags} ->
begin match l_typ, r_typ with
| Integer, Integer ->
check_div_args env typed_l typed_r;
Integer
| Bit { width = l_width }, Bit { width = r_width } when l_width = r_width ->
check_div_args env typed_l typed_r;
Bit { width = l_width }
| Integer, _ -> raise_mismatch (typed_r.tags) "arbitrary precision integer" r_typ
| _, _ -> raise_mismatch (typed_l.tags) "arbitrary precision integer" l_typ
end
| Shl {tags} | Shr {tags} ->
begin match l_typ, is_nonnegative_numeric env typed_r with
| Bit _, true
| Int _, true -> l_typ
| Integer, true ->
if compile_time_known_expr env typed_r
then l_typ
else raise_s [%message "bad right hand argument to shift" ~typed_r:(typed_r: Prog.Expression.t)]
| _, true -> raise_s [%message "bad left hand argument to shift" ~l_typ:(l_typ: Typed.Type.t)]
| _ -> raise_s [%message "bad right hand argument to shift" ~typed_r:(typed_r: Prog.Expression.t)]
end
in
{ expr = BinaryOp { op = op; args = (typed_l, typed_r); tags = tags_bin op };
typ = typ;
dir = dir;
tags = tags_bin op}
P4 spec version 1.2.3
Operations on arbitrary-precision integers include:
Truncating integer division between positive values, denoted by /.
Modulo between positive values, denoted by %.
Note: bitwise-operations (|,&,^,~) are not defined on expressions of type int. In addition, it is illegal to apply division and modulo to negative values.
Note: saturating arithmetic is not supported for arbitrary-precision integers.
To keep the language simple and avoid introducing hidden costs, P4 only implicitly casts from int to fixed-width types and from enums with an underlying type to the underlying type. In particular, applying a binary operation (except shifts and concatenation) to an expression of type int and an expression with a fixed-width type will implicitly cast the int expression to the type of the other expression. For enums with an underlying type, it can be implicitly cast to its underlying type whenever appropriate, including but not limited to in shifts, concatenation, bit slicing indexes, header stack indexes as well as other unary and binary operations.
For example, given the following declarations,
enum bit<8> E {
a = 5
}
bit<8> x;
bit<16> y;
int<8> z;
the compiler will add implicit casts as follows:
x + 1 becomes x + (bit<8>)1z < 0 becomes z < (int<8>)0x | 0xFFF becomes x | (bit<8>)0xFFF; overflow warning
x + E.a becomes x + (bit<8>)E.ax << 256 remains unchanged; 256 not implicitly cast to 8w0 in a shift; overflow warning
16w11 << E.a becomes 16w11 << (bit<8>)E.ax[E.a:0] becomes x[(bit<8>)E.a:0]E.a ++ 8w0 becomes (bit<8>)E.a ++ 8w0
Each of the following issues is referred to in Petr4 code with their number for reference.
check_binary_opfunction).For example, P4 spec has this example:
16w11 << E.abecomes16w11 << (bit<8>)E.awherecoerce_binary_op_args). However, P4 spec doesn't explicitly state anything regarding such insertion of cast, it also doesn't have any such example. What's the expected behavior?bit<w>orint<w>(find it incheck_binary_opfunction, pattern match for| Div {tags} | Mod {tags} -> ...). However, P4 spec only allows such operands to be integers.Petr4 code
P4 spec version 1.2.3
Operations on arbitrary-precision integers include:
Note: bitwise-operations
(|,&,^,~)are not defined on expressions of type int. In addition, it is illegal to apply division and modulo to negative values.Note: saturating arithmetic is not supported for arbitrary-precision integers.
To keep the language simple and avoid introducing hidden costs, P4 only implicitly casts from int to fixed-width types and from enums with an underlying type to the underlying type. In particular, applying a binary operation (except shifts and concatenation) to an expression of type int and an expression with a fixed-width type will implicitly cast the int expression to the type of the other expression. For enums with an underlying type, it can be implicitly cast to its underlying type whenever appropriate, including but not limited to in shifts, concatenation, bit slicing indexes, header stack indexes as well as other unary and binary operations.
For example, given the following declarations,
the compiler will add implicit casts as follows:
x + 1becomesx + (bit<8>)1z < 0becomesz < (int<8>)0x | 0xFFFbecomesx | (bit<8>)0xFFF; overflow warningx + E.abecomesx + (bit<8>)E.ax << 256remains unchanged;256not implicitly cast to8w0in a shift; overflow warning16w11 << E.abecomes16w11 << (bit<8>)E.ax[E.a:0]becomesx[(bit<8>)E.a:0]E.a ++ 8w0becomes(bit<8>)E.a ++ 8w0