Skip to content

Commit

Permalink
comment
Browse files Browse the repository at this point in the history
  • Loading branch information
trdthg committed Aug 5, 2024
1 parent 3ade8d8 commit 45851a0
Show file tree
Hide file tree
Showing 14 changed files with 4,992 additions and 5 deletions.
368 changes: 368 additions & 0 deletions log.test.txt
View file

Large diffs are not rendered by default.

4,313 changes: 4,313 additions & 0 deletions test.log.txt
View file

Large diffs are not rendered by default.

13 changes: 8 additions & 5 deletions test/sailcov/Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,17 @@
basename="nested_mapping"
filename="nested_mapping.sail"
basename="nested_mapping4"
filename="${basename}.sail"
sail="/home/trdthg/repo/sail/sail"
sail_dir="/home/trdthg/repo/sail"
sailcov="/home/trdthg/repo/sail/sailcov/sailcov"

all: clear build_sail all_branch build_model taken cov diff
all: clear build_sail build_sailcov all_branch build_model taken cov diff
build_and_run_c: build_model taken

build_sail:
cd ${sail_dir} && make -f ${sail_dir}/Makefile
cd ${sail_dir} && make

build_sailcov:
cd ${sail_dir}/sailcov && make

all_branch:
${sail} -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage ${basename}.branches ${filename} -o ${basename}
Expand All @@ -26,4 +29,4 @@ diff:
diff ${basename}.html ${basename}.expect

clear:
rm -f ${basename}.taken ${basename}.bin ${basename}.branches
rm -f ${basename}.taken ${basename}.bin ${basename}.branches ${basename}.html ${basename}.c
33 changes: 33 additions & 0 deletions test/sailcov/nested_mapping.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>nested_mapping</title></head>
<body>
<h1>nested_mapping.sail (2/6) 33%</h1>
<code style="display: block">
default&nbsp;Order&nbsp;dec<br>
$include&nbsp;&lt;prelude.sail&gt;<br>
<br>
union&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;B&nbsp;:&nbsp;(bool),<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;<span style="background-color: hsl(0, 85%, 80%)">true</span>&nbsp;&nbsp;&nbsp;&lt;-&gt;&nbsp;0b10,<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">false</span>&nbsp;&nbsp;&lt;-&gt;&nbsp;0b11<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%)">0b00</span>&nbsp;&lt;-&gt;&nbsp;Z(),<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">0b01</span>&nbsp;&lt;-&gt;&nbsp;Z(),<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">bool_not_bits2(s)</span>&nbsp;&lt;-&gt;&nbsp;B(s),<br>
}<br>
<br>
val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;encdec_value&nbsp;=&nbsp;encdec(0b00)<br>
}</span><br>
</code>
</body>
</html>
32 changes: 32 additions & 0 deletions test/sailcov/nested_mapping1.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>nested_mapping1</title></head>
<body>
<h1>nested_mapping1.sail (4/5) 80%</h1>
<code style="display: block">
default&nbsp;Order&nbsp;dec<br>
$include&nbsp;&lt;prelude.sail&gt;<br>
<br>
union&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;B&nbsp;:&nbsp;(bool),<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>
}<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;0b00&nbsp;&lt;-&gt;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">Z()</span>,<br>
}<br>
<br>
val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;encdec_value&nbsp;=&nbsp;encdec(0b00)<br>
}</span><br>
</code>
</body>
</html>
28 changes: 28 additions & 0 deletions test/sailcov/nested_mapping1.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

let false_val = false
let false_2 = false == true

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) <-> B(s),
0b01 if true <-> Z(),
0b00 if false_val <-> Z(),
0b00 if false_val == true <-> Z(),
0b00 <-> Z(),
}

val main : unit -> unit
function main() = {
let encdec_value = encdec(0b00)
}
33 changes: 33 additions & 0 deletions test/sailcov/nested_mapping2.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>nested_mapping2</title></head>
<body>
<h1>nested_mapping2.sail (2/5) 40%</h1>
<code style="display: block">
default&nbsp;Order&nbsp;dec<br>
$include&nbsp;&lt;prelude.sail&gt;<br>
<br>
union&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;B&nbsp;:&nbsp;(bool),<br>
&nbsp;&nbsp;Z&nbsp;:&nbsp;unit,<br>
}<br>
<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>
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%)">0b00</span>&nbsp;&lt;-&gt;&nbsp;Z(),<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">0b1&nbsp;@&nbsp;bool_not_bits(s)</span>&nbsp;&lt;-&gt;&nbsp;B(s),<br>
}<br>
<br>
val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;_&nbsp;=&nbsp;encdec(0b00)<br>
}</span><br>
</code>
</body>
</html>
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping2.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit,
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

mapping encdec : bits(2) <-> ast = {
0b00 <-> Z(),
0b1 @ bool_not_bits(s) <-> B(s),
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}
33 changes: 33 additions & 0 deletions test/sailcov/nested_mapping3.expect
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>nested_mapping3</title></head>
<body>
<h1>nested_mapping3.sail (3/5) 60%</h1>
<code style="display: block">
default&nbsp;Order&nbsp;dec<br>
$include&nbsp;&lt;prelude.sail&gt;<br>
<br>
union&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;B&nbsp;:&nbsp;(bool),<br>
&nbsp;&nbsp;Z&nbsp;:&nbsp;unit,<br>
}<br>
<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>
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%)">0b1&nbsp;@&nbsp;bool_not_bits(s)</span>&nbsp;&lt;-&gt;&nbsp;B(s),<br>
&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">0b00</span>&nbsp;&lt;-&gt;&nbsp;Z(),<br>
}<br>
<br>
val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;_&nbsp;=&nbsp;encdec(0b00)<br>
}</span><br>
</code>
</body>
</html>
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping3.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit,
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) <-> B(s),
0b00 <-> Z(),
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping4.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1
}

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) if true <-> B(s),
0b00 <-> Z()
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}
29 changes: 29 additions & 0 deletions test/sailcov/nested_mapping5.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit,
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

let false_val = false
let false_2 = false == true

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) <-> B(s),
0b01 if true <-> Z(),
0b00 if false_val <-> Z(),
0b00 if false_val == true <-> Z(),
0b0 @ bool_not_bits(s) if true <-> B(s),
0b00 <-> Z(),
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}
27 changes: 27 additions & 0 deletions test/sailcov/nested_mapping_demo.full_branches
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
$[complete]
function encdec_forwards arg# = let head_exp# = arg# in
$[complete] $[mapping_match] match $[complete] match head_exp# {
v__0 if and_bool(
let mapping0# : bitvector(1) =
$[overloaded { "name" = "vector_subrange", "is_infix" = false }] subrange_bits(v__0, 0, 0)
in
bool_not_bits_backwards_matches(mapping0#),
$[overloaded { "name" = "==", "is_infix" = true }]
eq_bits(
$[overloaded { "name" = "vector_subrange", "is_infix" = false }]
subrange_bits(v__0, 1, 1), [bitone])
) =>
let mapping0# : bitvector(1) =
$[overloaded { "name" = "vector_subrange", "is_infix" = false }] subrange_bits(v__0, 0, 0)
in
$[complete] match bool_not_bits_backwards(mapping0#) {
s => Some(B(s)),
_ => None()
},
_ => None()
} {
Some(result) => result,
None(_) => $[incomplete] match head_exp# {
b__0 if $[overloaded { "name" = "==", "is_infix" = true }] eq_bits(b__0, [bitzero, bitzero]) => Z()
}
}
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping_demo.sail
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit,
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) <-> B(s),
0b00 <-> Z(),
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}

0 comments on commit 45851a0

Please sign in to comment.