@@ -18,6 +18,113 @@ open p4_cake_exec_semProgTheory;
1818open p4_cake_transformLib p4_cake_auxLib;
1919open p4_cake_arch_v1modelProgTheory;
2020
21+ (*
22+ open realLib;
23+
24+ realLib.prefer_real;
25+
26+ map (fn (a,b) => (a, (Real.fromInt b) / 3.0))
27+
28+ [
29+ (1, 5696),
30+ (2, 4736),
31+ (3, 4928),
32+ (4, 5056),
33+ (5, 4288),
34+ (6, 4608),
35+ (7, 4480)
36+ ]
37+
38+ *)
39+
40+ (* ********************)
41+
42+ fun get_keys [] = []
43+ | get_keys (h::t) =
44+ let
45+ val matching = fst $ dest_pair h
46+ val (s_list_tm, prio) = dest_pair matching
47+ val s_list = fst $ dest_list $ s_list_tm
48+ in
49+ if length s_list = 1
50+ then
51+ let
52+ val s = el 1 s_list
53+ in
54+ if is_s_sing s
55+ then
56+ let
57+ val (bool_list_tm, width_tm) = dest_pair $ dest_v_bit $ dest_s_sing s
58+ val value = int_of_term $ rhs $ concl $ EVAL “v2n ^bool_list_tm”
59+ val width = int_of_term width_tm
60+ in
61+ ((value, width), int_of_term prio)::(get_keys t)
62+ end
63+ else raise Fail " get_keys only supports s_sing"
64+ end
65+ else raise Fail " get_keys only supports single matching keys (got multiple entries)"
66+ end
67+ ;
68+
69+ (* Populate a table with singleton keys, outside of existing entries.
70+ * Used for creating dummy entries for benchmarking table matching *)
71+ (* TODO: How to best handle priority? Best make new entries the prioritized ones... *)
72+ fun populate_table ' tbl rand_gen n_additional_entries =
73+ let
74+ val (name, entries) = dest_pair tbl
75+ val entries_list_tm = p4_coreLib.dest_tbl_regular entries
76+ val entries_list = fst $ dest_list $ entries_list_tm
77+ val (keys, prios) = unzip $ get_keys entries_list
78+ (* TODO: Hack. Warn if widths disagree. *)
79+ val width = el 1 $ map snd keys
80+
81+ val max_prio = fst $ mlibUseful.max (fn (a,b) => Int.compare (a, b)) prios
82+
83+ fun get_rand_range width rand_gen existing_keys =
84+ let
85+ val range_value1 = Random.range (0 , (funpow width (fn a => a*2 ) 1 )) rand_gen;
86+ val range_value2 = Random.range (0 , (funpow width (fn a => a*2 ) 1 )) rand_gen;
87+ val (lo, hi) =
88+ if range_value1 < range_value2
89+ then (range_value1, range_value2)
90+ else (range_value2, range_value1)
91+ val lo' = rhs $ concl $ EVAL $ “(fixwidth ^(numSyntax.term_of_int width) $ n2v ^(numSyntax.term_of_int lo), ^(numSyntax.term_of_int width))”
92+ val hi' = rhs $ concl $ EVAL $ “(fixwidth ^(numSyntax.term_of_int width) $ n2v ^(numSyntax.term_of_int hi), ^(numSyntax.term_of_int width))”
93+ in
94+ if not $ exists (fn a => a >= lo) existing_keys
95+ then
96+ mk_s_range (lo', hi')
97+ else get_rand_range width rand_gen existing_keys
98+ end
99+ ;
100+
101+ (* TODO: Chance for doubles now very low *)
102+ fun add_entries existing_keys width rand_gen 0 = []
103+ | add_entries existing_keys width rand_gen n_additional_entries =
104+ let
105+ val new_entry = get_rand_range width rand_gen existing_keys
106+ in
107+ new_entry::(add_entries existing_keys width rand_gen (n_additional_entries-1 ))
108+ end
109+ ;
110+
111+ (* TODO: Take action as an argument *)
112+ val action =
113+ “(" NoAction"
114+ [e_v (v_bool T); e_v (v_bool T)])”
115+ val new_entries = add_entries (map fst keys) width rand_gen n_additional_entries
116+ val new_entries' = map (fn a => mk_pair (mk_list ([a], “:s”), term_of_int (max_prio+1 ))) new_entries
117+ val new_entries_tm = mk_list (map (fn a => mk_pair (a, action)) new_entries', “:(s list # num) # string # e list”)
118+
119+ val entries_list_tm' = rhs $ concl $ EVAL “^new_entries_tm ++ ^entries_list_tm”
120+
121+ in
122+ mk_pair (name, p4_coreLib.mk_tbl_regular entries_list_tm')
123+ end
124+ ;
125+
126+ (* ********************)
127+
21128val _ = translation_extends " p4_cake_arch_v1modelProg"
22129
23130val ipv4_match_tbl =
@@ -95,9 +202,9 @@ val smac_tbl =
95202
96203val rand_gen = Random.newgen ();
97204
98- val n_additional_entries = 10 ;
205+ val n_additional_entries = 1000 ;
99206
100- val dmac_tbl' = populate_table dmac_tbl rand_gen n_additional_entries;
207+ val dmac_tbl' = populate_table' dmac_tbl rand_gen n_additional_entries;
101208
102209val vss_v1model_actx = “([arch_block_inp;
103210 arch_block_pbl " TopParser"
0 commit comments