Skip to content

Commit 8c4f532

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
restructered and prepped for new test case folder
1 parent 7dcac97 commit 8c4f532

17 files changed

+135
-52
lines changed

‎Makefile‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,11 @@ hol/p4_from_json: hol
1212
Holmake -r -I hol/p4_from_json
1313

1414
policy_to_table: hol
15-
cd hol/policy_to_table && Holmake bdd_utils.uo && Holmake fwd_proof.uo
1615
Holmake -r -I hol -I hol/policy_to_table
1716

17+
policy_test_cases: policy_to_table
18+
cd hol/policy_to_table/policy_test_cases && Holmake
19+
1820
validate: hol/p4_from_json
1921
cd hol/p4_from_json && ./validate.sh
2022

@@ -34,5 +36,6 @@ clean:
3436

3537
clean_policy:
3638
cd hol/policy_to_table && Holmake clean
39+
cd hol/policy_to_table/policy_test_cases && Holmake clean
3740

3841
.PHONY: default clean hol

‎hol/policy_to_table/bdd_fwd_pipeline_exampleScript.sml‎

Lines changed: 11 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
open HolKernel boolLib liteLib simpLib Parse bossLib;
1+
open HolKernel boolLib liteLib simpLib Parse bossLib pairLib;
22
open arithmeticTheory stringTheory containerTheory pred_setTheory
33
listTheory finite_mapTheory;
44

@@ -38,7 +38,7 @@ open table_bs_propertiesTheory;
3838

3939

4040

41-
val _ = load "bdd_utils";
41+
open bdd_utilsLib;
4242

4343
val _ = new_theory "bdd_fwd_pipeline_example";
4444

@@ -69,12 +69,12 @@ val test_pd_type = “[("ip", type_record [("priority", type_length 3);
6969
("age", type_length 8);
7070
("type", type_length 4)])]”;
7171

72-
val is_high_priority = “(arithm_le (lv_acc (lv_x "ip") "priority") ^(BDDUtils.make_bv 2 3))”;
73-
val is_medium_priority = “(arithm_ge (lv_acc (lv_x "ip") "priority") ^(BDDUtils.make_bv 4 3))”;
74-
val is_small_packet = “(arithm_le (lv_acc (lv_x "ip") "size") ^(BDDUtils.make_bv 500 16))”;
75-
val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^(BDDUtils.make_bv 200 8))”;
76-
val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 3 4))”;
77-
val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^(BDDUtils.make_bv 8 4))”;
72+
val is_high_priority = “(arithm_le (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 2 3))”;
73+
val is_medium_priority = “(arithm_ge (lv_acc (lv_x "ip") "priority") ^(bdd_utilsLib.make_bv 4 3))”;
74+
val is_small_packet = “(arithm_le (lv_acc (lv_x "ip") "size") ^(bdd_utilsLib.make_bv 500 16))”;
75+
val is_young_packet = “(arithm_ge (lv_acc (lv_x "ip") "age") ^( bdd_utilsLib.make_bv 200 8))”;
76+
val is_control_type = “(arithm_le (lv_acc (lv_x "ip") "type") ^( bdd_utilsLib.make_bv 3 4))”;
77+
val is_data_type = “(arithm_ge (lv_acc (lv_x "ip") "type") ^( bdd_utilsLib.make_bv 8 4))”;
7878

7979
val policy_me = “[("x", ^is_high_priority);
8080
("y", ^is_medium_priority);
@@ -149,7 +149,7 @@ val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_fu
149149

150150
(* automatically generate a var table from the var policy's BDD via sml*)
151151
val test_groupings = rhs(concl(EVAL policy_full_order));
152-
val gen_var_table_auto = BDDUtils.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
152+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
153153

154154

155155
(* now create a BDD for the table*)
@@ -158,7 +158,7 @@ val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table
158158

159159

160160
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
161-
val get_i_policy = BDDUtils.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
161+
val get_i_policy = bdd_utilsLib.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
162162
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
163163
^eval_table_full_opt_auto_rhs”;
164164
*)
@@ -238,13 +238,7 @@ val final_thm = prove(
238238

239239

240240

241-
(*
242-
TODO:
243-
1. sota review: why is this work more complete than anything we have found
244-
2. complexity: stage2 complexity. [stage1 and 3 are linear wrt. size of input probably?]
245-
3. Can we handle practical tables, and deploy them?
246-
4. performance and scalability (WCET) + synthetic examples that reflects the complexity of the three stages of the pipeline
247-
*)
241+
248242

249243

250244

‎hol/policy_to_table/bdd_utilsLib.sig‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
signature bdd_utilsLib =
2+
sig
3+
include Abbrev
4+
5+
val make_bv :int -> int -> term
6+
val pairBDDs : term * term -> term
7+
val bdd_to_tables_iterative : term -> term -> term
8+
9+
10+
end

hol/policy_to_table/bdd_utils.sml renamed to hol/policy_to_table/bdd_utilsLib.sml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
1+
structure bdd_utilsLib :> bdd_utilsLib = struct
2+
13
open HolKernel boolLib bossLib Parse;
24
open listTheory pairTheory optionTheory;
35
open pairSyntax numSyntax listSyntax stringSyntax optionSyntax;
46

5-
structure BDDUtils = struct
67

78
fun make_bv n len = let
89
val n_term = numSyntax.mk_numeral (Arbnum.fromInt n)
@@ -442,7 +443,7 @@ fun bdd_to_tables_iterative bdd_term groupings_term =
442443

443444

444445

445-
end;
446+
end
446447

447448
(*
448449
(* Individual table generation *)

‎hol/policy_to_table/fwd_proofLib.sig‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
signature fwd_proofLib =
2+
sig
3+
include Abbrev
4+
5+
val convert_arith_policy_to_interval_tables : term * term * term * term * term -> thm
6+
7+
end

hol/policy_to_table/fwd_proof.sml renamed to hol/policy_to_table/fwd_proofLib.sml

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
1-
open HolKernel boolLib liteLib simpLib Parse bossLib;
1+
structure fwd_proofLib :> fwd_proofLib = struct
2+
3+
4+
open HolKernel boolLib liteLib simpLib Parse bossLib pairLib;
25
open arithmeticTheory stringTheory containerTheory pred_setTheory
36
listTheory finite_mapTheory;
47

@@ -36,9 +39,7 @@ open table_arith_to_intervalTheory;
3639
open bdd_auxTheory;
3740
open table_bs_propertiesTheory;
3841

39-
40-
41-
val _ = load "bdd_utils";
42+
open bdd_utilsLib;
4243

4344

4445

@@ -53,9 +54,6 @@ val _ = type_abbrev("action_rule_type", “:((string# num list) action_expr) rul
5354
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
5455
*)
5556

56-
57-
58-
structure mk_fwd_proof = struct
5957

6058

6159
fun convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
@@ -94,7 +92,7 @@ structure mk_fwd_proof = struct
9492

9593
(* automatically generate a var table from the var policy's BDD via sml*)
9694
val test_groupings = rhs(concl(EVAL policy_full_order));
97-
val gen_var_table_auto = BDDUtils.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
95+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative eval_policy_full_opt_rhs test_groupings;
9896

9997

10098
(* now create a BDD for the table*)
@@ -103,7 +101,7 @@ structure mk_fwd_proof = struct
103101

104102

105103
(* get I (pairs isomorphic in the graph), and check if isisIsomorph *)
106-
val get_i_policy = BDDUtils.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
104+
val get_i_policy = bdd_utilsLib.pairBDDs (eval_policy_full_opt_rhs, eval_table_full_opt_auto_rhs);
107105
(*val is_tbl_policy1_iso = EVAL “isIsomorph_exec ^get_i_policy ^eval_policy_full_opt_rhs
108106
^eval_table_full_opt_auto_rhs”;
109107
*)

‎hol/policy_to_table/policy_test_cases/.hol/logs/auto_test1Theory‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
<<HOL message: Created theory "auto_test1">>
2+
Exporting theory "auto_test1" ... done.
3+
Theory "auto_test1" took 52.0s to build

‎hol/policy_to_table/policy_test_cases/.hol/logs/auto_test2Theory‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
<<HOL message: Created theory "auto_test2">>
2+
Exporting theory "auto_test2" ... done.
3+
Theory "auto_test2" took 0.91415s to build

‎hol/policy_to_table/policy_test_cases/.hol/logs/auto_test_pipelineTheory‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml
2+
error in quse /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml : Fail "Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml"
3+
error in load fwd_proof : Fail "Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml"
4+
error in quse /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/auto_test_pipelineScript.sml : Fail "Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml"
5+
error in load /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/auto_test_pipelineScript : Fail "Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml"
6+
Uncaught exception at poly/poly-init2.ML:36: Fail "Use: non-existent file /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_test_cases/fwd_proof.sml"

‎hol/policy_to_table/policy_test_cases/.hol/make-deps/auto_test1Script.sml.d‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
auto_test1Script.uo: /home/anoud/HOL/sigobj/HolKernel.uo /home/anoud/HOL/sigobj/Parse.uo /home/anoud/Desktop/HOL4P4/hol/policy_to_table/bdd_utilsLib.uo /home/anoud/HOL/sigobj/boolLib.uo /home/anoud/HOL/sigobj/bossLib.uo /home/anoud/Desktop/HOL4P4/hol/policy_to_table/fwd_proofLib.uo /home/anoud/HOL/sigobj/liteLib.uo /home/anoud/Desktop/HOL4P4/hol/policy_to_table/policy_arith_to_varTheory.uo /home/anoud/HOL/sigobj/simpLib.uo

0 commit comments

Comments
 (0)