Merge pull request #48 from kth-step/dev_bool_cast

Cast to bool

Author: AnoudAlshnakat

hol/p4Script.sml

@@ -94,6 +94,7 @@ binop =
 val _ = Hol_datatype ` 
 cast = 
    cast_unsigned of m (* unsigned cast *)
+ | cast_bool (* bool cast *)
 `;
 val _ = Hol_datatype ` 
 unop = 
@@ -343,6 +344,14 @@ val bool_cast_def = Define `
   bool_cast n' b = (fixwidth n' [b], n')
 `;
 
+val to_bool_cast_def = Define `
+  to_bool_cast (bl, n) = HD $ REVERSE bl
+`;
+
+val id_bool_cast_def = Define `
+  id_bool_cast b = b
+`;
+
 val bitv_bl_binop_def = Define `
   bitv_bl_binop binop (bl, n) (bl', n') = (fixwidth n (binop bl bl'), n)
 `;
@@ -2325,6 +2334,18 @@ Inductive e_sem:
  ==> 
 ( ( e_red ctx g_scope_list scope_list (e_cast (cast_unsigned n) (e_v (v_bool  b ))) (e_v (v_bit bitv))  ([]:frame list)  )))
 
+[e_cast_to_bool:] (! (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (bitv:bitv) (b:b) .
+(clause_name "e_cast_to_bool") /\
+(( (to_bool_cast  bitv  =  b ) ))
+ ==> 
+( ( e_red ctx g_scope_list scope_list (e_cast cast_bool (e_v (v_bit bitv))) (e_v (v_bool  b ))  ([]:frame list)  )))
+
+[e_cast_id_bool:] (! (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (b:b) (b':b) .
+(clause_name "e_cast_id_bool") /\
+(( (id_bool_cast  b  =  b' ) ))
+ ==> 
+( ( e_red ctx g_scope_list scope_list (e_cast cast_bool (e_v (v_bool  b ))) (e_v (v_bool  b' ))  ([]:frame list)  )))
+
 [e_mul:] (! (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (bitv:bitv) (bitv':bitv) (bitv'':bitv) .
 (clause_name "e_mul") /\
 (( (bitv_binop binop_mul  bitv   bitv'  = SOME  bitv'' ) ))
@@ -3324,6 +3345,12 @@ Inductive e_typ:
 ( ? b tp. ( e_typ  t_scopes_tup   T_e   e  tp b /\ ? n . ( tp = t_tau (tau_bit n) \/ tp = t_tau (tau_bool ) ) ) ))
  ==> 
 ( ( e_typ t_scopes_tup T_e (e_cast (cast_unsigned n) e) (t_tau (tau_bit  n ))  F  )))
+
+[e_typ_cast_to_bool:] (! (t_scopes_tup:t_scopes_tup) (T_e:T_e) (e:e) (tau:tau) (b:b) .
+(clause_name "e_typ_cast_to_bool") /\
+(( ? b tp. ( e_typ  t_scopes_tup   T_e   e  tp b /\ ? n . ( tp = t_tau (tau_bit n) \/ tp = t_tau (tau_bool ) ) ) ))
+ ==> 
+( ( e_typ t_scopes_tup T_e (e_cast cast_bool e) (t_tau tau_bool)  F  )))
 End
 (** definitions *)
 

hol/p4_e_progressScript.sml

@@ -1637,14 +1637,19 @@ Cases_on `is_const e` >| [
 
  (*from the typing rules we know *)
  Cases_on ‘c’ >>
- gvs[] >>
-               
- OPEN_EXP_TYP_TAC ``(e_cast (cast_unsigned n) (e_v v))`` >> fs[] >>
- OPEN_EXP_TYP_TAC ``e_v v`` >> fs[] >>
-
- gvs[Once e_sem_cases]  >>                
- OPEN_V_TYP_TAC ``v`` >> gvs[clause_name_def] 
- ,
+ gvs[] >| [            
+  OPEN_EXP_TYP_TAC ``(e_cast (cast_unsigned n) (e_v v))`` >> fs[] >>
+  OPEN_EXP_TYP_TAC ``e_v v`` >> fs[] >> (
+   gvs[Once e_sem_cases]  >>                
+   OPEN_V_TYP_TAC ``v`` >> gvs[clause_name_def]
+  ),
+
+  OPEN_EXP_TYP_TAC ``(e_cast cast_bool (e_v v))`` >> fs[] >>
+  OPEN_EXP_TYP_TAC ``e_v v`` >> fs[] >> (
+   gvs[Once e_sem_cases]  >>                
+   OPEN_V_TYP_TAC ``v`` >> gvs[clause_name_def]
+  )
+ ],
 
 
  OPEN_EXP_TYP_TAC ``(e_cast c e)`` >>

hol/p4_e_subject_reductionScript.sml

@@ -5557,14 +5557,28 @@ REPEAT STRIP_TAC >| [
     gvs[Once e_typ_cases] >>
     gvs[Once v_typ_cases] >>
     gvs[Once v_typ_cases] >>
-    METIS_TAC[bv_casting_length2]    
-    ,
+    METIS_TAC[bv_casting_length2],
+    
     OPEN_EXP_TYP_TAC ``e_cast (cast_unsigned n) (e_v (v_bool b'))`` >>
     gvs[Once e_typ_cases] >>
     gvs[Once e_typ_cases] >>
     gvs[Once v_typ_cases] >>
     gvs[Once v_typ_cases] >>
-    METIS_TAC[bool_casting_length, clause_name_def]              
+    METIS_TAC[bool_casting_length, clause_name_def],
+
+    OPEN_EXP_TYP_TAC ``e_cast cast_bool (e_v (v_bit bitv))`` >>
+    gvs[Once e_typ_cases] >>
+    gvs[Once e_typ_cases] >>
+    gvs[Once v_typ_cases] >>
+    gvs[Once v_typ_cases] >>
+    METIS_TAC[bool_casting_length, clause_name_def],
+
+    OPEN_EXP_TYP_TAC ``e_cast cast_bool (e_v (v_bool b'))`` >>
+    gvs[Once e_typ_cases] >>
+    gvs[Once e_typ_cases] >>
+    gvs[Once v_typ_cases] >>
+    gvs[Once v_typ_cases] >>
+    METIS_TAC[bool_casting_length, clause_name_def]
     ]
     ,
 

hol/p4_exec_semScript.sml

@@ -64,15 +64,19 @@ Definition e_exec_unop_def:
 End
 
 Definition cast_exec_def:
- (cast_exec cast (v_bit bitv) = SOME (v_bit $ bitv_cast cast bitv))
+ (cast_exec (cast_unsigned n) (v_bit bitv) = SOME (v_bit $ bitv_cast n bitv))
  /\
- (cast_exec cast (v_bool b) = SOME (v_bit $ bool_cast cast b))
+ (cast_exec (cast_unsigned n) (v_bool b) = SOME (v_bit $ bool_cast n b))
  /\
- (cast_exec cast v = NONE)
+ (cast_exec (cast_bool) (v_bit bitv) = SOME (v_bool $ to_bool_cast bitv))
+ /\
+ (cast_exec _ _ = NONE)
 End
 
 Definition e_exec_cast_def:
- (e_exec_cast (cast_unsigned n) (e_v v) = cast_exec n v)
+ (e_exec_cast (cast_unsigned n) (e_v v) = cast_exec (cast_unsigned n) v)
+  /\
+ (e_exec_cast (cast_bool) (e_v v) = cast_exec (cast_bool) v)
   /\
  (e_exec_cast _ _ = NONE)
 End

hol/p4_exec_sem_e_soundnessScript.sml

@@ -578,6 +578,9 @@ Cases_on `is_v e` >| [
   fs [clause_name_def],
 
   irule ((valOf o find_clause_e_red) "e_cast_bitv") >>
+  fs [clause_name_def],
+
+  irule ((valOf o find_clause_e_red) "e_cast_to_bool") >>
   fs [clause_name_def]
  ],
 

hol/p4_from_json/excluded.sml

@@ -74,10 +74,11 @@ val exclude_descs =
    ["decl-soundness",
     "enum-bmv2"]),
 (*
-    To-bool cast (manually spotted)
+    More expressive STF specifications
 *)
-  ("supporting to-bool cast in HOL4P4",
-   ["issue1814-1-bmv2"]),
+  ("more expressive STF specifications",
+   ["issue1814-1-bmv2",
+    "switch_ebpf"]),
 (*
     To-struct cast (manually spotted)
 *)
@@ -94,20 +95,10 @@ val exclude_descs =
   ("adding counter extern to V1Model model",
    ["issue1566-bmv2"]),
 (*
-    Return struct of table application
-*)
-  ("adding support for desugaring more table application expressions to import tool",
-   ["hit_ebpf",
-    "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