unary and binary operation typing

[pataei]

P4 states that when sub-expressions in expressions with unary/binary expressions have type int, they must be compile-time-known. However, Petr4 doesn't check this and freely allows them to just have int type without being compile-time-know.

Petr4 code

It can be found in checker.ml.

let assert_bool = make_assert "bool"
  begin function
  | Bool -> Some Type.Bool
  | _ -> None
  end

let assert_bit = make_assert "unsigned int"
  begin function
  | Bit { width } -> Some (Type.Bit { width })
  | _ -> None
  end

(* numeric(t) <=> t = int \/ t = int<n> \/ t = bit<n> *)
let assert_numeric = make_assert "integer"
  begin function
  | Integer -> Some None
  | Int typ
  | Bit typ -> Some (Some typ)
  | _ -> None
  end

let assert_runtime_numeric = make_assert "bit<> or int<>"
  begin function
  | Int typ
  | Bit typ -> Some typ
  | _ -> None
  end

let type_unary_op env ctx op arg =
  let arg_typed = type_expression env ctx arg in
  let arg_typ = arg_typed.typ in
  begin match op with
  | Not    _ -> assert_bool (Types.Expression.tags arg) arg_typ |> ignore
  | BitNot _ -> assert_runtime_numeric (Types.Expression.tags arg) arg_typ |> ignore
  | UMinus _ -> assert_numeric (Types.Expression.tags arg) arg_typ |> ignore
  end;
  { expr = UnaryOp { op = op;
                     arg = arg_typed;
                     tags = Info.dummy};
    typ = arg_typ;
    dir = arg_typed.dir;
    tags = Info.dummy}

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 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
  let r_typ = reduce_enums_in_type env typed_r.typ in
  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 *)
       (* TODO: discuss with Ryan. discrepency with spec. *)
    | 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 *)
    (* TODO: discuss with Ryan. discrepency with spec. *)
    | 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 *)
       (* TODO: discuss with Ryan. then why do we allow it for bit<w> too?*)
    | 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
       (* TODO: check this with Ryan. section 8.5 of spec.  *)
    | 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.

The type int denotes arbitrary-precision integers. In P4, all expressions of type int must be compile-time known values.

[pataei]

The scenario of having binary/unary operation on a non-compile-time-known is almost non-existent. However, it would be good to have the check. It's low priority.