Adding the necessary fixes for the specific V1Model externs in the symbexec tests

Author: didriklundberg

hol/p4_v1modelScript.sml

@@ -292,9 +292,8 @@ Definition get_oracle_calls_array_def:
 End
 
 Definition v1model_register_construct_inner_def:
- (v1model_register_construct_inner size width oracle_index random_oracle =
+ v1model_register_construct_inner size width oracle_index random_oracle =
   get_oracle_calls_array width oracle_index random_oracle size
- )
 End
 
 Definition register_construct_def:
@@ -304,7 +303,7 @@ Definition register_construct_def:
    (case lookup_lval scope_list (lval_varname (varn_name "targ1")) of
     | SOME (v_bit (bl', n')) =>
      let size = v2n bl in
-     let width = v2n bl' in
+     let width = n' in
      let ext_obj_map' = AUPDATE ext_obj_map (counter, INR (v1model_v_ext_register (v1model_register_construct_inner size width oracle_index random_oracle))) in
      (case assign scope_list (v_ext_ref counter) (lval_varname (varn_name "this")) of
       | SOME scope_list' =>

hol/symb_exec/p4_symb_execLib.sml

@@ -729,26 +729,6 @@ fun p4_should_branch (fty_map, b_fty_map, pblock_action_names_map) const_actions
 (*
 val apply (tbl_name, e) = apply (“"t2"”, “[e_v (v_bit ([e1; e2; e3; e4; e5; e6; e7; T],8))]”);
 
-basic:
-val apply (tbl_name, e) = apply
-    (“"spd"”,
-     “[e_v
-         (v_bit
-            ([ip128; ip129; ip130; ip131; ip132; ip133; ip134; ip135; ip136;
-              ip137; ip138; ip139; ip140; ip141; ip142; ip143; ip144; ip145;
-              ip146; ip147; ip148; ip149; ip150; ip151; ip152; ip153; ip154;
-              ip155; ip156; ip157; ip158; ip159],32));
-       e_v (v_bit ([ip72; ip73; ip74; ip75; ip76; ip77; ip78; ip79],8))]”);
-
-ARBs:
-val apply (tbl_name, e) = apply
-    (“"forward"”,
-     “[e_v
-       (v_bit
-	  ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
-	    ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
-	    ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],32))]”);
-
 *)
     if (hurdUtils.forall is_e_v) (fst $ dest_list e) andalso
        (* Perform a symbolic branch if the apply expression (list) contains
@@ -805,7 +785,7 @@ basic:
 *)
         val i = #1 $ dest_aenv $ #1 $ dest_astate astate
         (* TODO: Unify with the syntactic function obtaining the state above? *)
-        val (ab_list, pblock_map, _, _, _, _, _, _, _, _, _, _, _) = dest_actx $ rhs $ concl ctx_def
+        val (ab_list, pblock_map, _, _, _, _, _, _, _, _, _, _, _) = dest_actx $ rhs $ snd $ strip_forall $ concl ctx_def
         val (curr_block, _) = dest_arch_block_pbl $ rhs $ concl $ HOL4P4_CONV $ mk_el (i, ab_list)
 
         (* TODO: All of the information extracted from the ctx below could be
@@ -3027,7 +3007,7 @@ fun p4_debug_symb_exec arch_ty ctx_data (fty_map, b_fty_map, pblock_action_names
      (ctx_tm, hd $ Defn.eqns_of $ Defn.mk_defn ctx_name (mk_eq(mk_var(ctx_name, type_of ctx_tm), ctx_tm)))
     end
    | def_thm ctx_def =>
-    (rhs $ concl ctx_def, ctx_def)
+    (snd $ strip_forall $ rhs $ concl ctx_def, ctx_def)
 
   val (path_tree, state_list) = p4_symb_exec 1 true arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond NONE fuel
   val state_list_tms = map (fn (path_id, path_cond, step_thm) => (path_id, path_cond, dest_step_thm step_thm)) state_list

hol/symb_exec/p4_symb_exec_v1modelLib.sml

@@ -38,20 +38,25 @@ fun approx_v1model_register_construct p4_symb_arg_prefix fv_index scope_list asc
   val array_size = fst $ dest_pair $ dest_v_bit $ lookup_var "size" scope_list
   val targ1_width = snd $ dest_pair $ dest_v_bit $ lookup_var "targ1" scope_list
   val oracle_index = #5 $ dest_v1model_ascope ascope
-  val tm1 = mk_v1model_register_construct_inner (array_size, targ1_width, oracle_index, random_oracle_tm)
 
   (* TODO: HOL4P4_CONV? *)
   val array_size_num = rhs $ concl $ EVAL (mk_v2n array_size)
 
+  val tm1 = mk_v1model_register_construct_inner (array_size_num, targ1_width, oracle_index, random_oracle_tm)
+
   (* TODO: Hacky... *)
   val rhs_tm = hd $ fst $ dest_list $ fixedwidth_freevars_fromindex_ty (p4_symb_arg_prefix, fv_index, 1, mk_list_type $ mk_prod (mk_list_type bool, num))
   val goal_tm = mk_disj_list [boolSyntax.mk_exists (rhs_tm, mk_conj (mk_eq (tm1, rhs_tm), (mk_wellformed_register_array (targ1_width, rhs_tm))))]
 
   val approx_thm =
    (* “^goal_tm” *)
-   (* TODO: Fix this *)
    prove(goal_tm,
-    SIMP_TAC std_ss [disj_list_def, v1model_register_construct_inner_def (*, wellformed_register_array_replicate_arb *)]
+(*
+    SIMP_TAC std_ss [disj_list_def, v1model_register_construct_inner_def, get_oracle_calls_array_def] >>
+*)
+   (* TODO: Why doesn't just the above work? Make more efficient solution... *)
+    SIMP_TAC bool_ss [disj_list_def] >>
+    EVAL_TAC
    );
  in
   SOME (approx_thm, [fv_index+1])
@@ -83,8 +88,23 @@ fun approx_v1model_register_read p4_symb_arg_prefix fv_index scope_list ascope =
    rpt (goal_term (fn tm => tmCases_on (fst $ dest_eq $ snd $ strip_exists tm) []) >> FULL_SIMP_TAC list_ss [])
   );
 
+  val oracle_index_int = int_of_term oracle_index
+  val w = (int_of_term entry_width)-1
+
+  (* TODO: Move? *)
+  fun provide_oracle_witnesses oracle_index_int 0 =
+     exists_tac (mk_comb (random_oracle_tm, term_of_int oracle_index_int))
+    | provide_oracle_witnesses oracle_index_int w =
+     let
+      val curr_index = oracle_index_int + w
+     in
+      provide_oracle_witnesses oracle_index_int (w-1) >>
+      exists_tac (mk_comb (random_oracle_tm, term_of_int curr_index))
+     end
+  ;
+
   val approx_thm =
-   (* “^goal_tm” *)
+   (* “^(mk_imp (mk_wellformed_register_array (entry_width, array), goal_tm))” *)
    prove(mk_imp (mk_wellformed_register_array (entry_width, array), goal_tm),
     (* As soon as possible, hide the array, which may be big *)
     markerLib.ABBREV_TAC (mk_eq (mk_var("array", mk_list_type (mk_prod (mk_list_type bool, num))) ,array)) >>
@@ -94,7 +114,10 @@ fun approx_v1model_register_read p4_symb_arg_prefix fv_index scope_list ascope =
     CASE_TAC >- (
      (* TODO: HOL4P4_TAC or other solution? *)
      EVAL_TAC >>
+(*
      ntac (int_of_term entry_width) (exists_tac (mk_arb bool)) >>
+*)
+     provide_oracle_witnesses oracle_index_int w >>
      REWRITE_TAC []
     ) >>
     Cases_on ‘x’ >>

hol/symb_exec/tests/register_readScript.sml

@@ -265,7 +265,7 @@ val symb_exec7_astate_symb =
        ("action_run",v_bit (REPLICATE 32 F,32))],NONE)]],
  arch_frame_list_empty,status_running):v1model_ascope astate``;
 
- val fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_ftymap_entries ^symb_exec7_ftymap”
+val fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_ftymap_entries ^symb_exec7_ftymap”
 val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b_ftymap_entries ^symb_exec7_blftymap”
 
 val symb_exec7_ctx_tm = “(^fty_map', ^b_fty_map', ^symb_exec7_pblock_action_names_map)”
@@ -297,6 +297,12 @@ val fuel = 1;
 val postcond_rewr_thms = []
 val postcond_simpset = pure_ss
 
+(*
+#3 $ el 1 $ snd $ p4_symb_exec 1 debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt 20;
+
+#3 $ el 1 $ snd $ p4_symb_exec 1 debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt 21;
+*)
+
 val time_start = Time.now();
 (*
 val p4_symb_exec_fun = (p4_symb_exec 1)

hol/symb_exec/tests/table_unknownScript.sml

@@ -135,17 +135,17 @@ val symb_exec6_actx = ``([arch_block_inp;
  v1model_input_f
    (v_struct
       [("h",
-        v_header ARB
+        v_header F
           [("row",
             v_struct
-              [("e",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
+              [("e",v_bit ([F; F; F; F; F; F; F; F],8));
                ("t",
                 v_bit
-                  ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
-                    ARB; ARB; ARB; ARB; ARB],16));
-               ("l",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
-               ("r",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
-               ("v",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8))])])],
+                  ([F; F; F; F; F; F; F; F; F; F; F;
+                    F; F; F; F; F],16));
+               ("l",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("r",v_bit ([F; F; F; F; F; F; F; F],8));
+               ("v",v_bit ([F; F; F; F; F; F; F; F],8))])])],
     v_struct []),v1model_output_f,v1model_copyin_pbl,v1model_copyout_pbl,
  v1model_apply_table_f,
  [("header",NONE,
@@ -231,8 +231,8 @@ val symb_exec6_astate_symb = rhs $ concl $ EVAL ``p4_append_input_list [([e1; e2
        e_v (v_bit ([F; F; F; F; F; T; T; F; T],9))])])],0),
  [[(varn_name "gen_apply_result",
     v_struct
-      [("hit",v_bool ARB); ("miss",v_bool ARB);
-       ("action_run",v_bit (REPLICATE 32 ARB,32))],NONE)]],
+      [("hit",v_bool F); ("miss",v_bool T);
+       ("action_run",v_bit (REPLICATE 32 F,32))],NONE)]],
  arch_frame_list_empty,status_running):v1model_ascope astate``;
 
 (* Additional parts of the context relevant only to symbolic execution *)