Skip to content

Commit 89a10a2

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
created a lib for the bdd tranlation to fit in the pipeline
1 parent c6195a1 commit 89a10a2

File tree

2 files changed

+280
-0
lines changed

2 files changed

+280
-0
lines changed

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sig‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
signature apply_trans_to_IOLib =
2+
sig
3+
include Abbrev
4+
5+
end

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml‎

Lines changed: 275 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,275 @@
1+
structure apply_trans_to_IOLib :> apply_trans_to_IOLib = struct
2+
3+
4+
open HolKernel Parse boolLib bossLib;
5+
open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
6+
7+
open sptrees_bdd_trans_ProgTheory;
8+
open preamble basis ml_translatorLib ;
9+
10+
open miscTheory ml_translatorTheory ListProgTheory ;
11+
open fromSexpTheory;
12+
13+
14+
val _ = translation_extends "sptrees_bdd_trans_Prog";
15+
16+
17+
18+
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
19+
20+
Definition policy_order_test_def:
21+
policy_order_test = (["x";"y";"z"]:string list)
22+
End
23+
24+
val r = translate policy_order_test_def;
25+
26+
Definition policy_content_test_def:
27+
policy_content_test = [
28+
(Var "x", action ("allow",[1]));
29+
(And (Var "y") (Var "z"), action ("allow",[2]));
30+
(True, action ("drop",[]))
31+
]:action_policy_type
32+
End
33+
34+
val r = translate policy_content_test_def;
35+
36+
37+
Definition policy_main_hol4_def:
38+
policy_main_hol4 =
39+
case sp_mk_BDD_policy policy_content_test policy_order_test of
40+
| NONE => NONE
41+
| SOME (r,sp_edges,sp_labels) => SOME (r,
42+
((toSortedAList sp_edges):edges),
43+
((toSortedAList sp_labels): (((string#num list) action_expr) policy, (string#num list) action_expr) labelings) )
44+
End
45+
46+
47+
48+
49+
50+
val r = translate policy_main_hol4_def;
51+
52+
53+
val res = append_prog o process_topdecs $
54+
‘fun main () =
55+
let
56+
val args = CommandLine.arguments()
57+
in
58+
(case policy_main_hol4 of
59+
None => (TextIO.print "No BDD can be created \n")
60+
| Some bdd =>
61+
(
62+
TextIO.print "(" ;
63+
TextIO.print (Int.toString (fst bdd));
64+
(TextIO.print "n , \n");
65+
66+
TextIO.print "(" ;
67+
print_tuple_list (fst (snd (bdd))) ;
68+
TextIO.print "):edges , \n";
69+
70+
TextIO.print "(" ;
71+
print_list_label (snd (snd (bdd))) ;
72+
TextIO.print "): (((string#num list) action_expr) policy, (string#num list) action_expr) labelings";
73+
74+
TextIO.print ")"
75+
)
76+
77+
)
78+
end ;’
79+
;
80+
81+
82+
val prog =
83+
``SNOC
84+
(Dlet unknown_loc (Pcon NONE [])
85+
(App Opapp [Var (Short "main"); Con NONE []]))
86+
^(get_ml_prog_state() |> get_prog)
87+
`` |> EVAL |> concl |> rhs
88+
89+
90+
91+
val _ = astToSexprLib.write_ast_to_file "../bdd_cake_test/test_bdd_policy.sexp" prog;
92+
93+
94+
val status = OS.Process.system "cd ../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S && cc test_bdd_policy.cake.S basis_ffi.c -lm -o test_bdd_policy.cake -lm && cd ../bdd_cake_test/ && time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt"
95+
96+
val _ = if OS.Process.isSuccess status
97+
then print "Ja, policy cakeML compilation completed\n"
98+
else (print "Nej, policy cakeML compilation failed\n";
99+
OS.Process.exit OS.Process.failure)
100+
101+
102+
103+
(*
104+
105+
cp test_bdd_policy.sexp ../bdd_cake_test
106+
107+
CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S
108+
109+
cc test_bdd_policy.cake.S basis_ffi.c -lm -o test_bdd_policy.cake -lm
110+
111+
time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt
112+
113+
114+
*)
115+
116+
117+
118+
119+
120+
121+
122+
123+
val ins = TextIO.openIn "../bdd_cake_test/bdd_policy_cakeml_export.txt";
124+
val content_str = TextIO.inputAll ins;
125+
val _ = TextIO.closeIn ins;
126+
127+
(*open Term;*)
128+
129+
val content_term =
130+
let
131+
(* Clean the string by removing newlines and backslash escapes *)
132+
fun clean s =
133+
let
134+
val chars = String.explode s
135+
fun process [] = []
136+
| process (#"\\" :: #"n" :: rest) = process rest (* remove \n *)
137+
| process (c :: rest) = c :: process rest
138+
in
139+
String.implode (process chars)
140+
end
141+
142+
val cleaned = clean content_str
143+
val parsed = Parse.Term [QUOTE cleaned]
144+
in
145+
parsed
146+
end;
147+
148+
149+
150+
151+
152+
153+
val policy_full_order = “[
154+
("A",["x";"y"]);
155+
("B" ,["z"])
156+
]”;
157+
158+
159+
val test_groupings = rhs(concl(EVAL policy_full_order));
160+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative content_term test_groupings;
161+
162+
163+
164+
165+
(*
166+
val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ["x";"y";"z"] 1”;
167+
*)
168+
169+
170+
Definition table_content_test_def:
171+
table_content_test = (^gen_var_table_auto : action_table_type)
172+
End
173+
174+
val r = translate table_content_test_def;
175+
176+
177+
Definition table_main_hol4_def:
178+
table_main_hol4 =
179+
case sp_mk_BDD_table table_content_test policy_order_test of
180+
| NONE => NONE
181+
| SOME (r,sp_edges,sp_labels) => SOME (r,
182+
((toSortedAList sp_edges):edges),
183+
((toSortedAList sp_labels): (action_table_type, (string#num list) action_expr) labelings) )
184+
End
185+
186+
187+
val r = translate table_main_hol4_def;
188+
189+
190+
val res = append_prog o process_topdecs $
191+
‘fun main () =
192+
let
193+
val args = CommandLine.arguments()
194+
in
195+
(case table_main_hol4 of
196+
None => (TextIO.print "No BDD can be created \n")
197+
| Some bdd =>
198+
(
199+
TextIO.print "(" ;
200+
TextIO.print (Int.toString (fst bdd));
201+
(TextIO.print "n , \n");
202+
203+
TextIO.print "(" ;
204+
print_tuple_list (fst (snd (bdd))) ;
205+
TextIO.print "):edges , \n";
206+
207+
TextIO.print "(" ;
208+
print_list_tables_lbl (snd (snd (bdd))) ;
209+
TextIO.print "): (action_table_type, (string#num list) action_expr) labelings)"
210+
)
211+
212+
)
213+
end ;
214+
’;
215+
216+
217+
val prog =
218+
``SNOC
219+
(Dlet unknown_loc (Pcon NONE [])
220+
(App Opapp [Var (Short "main"); Con NONE []]))
221+
^(get_ml_prog_state() |> get_prog)
222+
`` |> EVAL |> concl |> rhs
223+
224+
225+
226+
val _ = astToSexprLib.write_ast_to_file "../bdd_cake_test/test_bdd_table.sexp" prog;
227+
228+
229+
val status = OS.Process.system "cd ../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_table.sexp > test_bdd_table.cake.S && cc test_bdd_table.cake.S basis_ffi.c -lm -o test_bdd_table.cake -lm && cd ../bdd_cake_test/ && time ./test_bdd_table.cake > bdd_table_cakeml_export.txt"
230+
231+
val _ = if OS.Process.isSuccess status
232+
then print "Ja, table cakeML compilation completed\n"
233+
else (print "Nej, table cakeML compilation failed\n";
234+
OS.Process.exit OS.Process.failure)
235+
236+
237+
238+
(*
239+
reset_translation
240+
val _ = astPP.enable_astPP ();
241+
val _ = (max_print_depth := 200);
242+
*)
243+
244+
245+
246+
val ins = TextIO.openIn "../bdd_cake_test/bdd_cake_cakeml_export.txt";
247+
val content_str = TextIO.inputAll ins;
248+
val _ = TextIO.closeIn ins;
249+
250+
251+
252+
253+
val content_term =
254+
let
255+
(* Clean the string by removing newlines and backslash escapes *)
256+
fun clean s =
257+
let
258+
val chars = String.explode s
259+
fun process [] = []
260+
| process (#"\\" :: #"n" :: rest) = process rest (* remove \n *)
261+
| process (c :: rest) = c :: process rest
262+
in
263+
String.implode (process chars)
264+
end
265+
266+
val cleaned = clean content_str
267+
val parsed = Parse.Term [QUOTE cleaned]
268+
in
269+
parsed
270+
end;
271+
272+
273+
274+
275+
end;

0 commit comments

Comments
 (0)