Skip to content

Commit 9ef1c20

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
made a script to run bdd binary, and edited test cases accordingly
1 parent f7041a2 commit 9ef1c20

16 files changed

+476
-107
lines changed

‎hol/policy_to_table/bdd_cake_trans/policy_parse_cakeml_ProgScript.sml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,12 @@ fun parse_policy_list s =
168168
let val (entry, s) = parse_policy_entry s
169169
val s = skip_ws s
170170
in case s of
171-
#";" :: rest => parse_entries (entry :: acc) (skip_ws rest)
171+
#";" :: rest =>
172+
let val rest = skip_ws rest in
173+
case rest of
174+
#"]" :: rest => (List.rev (entry :: acc), skip_ws rest)
175+
| _ => parse_entries (entry :: acc) rest
176+
end
172177
| #"]" :: rest => (List.rev (entry :: acc), skip_ws rest)
173178
| _ => (List.rev (entry :: acc), s)
174179
end

‎hol/policy_to_table/bdd_cake_trans/table_parse_cakeml_ProgScript.sml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,12 @@ fun parse_tables_list s =
200200
let val (tbl, s) = parse_table s
201201
val s = skip_ws s
202202
in case s of
203-
#";" :: rest => parse_list (tbl :: acc) (skip_ws rest)
203+
#";" :: rest =>
204+
let val rest = skip_ws rest in
205+
case rest of
206+
#"]" :: rest => (List.rev (tbl :: acc), skip_ws rest)
207+
| _ => parse_list (tbl :: acc) rest
208+
end
204209
| #"]" :: rest => (List.rev (tbl :: acc), skip_ws rest)
205210
| _ => (List.rev (tbl :: acc), s)
206211
end

‎hol/policy_to_table/fwd_proof_cakeLib.sig‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
signature fwd_proof_cakeLib =
2+
sig
3+
include Abbrev
4+
5+
6+
val convert_arith_policy_to_interval_tables_cake : term * term * term * term * term * string -> thm
7+
val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
8+
9+
10+
end

‎hol/policy_to_table/fwd_proof_cakeLib.sml‎

Lines changed: 324 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,324 @@
1+
structure fwd_proof_cakeLib :> fwd_proof_cakeLib = struct
2+
3+
4+
open HolKernel boolLib liteLib simpLib Parse bossLib pairLib;
5+
open arithmeticTheory stringTheory containerTheory pred_setTheory
6+
listTheory finite_mapTheory;
7+
8+
open bitstringTheory;
9+
open wordsTheory;
10+
open optionTheory;
11+
open sumTheory;
12+
open stringTheory;
13+
open ottTheory;
14+
open pairTheory;
15+
open rich_listTheory;
16+
open arithmeticTheory;
17+
open alistTheory;
18+
open numeralTheory;
19+
open alistTheory;
20+
21+
22+
open p4Lib;
23+
open blastLib bitstringLib;
24+
open p4Theory;
25+
open p4_auxTheory;
26+
open p4_coreTheory;
27+
28+
open bdd_genTheory;
29+
open pred_specTheory;
30+
open policy_specTheory;
31+
open tables_specTheory;
32+
open bdd_isomorphTheory;
33+
open bdd_end_to_endTheory;
34+
35+
open policy_arith_to_varTheory;
36+
open table_var_to_arithTheory;
37+
open table_arith_to_intervalTheory;
38+
39+
open bdd_auxTheory;
40+
open table_bs_propertiesTheory;
41+
42+
open bdd_utilsLib;
43+
44+
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
45+
val _ = type_abbrev("action_table_type", “:((string# num list) var_table_list # num)”);
46+
47+
48+
fun time_stage (stage_name, timer_cpu, timer_real) =
49+
let
50+
val cpu_time = Timer.checkCPUTimer timer_cpu
51+
val real_time = Timer.checkRealTimer timer_real
52+
val _ = HOL_MESG (stage_name ^ " completed in: " ^
53+
Time.toString (#usr cpu_time) ^ " user, " ^
54+
Time.toString (#sys cpu_time) ^ " system, " ^
55+
Time.toString real_time ^ " real\n")
56+
in
57+
(cpu_time, real_time)
58+
end
59+
60+
61+
fun write_term_to_file (filename, term_string) =
62+
let
63+
val content = term_to_string term_string
64+
val outstream = TextIO.openOut filename
65+
val _ = TextIO.output(outstream, content)
66+
val _ = TextIO.closeOut outstream
67+
in
68+
()
69+
end;
70+
71+
72+
fun convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order, file_name) =
73+
74+
(* this compiles the input with cakeML It takes a very longer time, so I created a parser in CakeML, This should be in fwd_proof_cakeLib file*)
75+
76+
77+
let
78+
79+
val start_cpu_total = Timer.startCPUTimer ();
80+
val start_real_total = Timer.startRealTimer ();
81+
82+
(***********************)
83+
(* STAGE 1 *)
84+
(***********************)
85+
86+
(*convert arith policy to var policy*)
87+
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
88+
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
89+
90+
91+
(* first establish distinction of domain and range of me*)
92+
val policy_me_fst_distinct = EVAL “ALL_DISTINCT (MAP FST ^policy_me)”;
93+
val policy_me_snd_distinct = EVAL “ALL_DISTINCT (MAP SND ^policy_me)”;
94+
95+
val all_distinct_conj = CONJ policy_me_fst_distinct policy_me_snd_distinct;
96+
97+
98+
(* Theorem of correctness for conversion from arith policy to var policy *)
99+
val arith_policy_var_policy_thm = REWRITE_RULE[all_distinct_conj, arith_policy_eval]
100+
(ISPECL[arith_policy, var_policy, policy_me] policy_airth_to_var_sem_conversion_correct);
101+
102+
val _ = time_stage ("Stage 1", start_cpu_total, start_real_total)
103+
104+
(***********************)
105+
(* STAGE 2 *)
106+
(***********************)
107+
108+
val start_cpu_total_stage2 = Timer.startCPUTimer ();
109+
val start_real_total_stage2 = Timer.startRealTimer ();
110+
111+
112+
(************************************************************)
113+
(* Fetch policy's BDD from the output text file *)
114+
(************************************************************)
115+
(*
116+
val _ = write_term_to_file ("../bdd_cake_test/policy_out_test.txt", var_policy);
117+
val _ = write_term_to_file ("../bdd_cake_test/order_out_test.txt", policy_order);
118+
*)
119+
120+
121+
122+
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_policy_out_test.txt", var_policy);
123+
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_order_out_test.txt", policy_order);
124+
125+
126+
val status_exec_policy = OS.Process.system
127+
("cd ../bdd_cake_test/ && time ./test_bdd_policy.cake " ^
128+
file_name ^ "_policy_out_test.txt " ^
129+
file_name ^ "_order_out_test.txt > " ^
130+
file_name ^ "_bdd_policy_cakeml_export.txt")
131+
132+
133+
val _ = if OS.Process.isSuccess status_exec_policy
134+
then print "Ja, policy BDD compilation completed\n"
135+
else (print "Nej, policy NDD compilation failed\n";
136+
OS.Process.exit OS.Process.failure)
137+
138+
139+
140+
val filename_policy_export = "../bdd_cake_test/" ^ file_name ^ "_bdd_policy_cakeml_export.txt"
141+
val ins_policy = TextIO.openIn filename_policy_export
142+
val policy_content_str = TextIO.inputAll ins_policy;
143+
val _ = TextIO.closeIn ins_policy;
144+
145+
(*open Term;*)
146+
147+
val policy_bdd_content_term =
148+
let
149+
(* Clean the string by removing newlines and backslash escapes *)
150+
fun clean s =
151+
let
152+
val chars = String.explode s
153+
fun process [] = []
154+
| process (#"\\" :: #"n" :: rest) = process rest (* remove \n *)
155+
| process (c :: rest) = c :: process rest
156+
in
157+
String.implode (process chars)
158+
end
159+
160+
val cleaned = clean policy_content_str
161+
val parsed = Parse.Term [QUOTE cleaned]
162+
in
163+
parsed
164+
end;
165+
166+
val _ = print "AA:finished cleaning input \n";
167+
168+
169+
170+
(************************************************************)
171+
(* Generate a table using sml function *)
172+
(************************************************************)
173+
174+
val test_groupings = rhs(concl(EVAL policy_full_order));
175+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative policy_bdd_content_term test_groupings;
176+
177+
val _ = print "AA:finished creating table \n";
178+
179+
(**********************************************************)
180+
(* prepp table: translation to CakeML *)
181+
(**********************************************************)
182+
183+
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_table_out_test.txt", gen_var_table_auto)
184+
185+
val status_exec_table = OS.Process.system
186+
("cd ../bdd_cake_test/ && time ./test_bdd_table.cake " ^
187+
file_name ^ "_table_out_test.txt " ^
188+
file_name ^ "_order_out_test.txt > " ^
189+
file_name ^ "_bdd_table_cakeml_export.txt");
190+
191+
192+
val _ = if OS.Process.isSuccess status_exec_table
193+
then print "Ja, table BDD compilation completed\n"
194+
else (print "Nej, table NDD compilation failed\n";
195+
OS.Process.exit OS.Process.failure)
196+
197+
198+
val filename_policy_export = "../bdd_cake_test/" ^ file_name ^ "_bdd_table_cakeml_export.txt"
199+
val ins_tbl = TextIO.openIn filename_policy_export
200+
val tbl_content_str = TextIO.inputAll ins_tbl;
201+
val _ = TextIO.closeIn ins_tbl;
202+
203+
val _ = print "AA:finished getting sexp table to hol4 \n";
204+
205+
206+
val table_bdd_content_term =
207+
let
208+
(* Clean the string by removing newlines and backslash escapes *)
209+
fun clean s =
210+
let
211+
val chars = String.explode s
212+
fun process [] = []
213+
| process (#"\\" :: #"n" :: rest) = process rest (* remove \n *)
214+
| process (c :: rest) = c :: process rest
215+
in
216+
String.implode (process chars)
217+
end
218+
219+
val cleaned = clean tbl_content_str
220+
val parsed = Parse.Term [QUOTE cleaned]
221+
in
222+
parsed
223+
end;
224+
225+
val _ = print "AA:finished cleaning sexp table in hol4 \n";
226+
227+
228+
229+
val get_i_policy = bdd_utilsLib.pairBDDs (policy_bdd_content_term, table_bdd_content_term);
230+
231+
val start_cpu_total_stage2_proof = Timer.startCPUTimer ();
232+
val start_real_total_stage2_proof = Timer.startRealTimer ();
233+
234+
val eval_policy_full_opt = mk_thm ( [], “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1 = SOME ^policy_bdd_content_term ”);
235+
val eval_table_full_opt_auto = mk_thm ( [], “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1 = SOME ^table_bdd_content_term ”);
236+
237+
238+
val var_eq_thm_extract = REWRITE_CONV [correct_var_policy_var_tables_exec_def, eval_policy_full_opt , eval_table_full_opt_auto] “correct_var_policy_var_tables_exec ^var_policy ^gen_var_table_auto ^policy_order ^get_i_policy”;
239+
val var_eq_thm_extract_red = computeLib.RESTR_EVAL_RULE [“correct_var_policy_var_tables_exec”, “sem_tables”,“sem_policy”, “mv_dom_vars”] var_eq_thm_extract;
240+
val var_policy_var_table_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] var_eq_thm_extract_red;
241+
242+
val _ = time_stage ("Stage 2 proof", start_cpu_total_stage2_proof, start_real_total_stage2_proof)
243+
val _ = time_stage ("Stage 2 total", start_cpu_total_stage2, start_real_total_stage2)
244+
245+
246+
(***********************)
247+
(* STAGE 3 *)
248+
(***********************)
249+
250+
val start_cpu_total_stage3 = Timer.startCPUTimer ();
251+
val start_real_total_stage3 = Timer.startRealTimer ();
252+
253+
(* covert var table to interval table *)
254+
val only_var_table = fst (dest_pair gen_var_table_auto);
255+
val convert_to_interval = EVAL “convert_var_to_sinterval_tables ^only_var_table ^policy_me ^test_pd_type”;
256+
val only_interval_table1 = optionSyntax.dest_some(rhs (concl convert_to_interval));
257+
258+
259+
(* Theorem of correctness for conversion from var table to inteval table *)
260+
val var_table_sinterval_tbl_thm =
261+
REWRITE_RULE [convert_to_interval] (ISPECL[only_var_table, only_interval_table1, “0:num”, policy_me, test_pd_type ] correct_tables_from_var_to_sinterval_thm);
262+
263+
val _ = time_stage ("Stage 3 total", start_cpu_total_stage3, start_real_total_stage3)
264+
265+
266+
(***********************)
267+
(* FINAL PROOF *)
268+
(***********************)
269+
270+
val start_cpu_final = Timer.startCPUTimer ();
271+
val start_real_final = Timer.startRealTimer ();
272+
273+
(* to glue the theorems we need to take care of the conditions/ assumptions *)
274+
275+
(* condition1 *)
276+
val every_lval_in_me_in_type_thm = EVAL “every_lval_in_me_in_type ^test_pd_type ^policy_me”;
277+
val cond1_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct] (ISPECL[policy_me, test_pd_type ] lval_in_me_distinct_imp_cond1);
278+
279+
280+
(* condition2 *)
281+
val in_order_then_in_me_thm = EVAL “in_order_then_in_me ^policy_order ^policy_me”;
282+
val ops_in_me_length_format_thm = EVAL “ops_in_me_length_format ^test_pd_type ^policy_me”;
283+
284+
val cond2_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
285+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
286+
(ISPECL[policy_me, test_pd_type, policy_order ]
287+
wf_format_imp_cond2);
288+
289+
(* condition3 *)
290+
val cond3_thm = REWRITE_RULE [every_lval_in_me_in_type_thm, policy_me_fst_distinct,
291+
in_order_then_in_me_thm, ops_in_me_length_format_thm]
292+
(ISPECL[policy_me, test_pd_type]
293+
wf_format_imp_cond3);
294+
295+
296+
val final_thm = prove(
297+
“! packet_input .
298+
wf_packet ^test_pd_type packet_input ⇒
299+
sem_arith_policy ^arith_policy packet_input =
300+
sem_sinterval_tables (^only_interval_table1,0) packet_input”
301+
,
302+
303+
rpt strip_tac >>
304+
305+
assume_tac arith_policy_var_policy_thm >>
306+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
307+
308+
assume_tac var_policy_var_table_thm >>
309+
first_x_assum (strip_assume_tac o (Q.SPECL [‘(create_mv ^policy_me packet_input)’])) >>
310+
311+
312+
assume_tac var_table_sinterval_tbl_thm >>
313+
first_x_assum (strip_assume_tac o (Q.SPECL [‘packet_input’,‘(create_mv ^policy_me packet_input)’])) >>
314+
315+
fs[cond1_thm, cond2_thm, cond3_thm]
316+
);
317+
318+
val _ = time_stage ("FINAL CORRECTNESS PROOF", start_cpu_final, start_real_final)
319+
320+
in
321+
final_thm
322+
end;
323+
324+
end;

‎hol/policy_to_table/policy_test_cases/internet_firewall_10Script.sml‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -435,17 +435,18 @@ val policy_full_order = ``[
435435
(* Testing scripts *)
436436
(********************)
437437

438-
(* old BDD alists + EVAL *)
438+
(* BDD alists + EVAL *)
439439

440440
(*
441-
val final_thm_res =
442-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order); *)
441+
val final_thm_res_eval =
442+
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
443+
*)
443444

444445

445-
(* new BDD sptrees + EVAL *)
446-
(*
447-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
448-
*)
446+
(* BDD alists + Cakeml w parser, just bin *)
447+
val final_thm_res_cake = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order,
448+
"internet_firewall_10");
449+
449450

450451

451452
val _ = export_theory ();

0 commit comments

Comments
 (0)