切分支

trdthg · Aug 13, 2024 · 8f862e7 · 8f862e7
1 parent 49e16eb
commit 8f862e7
Show file tree

Hide file tree

Showing 5 changed files with 4,454 additions and 10 deletions.
diff --git a/sailcov/main.ml b/sailcov/main.ml
@@ -558,6 +558,7 @@ let main () =
                   done
                 )
                 else if loc.badness > 0 then (
+                  (*  *)
                   warn_assert __LOC__ (loc.goodness <= 0);
                   current_badness := !current_badness + loc.badness;
                   for _ = 1 to loc.badness do
@@ -581,6 +582,7 @@ let main () =
                   output_string chan "</span>"
                 );
 
+                (*  *)
                 warn_assert __LOC__ (!current_goodness >= 0);
                 warn_assert __LOC__ (!current_badness >= 0)
               )

diff --git a/src/lib/mappings.ml b/src/lib/mappings.ml
@@ -212,9 +212,10 @@ let name_gen prefix =
        Pat_aux (Pat_when (pat, guard, mk_exp ~loc:l (E_app (mk_id ~loc:l "Some", [exp]))), annot) *)
 
 let some_arm = function
-  | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, mk_exp (E_app (mk_id "Some", [exp]))), annot)
-  | Pat_aux (Pat_when (pat, guard, exp), annot) ->
-      Pat_aux (Pat_when (pat, guard, mk_exp (E_app (mk_id "Some", [exp]))), annot)
+  | Pat_aux (Pat_exp (pat, exp), ((l, _) as annot)) ->
+      Pat_aux (Pat_exp (pat, mk_exp ~loc:l (E_app (mk_id ~loc:l "Some", [exp]))), annot)
+  | Pat_aux (Pat_when (pat, guard, exp), ((l, _) as annot)) ->
+      Pat_aux (Pat_when (pat, guard, mk_exp ~loc:l (E_app (mk_id ~loc:l "Some", [exp]))), annot)
 
 let wildcard_none = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit]))))
 
@@ -277,9 +278,11 @@ open Ast_util
 let rec mappings_match is_mapping subst mappings pexp =
   let handle_mapping (subst_id, P_aux (aux, (l, uannot))) =
     Printf.printf "mappings_match mappings LOC %s\n" (simple_string_of_loc l);
+    Printf.printf "测试入口 %s\n" (simple_string_of_loc l);
+
     match aux with
-    (* 好像是这里 *)
     | P_app (mapping, [subpat]) ->
+        Printf.printf "jin4 lai2 le4 ma %s\n" (simple_string_of_loc l);
         let direction = mapping_direction l uannot in
         let mapping_fun_id = mapping_function mapping direction in
         let mapping_guard_id = mapping_guard mapping direction in

diff --git a/test/sailcov/Makefile b/test/sailcov/Makefile
@@ -1,4 +1,4 @@
-basename="nested_mapping4"
+basename="nested_mapping_demo"
 filename="${basename}.sail"
 sail="/home/trdthg/repo/sail/sail"
 sail_dir="/home/trdthg/repo/sail"

diff --git a/test/sailcov/nested_mapping1.expect b/test/sailcov/nested_mapping1.expect
@@ -4,7 +4,7 @@
 <meta charset="utf-8">
 <title>nested_mapping1</title></head>
 <body>
-<h1>nested_mapping1.sail (4/5) 80%</h1>
+<h1>nested_mapping1.sail (7/12) 58%</h1>
 <code style="display: block">
 default&nbsp;Order&nbsp;dec<br>
 $include&nbsp;&lt;prelude.sail&gt;<br>
@@ -14,12 +14,19 @@ union&nbsp;ast&nbsp;=&nbsp;{<br>
 &nbsp;&nbsp;Z&nbsp;:&nbsp;unit<br>
 }<br>
 <br>
-mapping&nbsp;bool_not_bits2&nbsp;:&nbsp;bool&nbsp;&lt;-&gt;&nbsp;bits(2)&nbsp;=&nbsp;{<br>
-&nbsp;&nbsp;true&nbsp;&nbsp;&nbsp;&lt;-&gt;&nbsp;0b10,<br>
-&nbsp;&nbsp;false&nbsp;&nbsp;&lt;-&gt;&nbsp;0b11<br>
+mapping&nbsp;bool_not_bits&nbsp;:&nbsp;bool&nbsp;&lt;-&gt;&nbsp;bits(1)&nbsp;=&nbsp;{<br>
+&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">true</span>&nbsp;&nbsp;&nbsp;&lt;-&gt;&nbsp;0b0,<br>
+&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">false</span>&nbsp;&nbsp;&lt;-&gt;&nbsp;0b1,<br>
 }<br>
+<br>
+let&nbsp;false_val&nbsp;=&nbsp;false<br>
+let&nbsp;false_2&nbsp;=&nbsp;false&nbsp;==&nbsp;true<br>
+<br>
 mapping&nbsp;encdec&nbsp;&nbsp;:&nbsp;bits(2)&nbsp;&lt;-&gt;&nbsp;&nbsp;ast&nbsp;=&nbsp;{<br>
-&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">0b01</span>&nbsp;if&nbsp;<span style="background-color: hsl(120, 85%, 80%)">true</span>&nbsp;&lt;-&gt;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">Z()</span>,<br>
+&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">0b1&nbsp;@&nbsp;bool_not_bits(s)</span>&nbsp;&lt;-&gt;&nbsp;B(s),<br>
+&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 75%)"><span style="background-color: hsl(120, 85%, 75%)">0b01</span>&nbsp;if&nbsp;<span style="background-color: hsl(120, 85%, 75%)">true</span></span>&nbsp;&lt;-&gt;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">Z()</span>,<br>
+&nbsp;&nbsp;0b00&nbsp;if&nbsp;false_val&nbsp;&lt;-&gt;&nbsp;Z(),<br>
+&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">0b00</span>&nbsp;if&nbsp;<span style="background-color: hsl(120, 85%, 80%)">false_val&nbsp;==&nbsp;true</span>&nbsp;&lt;-&gt;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">Z()</span>,<br>
 &nbsp;&nbsp;0b00&nbsp;&lt;-&gt;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">Z()</span>,<br>
 }<br>
 <br>