Fixes to import tool for set expressions in select statements, fixes …

…to parsing scripts

hol/p4_from_json/excluded.sml

@@ -74,9 +74,9 @@ val exclude_descs =
    ["decl-soundness",
     "enum-bmv2"]),
 (*
-    To-bool cast (manually spotted)
+    More expressive STF specifications
 *)
-  ("supporting to-bool cast in HOL4P4",
+  ("more expressive STF specifications",
    ["issue1814-1-bmv2"]),
 (*
     To-struct cast (manually spotted)
@@ -101,13 +101,10 @@ val exclude_descs =
     "key-issue-1020_ebpf",
     "switch_ebpf"]),
 (*
-    Set expressions in select expression
-    FAIL: Could not parse .*\/(.*?)\. .*?: \["range".*
+    If-expressions
 *)
-  ("adding set expressions in select expressions to HOL4P4",
-   ["issue995-bmv2",
-    "issue1000-bmv2",
-    "issue-2123-2-bmv2",
+  ("adding if-expressions to HOL4P4",
+   ["issue-2123-2-bmv2",
     "issue-2123-3-bmv2"]),
 (*
     Exit statement

hol/p4_from_json/petr4_get_arch.sh

@@ -7,6 +7,8 @@ elif grep -q "#include \"very_simple_model.p4\"" "$1"; then
     echo "vss"
 elif grep -q "#include <v1model.p4>" "$1"; then
     echo "v1model"
+elif grep -q "#include \"v1model.p4\"" "$1"; then
+    echo "v1model"
 else
     echo "none"
 fi

hol/p4_from_json/petr4_to_hol4p4.sh

@@ -22,7 +22,7 @@ fi
 arch=$(./petr4_get_arch.sh "${JSON_PATH%.json}.p4")
 
 if [ "$arch" = "none" ]; then
-    echo "No architecture found in the associated .p4 file. Check that your P4 program uses a proper architecture, or adapt petr4_get_arch.sh to recognize the right architecture."
+    echo "No architecture found in ${JSON_PATH%.json}.p4. Check that your P4 program uses a proper architecture, or adapt petr4_get_arch.sh to recognize the right architecture."
     exit 1
 fi
 

hol/p4_from_json/petr4_to_hol4p4Script.sml

@@ -821,6 +821,7 @@ Datatype:
   | Exp e
   (* table.apply().action_run expression to be inlined *)
   | InlineApp (string list) e
+  | SetExp s
 End
 
 Definition msg_opt_INL_def:
@@ -854,6 +855,16 @@ Definition get_typeinf_dummy_args_def:
    | NONE => get_error_msg "could not transform extern function's type arguments to dummy arguments: " (Array tyargs)
 End
 
+Definition get_bitv_of_e_def:
+ get_bitv_of_e e =
+  case e of
+  | e_v v =>
+   (case v of
+    | v_bit bitv => SOME bitv
+    | _ => NONE)
+  | _ => NONE
+End
+
 (* TODO: Use OPTION_BIND, parse_arr and parse_obj *)
 Definition petr4_parse_expression_gen_def:
 (petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (exp, p_tau_opt) =
@@ -952,15 +963,19 @@ Definition petr4_parse_expression_gen_def:
         | Number op_const =>
          SOME_msg (Exp (e_v (v_bit (fixwidth n (n2v op_const), n))))
         | InlineApp s_l app_exp =>
-         get_error_msg "apply expression unsupported for casts: " op)
+         get_error_msg "apply expression unsupported for casts: " op
+        | SetExp set_exp =>
+         get_error_msg "apply expression unsupported for set expressions: " op)
       | SOME tau_bool =>
        (case res_op of
         | Exp op_exp =>
          SOME_msg (Exp (e_cast cast_bool op_exp))
         | Number op_const =>
          SOME_msg (Exp (e_v (v_bool (HD $ REVERSE (n2v op_const)))))
         | InlineApp s_l app_exp =>
-         get_error_msg "apply expression unsupported for casts: " op)
+         get_error_msg "apply expression unsupported for casts: " op
+        | SetExp set_exp =>
+         get_error_msg "apply expression unsupported for set expressions: " op)
       | SOME _ => get_error_msg "unsupported cast type: " cast_type
       | NONE => get_error_msg "unknown cast type: " cast_type)
     | NONE_msg op_msg => NONE_msg op_msg)
@@ -1010,7 +1025,7 @@ Definition petr4_parse_expression_gen_def:
              SOME_msg (Exp (mk_binop (e_v (v_bit (fixwidth n (n2v op1_const), n))) op2_exp))
             | SOME _ => get_error_msg "non-bitstring type inference unsupported for expression: " exp
             | NONE => get_error_msg "type inference failed for expression: " exp)
-          | _ => get_error_msg "expression contains binop on constants or apply exp: " exp)
+          | _ => get_error_msg "expression contains binop on constants, apply exp or set exp: " exp)
         | NONE_msg op2_msg => NONE_msg op2_msg)
       | NONE_msg op1_msg => NONE_msg op1_msg)
     | NONE => NONE_msg ("unknown optype: "++optype))
@@ -1133,6 +1148,46 @@ Definition petr4_parse_expression_gen_def:
     | SOME_msg exp_list_res =>
      SOME_msg (Exp (e_struct (ZIP(MAP toString $ TL $ COUNT_LIST ((LENGTH exp_list_res) + 1), exp_list_res))))
     | NONE_msg exps_msg => NONE_msg ("could not parse tuple element: "++exps_msg))
+  (* Mask (set expression) *)
+  | Array [String "mask";
+           Object [("tags", tags);
+                   ("expr", expr);
+                   ("mask", mask)]] =>
+   (case petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (expr, p_tau_opt) of
+    | SOME_msg (Exp res_expr) =>
+     (case petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (mask, p_tau_opt) of
+      | SOME_msg (Exp res_mask) =>
+       (case get_bitv_of_e res_expr of
+        | SOME bitv =>
+         (case get_bitv_of_e res_mask of
+          | SOME bitv' =>
+           SOME_msg $ SetExp $ s_mask bitv bitv'
+          | NONE => get_error_msg "non-bitvector as mask: " exp)
+        | NONE => get_error_msg "non-bitvector as masked bitstring: " exp)
+      | _ => get_error_msg "unexpected mask: " exp
+      | NONE_msg mask_msg => NONE_msg mask_msg)
+    | _ => get_error_msg "unexpected masked bitstring: " exp
+    | NONE_msg expr_msg => NONE_msg expr_msg)
+  (* Range (set expression) *)
+  | Array [String "range";
+           Object [("tags", tags);
+                   ("lo", lo);
+                   ("hi", hi)]] =>
+   (case petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (lo, p_tau_opt) of
+    | SOME_msg $ Exp res_lo =>
+     (case petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (hi, p_tau_opt) of
+      | SOME_msg $ Exp res_hi =>
+       (case get_bitv_of_e res_lo of
+        | SOME bitv =>
+         (case get_bitv_of_e res_hi of
+          | SOME bitv' =>
+           SOME_msg $ SetExp $ s_range bitv bitv'
+          | NONE => get_error_msg "non-bitvector as interval lower bound: " exp)
+        | NONE => get_error_msg "non-bitvector as interval upper bound: " exp)
+      | _ => get_error_msg "unexpected interval upper bound: " exp
+      | NONE_msg hi_msg => NONE_msg hi_msg)
+    | _ => get_error_msg "unexpected interval lower bound: " exp
+    | NONE_msg lo_msg => NONE_msg lo_msg)
   | _ => get_error_msg "unknown JSON format of expression: " exp) /\
 (* TODO: Use OPTION_BIND, parse_arr and parse_obj *)
  (petr4_parse_args (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) [] =
@@ -1155,6 +1210,7 @@ Definition petr4_parse_expression_gen_def:
        | SOME other_tau => get_error_msg "non-bitstring type inference unsupported for exp: " exp
        | NONE => get_error_msg "type inference information missing for function argument: " exp)
      | SOME_msg (InlineApp s_l exp_app) => get_error_msg "apply expressions as arguments disallowed by import tool: " exp
+     | SOME_msg (SetExp set_exp) => get_error_msg "set expressions as arguments disallowed by import tool: " exp
      | NONE_msg exp_msg => NONE_msg ("could not parse arguments: "++exp_msg)
    else NONE_msg ("unsupported argument type: "++argtype)
   | _ => get_error_msg "unknown JSON format of argument: " (FST h)) /\
@@ -1168,7 +1224,8 @@ Definition petr4_parse_expression_gen_def:
     (case petr4_parse_expressions (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) t of
      | SOME_msg exps_res => SOME_msg (exp_res::exps_res)
      | NONE_msg exps_msg => NONE_msg exps_msg)
-   | NONE_msg exp_msg => NONE_msg ("could not parse expression: "++exp_msg))
+  | SOME_msg (SetExp e) => get_error_msg "set expression in unsupported location: " h1
+  | NONE_msg exp_msg => NONE_msg ("could not parse expression: "++exp_msg))
 Termination
 WF_REL_TAC `measure ( \ t. case t of
                            | (INL (maps, json, p_tau_opt)) => json_size json
@@ -1197,6 +1254,7 @@ Definition petr4_parse_expression_def:
   | SOME_msg (Number n) => get_error_msg "no type inference information provided for integer constant: " exp
   | SOME_msg (Exp e) => SOME_msg e
   | SOME_msg (InlineApp s_l e) => get_error_msg "apply expression in unsupported location: " exp
+  | SOME_msg (SetExp s) => get_error_msg "set expression in unsupported location: " exp
   | NONE_msg exp_msg => NONE_msg ("could not parse value: "++exp_msg)
 End
 
@@ -1743,23 +1801,21 @@ Definition petr4_parse_direct_application_def:
            SOME_msg ([], [], [], [], [], stmt_app app_name keys))
         | NONE =>
          (* TODO: Does the below work if we just skip the lookup and switch block_type_name for app_name? *)
-         (case ALOOKUP vtymap (varn_name app_name) of
-          | SOME (p_tau_blk block_type_name) =>
 
-           (case ALOOKUP pblock_map block_type_name of
+           (case ALOOKUP pblock_map app_name of
             | SOME ((pbl_type_control, params, b_func_map, decl_list, pars_map, tbl_map):pblock_extra, param_types) =>
-             (case FIND_EXTRACT_ONE (\ (k,v). k = block_type_name) b_func_map of
+             (case FIND_EXTRACT_ONE (\ (k,v). k = app_name) b_func_map of
               (* Params has format (string # dir) *)
               | SOME ((name, (body, params')), b_func_map') =>
                (case petr4_parse_args (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (ZIP (args, MAP SOME (parameterise_taus param_types))) of
                 | SOME_msg res_args =>
                  if p4_stmt_contains_return body
-                 then NONE_msg ("nested control block "++(app_name++(" of type "++(block_type_name++" contains a return statement, which is unsupported by the inlining scheme"))))
+                 then NONE_msg ("nested control block "++(app_name++(" of type "++(app_name++" contains a return statement, which is unsupported by the inlining scheme"))))
                  else
                   (* Prefixing of variables, tables and functions in body happens here *)
                   (case petr4_inline_block gscope app_name (p4_prefix_vars_tbls_funs_in_stmt gscope b_func_map app_name body) [] stmt_empty stmt_empty (ZIP(params, ZIP(res_args, param_types))) of
                    | SOME_msg (decl_list', stmt) =>
-                    (case ALOOKUP tbl_entries_map block_type_name of
+                    (case ALOOKUP tbl_entries_map app_name of
                      | SOME tbl_entries =>
                       (* TODO: Prefixing of variables in decl_list happens here - also prove it is OK *)
                       let inline_decl_list = p4_prefix_decl_list gscope app_name (decl_list'++decl_list) in
@@ -1772,14 +1828,11 @@ Definition petr4_parse_direct_application_def:
                                 (* List of taboo variable names *)
                                 MAP FST inline_decl_list,
                                 stmt)
-                     | NONE => NONE_msg ("could not find control block in tbl_entries_map: "++block_type_name))
+                     | NONE => NONE_msg ("could not find control block in tbl_entries_map: "++app_name))
                    | NONE_msg inline_msg => NONE_msg inline_msg)
                 | NONE_msg args_msg => NONE_msg ("could not parse nested control block: "++args_msg))
-              | NONE => NONE_msg ("could not find instantiation of nested control block: "++block_type_name))
-            | _ => NONE_msg ("could not find control block: "++block_type_name))
-
-               | _ =>
-                NONE_msg ("could not find entry of control block name "++app_name++" in value-type map (has it been instantiated in the block?)"))
+              | NONE => NONE_msg ("could not find instantiation of nested control block: "++app_name))
+            | _ => NONE_msg ("could not find control block: "++app_name))
 
         | _ =>
          NONE_msg ("could not find entry of table name "++app_name++" in apply map"))
@@ -3151,13 +3204,20 @@ Definition petr4_parse_matches_def:
   case h of
   | Array [String "Expression";
            Object [("tags", tags); ("expr", exp)]] =>
-   (* TODO: Note that this is technically more restrictive than the P4 definition, where select cases are expressions,
-    *       not necessarily values. Most targets probably restrict to values in practice though. *)
-   (case petr4_parse_value (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (exp, SOME expected_tau) of
-     | SOME_msg val_res =>
+   (case petr4_parse_expression_gen (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) (exp, SOME expected_tau) of
+     | SOME_msg (Exp exp_res) =>
+      (case exp_res of
+       | e_v v_res =>
+        (case petr4_parse_matches (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) t of
+         | SOME_msg matches_res => SOME_msg ((s_sing v_res)::matches_res)
+         | NONE_msg matches_msg => NONE_msg matches_msg)
+       | _ => get_error_msg "non-value, non-set expressions unsupported as select match cases: " h)
+
+     | SOME_msg (SetExp set_exp_res) =>
       (case petr4_parse_matches (tyenv, enummap, vtymap, ftymap, gscope, extfun_list) t of
-       | SOME_msg matches_res => SOME_msg ((s_sing val_res)::matches_res)
+       | SOME_msg matches_res => SOME_msg (set_exp_res::matches_res)
        | NONE_msg matches_msg => NONE_msg matches_msg)
+     | SOME_msg _ => get_error_msg "unexpected select match case: " h
      | NONE_msg exp_msg => NONE_msg ("could not parse select match case: "++exp_msg))
   | Array [String "Default";
            Object [("tags", tags)]] =>

hol/p4_from_json/petr4_to_hol4p4_symb.sh

@@ -22,7 +22,7 @@ fi
 arch=$(./petr4_get_arch.sh "${JSON_PATH%.json}.p4")
 
 if [ "$arch" = "none" ]; then
-    echo "No architecture found in the associated .p4 file. Check that your P4 program uses a proper architecture, or adapt petr4_get_arch.sh to recognize the right architecture."
+    echo "No architecture found in ${JSON_PATH%.json}.p4. Check that your P4 program uses a proper architecture, or adapt petr4_get_arch.sh to recognize the right architecture."
     exit 1
 fi