Skip to content

Commit

Permalink
Deploying to gh-pages from @ 479cbcb 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@zapashcanon
zapashcanon committed May 21, 2024
1 parent 0112afc commit 759b65c
Show file tree
Hide file tree
Showing 18 changed files with 671 additions and 671 deletions.
70 changes: 35 additions & 35 deletions coverage/src/cmd/cmd_sym.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -691,16 +691,16 @@ <h2>85.29%</h2>
| <span data-count="1285">_</span> -&gt; sym_expr )
in
let assume_i32 (i : Value.int32) : unit Choice.t =
<span data-count="769">l</span>et c = Value.I32.to_bool i in
<span data-count="769">C</span>hoice.add_pc c
<span data-count="762">l</span>et c = Value.I32.to_bool i in
<span data-count="762">C</span>hoice.add_pc c
in
let assume_positive_i32 (i : Value.int32) : unit Choice.t =
<span data-count="6">l</span>et c = Value.I32.ge i Value.I32.zero in
<span data-count="6">C</span>hoice.add_pc c
in
let assert_i32 (i : Value.int32) : unit Choice.t =
<span data-count="9619">l</span>et c = Value.I32.to_bool i in
<span data-count="9619">C</span>hoice.assertion c
<span data-count="9592">l</span>et c = Value.I32.to_bool i in
<span data-count="9594">C</span>hoice.assertion c
in
(* we need to describe their types *)
let functions =
Expand Down Expand Up @@ -738,40 +738,40 @@ <h2>85.29%</h2>
let abort () : unit Choice.t = <span data-count="1">C</span>hoice.add_pc @@ Value.Bool.cons<span data-count="1">t</span> false in

let i32 v : int32 Choice.t =
<span data-count="9876">m</span>atch view v with
| <span data-count="9875">V</span>al (Num (I32 v)) -&gt; Choice.return v
<span data-count="9863">m</span>atch view v with
| <span data-count="9860">V</span>al (Num (I32 v)) -&gt; Choice.return v
| <span data-count="0">_</span> -&gt;
Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v;
<span data-count="0">C</span>hoice.bind (abor<span data-count="0">t</span> ()) (fun () -&gt; <span data-count="0">C</span>hoice.return 666l)
in
let ptr v : int32 Choice.t =
<span data-count="2444">m</span>atch view v with
| <span data-count="2444">P</span>tr (b, _) -&gt; Choice.return b
<span data-count="2437">m</span>atch view v with
| <span data-count="2437">P</span>tr (b, _) -&gt; Choice.return b
| <span data-count="0">_</span> -&gt;
Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
<span data-count="0">C</span>hoice.bind (abor<span data-count="0">t</span> ()) (fun () -&gt; <span data-count="0">C</span>hoice.return 667l)
in
let alloc (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
<span data-count="9887">C</span>hoice.bind (i3<span data-count="9876">2</span> base) (fun base -&gt;
<span data-count="9885">C</span>hoice.with_thread (fun t -&gt;
<span data-count="9884">l</span>et memories = Thread.memories t in
<span data-count="9880">S</span>ymbolic_memory.iter
<span data-count="9883">C</span>hoice.bind (i3<span data-count="9856">2</span> base) (fun base -&gt;
<span data-count="9870">C</span>hoice.with_thread (fun t -&gt;
<span data-count="9869">l</span>et memories = Thread.memories t in
<span data-count="9860">S</span>ymbolic_memory.iter
(fun tbl -&gt;
<span data-count="9882">S</span>ymbolic_memory.ITbl.iter
<span data-count="9866">S</span>ymbolic_memory.ITbl.iter
(fun _ (m : Symbolic_memory.t) -&gt;
<span data-count="9884">S</span>ymbolic_memory.replace_size m base size )
<span data-count="9857">S</span>ymbolic_memory.replace_size m base size )
tbl )
memories;
<span data-count="9893">E</span>xpr.make (Ptr (base, Value.const_i3<span data-count="9895">2</span> 0l)) ) )
<span data-count="9886">E</span>xpr.make (Ptr (base, Value.const_i3<span data-count="9884">2</span> 0l)) ) )
in
let free (p : Value.int32) : unit Choice.t =
<span data-count="2445">C</span>hoice.bind (pt<span data-count="2444">r</span> p) (fun base -&gt;
<span data-count="2446">C</span>hoice.with_thread (fun t -&gt;
<span data-count="2446">l</span>et memories = Thread.memories t in
<span data-count="2446">S</span>ymbolic_memory.iter
<span data-count="2437">C</span>hoice.bind (pt<span data-count="2437">r</span> p) (fun base -&gt;
<span data-count="2437">C</span>hoice.with_thread (fun t -&gt;
<span data-count="2437">l</span>et memories = Thread.memories t in
<span data-count="2437">S</span>ymbolic_memory.iter
(fun tbl -&gt;
<span data-count="2445">S</span>ymbolic_memory.ITbl.iter
(fun _ (m : Symbolic_memory.t) -&gt; <span data-count="2446">S</span>ymbolic_memory.free m base)
<span data-count="2437">S</span>ymbolic_memory.ITbl.iter
(fun _ (m : Symbolic_memory.t) -&gt; <span data-count="2437">S</span>ymbolic_memory.free m base)
tbl )
memories ) )
in
Expand Down Expand Up @@ -901,10 +901,10 @@ <h2>85.29%</h2>
<span data-count="335">r</span>un_binary_modul ~unsafe ~optimize pc m

let get_model ~symbols solver pc =
<span data-count="1500">a</span>ssert <span data-count="1500">(</span>`Sat = Solver.Z3Batch.chec<span data-count="1500">k</span> solver pc);
<span data-count="1459">a</span>ssert <span data-count="1459">(</span>`Sat = Solver.Z3Batch.chec<span data-count="1459">k</span> solver pc);
match Solver.Z3Batch.model ~symbols solver with
| None -&gt; assert false
| <span data-count="1500">S</span>ome model -&gt; model
| <span data-count="1459">S</span>ome model -&gt; model

(* NB: This function propagates potential errors (Result.err) occurring
during evaluation (OS, syntax error, etc.), except for Trap and Assert,
Expand All @@ -931,13 +931,13 @@ <h2>85.29%</h2>
<span data-count="23">F</span>ormat.pp_std "Model:@\n @[&lt;v&gt;%a@]@." (Smtml.Model.pp ~no_values) model
in
let rec print_and_count_failures count_acc results =
<span data-count="1822">m</span>atch results () with
<span data-count="1781">m</span>atch results () with
| <span data-count="322">S</span>eq.Nil -&gt; Ok count_acc
| <span data-count="1500">S</span>eq.Cons ((result, thread), tl) -&gt;
| <span data-count="1459">S</span>eq.Cons ((result, thread), tl) -&gt;
let pc = Thread.pc thread in
<span data-count="1500">l</span>et symbols = thread.symbol_set in
<span data-count="1459">l</span>et symbols = thread.symbol_set in
let model = get_model ~symbols solver pc in
<span data-count="1500">l</span>et* is_err =
<span data-count="1459">l</span>et* is_err =
let open Symbolic_choice.Multicore in
match result with
| <span data-count="23">E</span>Assert assertion -&gt;
Expand All @@ -946,20 +946,20 @@ <h2>85.29%</h2>
| <span data-count="159">E</span>Trap tr -&gt;
print_bug (`ETrap (tr, model));
<span data-count="159">O</span>k true
| <span data-count="1317">E</span>Val (Ok ()) -&gt; Ok false
| <span data-count="1276">E</span>Val (Ok ()) -&gt; Ok false
| <span data-count="1">E</span>Val (Error e) -&gt; Error e
in
<span data-count="1499">l</span>et count_acc = if is_err then <span data-count="182">s</span>uc<span data-count="182">c</span> count_acc else <span data-count="1317">c</span>ount_acc in
<span data-count="1458">l</span>et count_acc = if is_err then <span data-count="182">s</span>uc<span data-count="182">c</span> count_acc else <span data-count="1276">c</span>ount_acc in
let* () =
if not no_values then
<span data-count="1291">l</span>et testcase =
List.sort compare (Smtml.Model.get_binding<span data-count="1291">s</span> model) |&gt; <span data-count="1291">L</span>ist.map snd
<span data-count="1250">l</span>et testcase =
List.sort compare (Smtml.Model.get_binding<span data-count="1250">s</span> model) |&gt; <span data-count="1250">L</span>ist.map snd
in
<span data-count="1291">T</span>estcase.write_testcas<span data-count="1291">e</span> ~dir:workspace ~err:is_err testcase
<span data-count="1250">T</span>estcase.write_testcas<span data-count="1250">e</span> ~dir:workspace ~err:is_err testcase
else <span data-count="208">O</span>k ()
in
<span data-count="1499">i</span>f (not is_err<span data-count="1317">)</span> || no_stop_at_failur<span data-count="169">e</span> then
<span data-count="1486">p</span>rint_and_count_failures count_acc tl
<span data-count="1458">i</span>f (not is_err<span data-count="1276">)</span> || no_stop_at_failur<span data-count="169">e</span> then
<span data-count="1445">p</span>rint_and_count_failures count_acc tl
else <span data-count="13">O</span>k count_acc
in
let results =
Expand All @@ -969,7 +969,7 @@ <h2>85.29%</h2>
(x, List.re<span data-count="85">v</span> @@ Thread.breadcrumb<span data-count="85">s</span> th) )
|&gt; <span data-count="29">L</span>ist.of_seq
|&gt; <span data-count="29">L</span>ist.sort (fun (_, bc1) (_, bc2) -&gt;
<span data-count="103">L</span>ist.compare Stdlib.Int32.compare bc1 bc2 )
<span data-count="101">L</span>ist.compare Stdlib.Int32.compare bc1 bc2 )
|&gt; <span data-count="29">L</span>ist.to_seq |&gt; <span data-count="58">S</span>eq.ma<span data-count="29">p</span> fst
else <span data-count="307">r</span>esults
in
Expand Down
28 changes: 14 additions & 14 deletions coverage/src/cmd/testcase.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,30 +96,30 @@ <h2>100.00%</h2>
open Syntax

let out_testcase ~dst ~err testcase =
<span data-count="1292">l</span>et o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
<span data-count="1292">l</span>et tag ?(atts = <span data-count="23212">[</span>]) name = <span data-count="23297">(</span>("", name), atts) in
let atts = if err then <span data-count="85">S</span>ome [ (("", "coversError"), "true") ] else <span data-count="1207">N</span>one in
let to_string v = <span data-count="22005">F</span>ormat.asprintf "%a" Smtml.Value.pp_num v in
let input v = <span data-count="22005">`</span>El (ta<span data-count="22005">g</span> "input", [ `Data (to_strin<span data-count="22005">g</span> v) ]) in
let testcase = `El (ta<span data-count="1292">g</span> ?atts "testcase", List.ma<span data-count="1292">p</span> input testcase) in
<span data-count="1251">l</span>et o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
<span data-count="1251">l</span>et tag ?(atts = <span data-count="21993">[</span>]) name = <span data-count="22078">(</span>("", name), atts) in
let atts = if err then <span data-count="85">S</span>ome [ (("", "coversError"), "true") ] else <span data-count="1166">N</span>one in
let to_string v = <span data-count="20827">F</span>ormat.asprintf "%a" Smtml.Value.pp_num v in
let input v = <span data-count="20827">`</span>El (ta<span data-count="20827">g</span> "input", [ `Data (to_strin<span data-count="20827">g</span> v) ]) in
let testcase = `El (ta<span data-count="1251">g</span> ?atts "testcase", List.ma<span data-count="1251">p</span> input testcase) in
let dtd =
{|&lt;!DOCTYPE testcase PUBLIC "+//IDN sosy-lab.org//DTD test-format testcase 1.1//EN" "https://sosy-lab.org/test-format/testcase-1.1.dtd"&gt;|}
in
Xmlm.output o (`Dtd (Some dtd));
<span data-count="1292">X</span>mlm.output_tree Fun.id o testcase
<span data-count="1251">X</span>mlm.output_tree Fun.id o testcase

let write_testcase =
let cnt = ref 0 in
fun ~dir ~err testcase -&gt;
<span data-count="1292">i</span>ncr cnt;
<span data-count="1292">l</span>et name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in
<span data-count="1292">l</span>et path = Fpath.append dir name in
<span data-count="1292">l</span>et* res =
Bos.OS.File.with_o<span data-count="1292">c</span> path
(fun chan () -&gt; <span data-count="1292">O</span>k (out_testcas<span data-count="1292">e</span> ~dst:(`Channel chan) ~err testcase))
<span data-count="1251">i</span>ncr cnt;
<span data-count="1251">l</span>et name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in
<span data-count="1251">l</span>et path = Fpath.append dir name in
<span data-count="1251">l</span>et* res =
Bos.OS.File.with_o<span data-count="1251">c</span> path
(fun chan () -&gt; <span data-count="1251">O</span>k (out_testcas<span data-count="1251">e</span> ~dst:(`Channel chan) ~err testcase))
()
in
<span data-count="1292">r</span>es
<span data-count="1251">r</span>es
</code></pre>
</div>
</div>
Expand Down
16 changes: 8 additions & 8 deletions coverage/src/concrete/thread.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,13 +125,13 @@ <h2>100.00%</h2>
; breadcrumbs : int32 list
}

let pc t = <span data-count="1500">t</span>.pc
let pc t = <span data-count="1459">t</span>.pc

let memories t = <span data-count="298690">t</span>.memories
let memories t = <span data-count="296968">t</span>.memories

let tables t = <span data-count="4566">t</span>.tables
let tables t = <span data-count="4502">t</span>.tables

let globals t = <span data-count="23600">t</span>.globals
let globals t = <span data-count="23431">t</span>.globals

let breadcrumbs t = <span data-count="85">t</span>.breadcrumbs

Expand All @@ -146,10 +146,10 @@ <h2>100.00%</h2>
}

let clone { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } =
<span data-count="9351">l</span>et memories = Symbolic_memory.clone memories in
<span data-count="9353">l</span>et tables = Symbolic_table.clone tables in
<span data-count="9356">l</span>et globals = Symbolic_global.clone globals in
<span data-count="9356">{</span> choices; symbol_set; pc; memories; tables; globals; breadcrumbs }
<span data-count="9266">l</span>et memories = Symbolic_memory.clone memories in
<span data-count="9268">l</span>et tables = Symbolic_table.clone tables in
<span data-count="9267">l</span>et globals = Symbolic_global.clone globals in
<span data-count="9268">{</span> choices; symbol_set; pc; memories; tables; globals; breadcrumbs }
</code></pre>
</div>
</div>
Expand Down
4 changes: 2 additions & 2 deletions coverage/src/data_structures/env_id.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,14 +112,14 @@ <h2>77.78%</h2>
<span data-count="2961">l</span>et last = succ last in
<span data-count="2961">(</span>{ c; last }, r)

let get i c = <span data-count="11796079">M</span>ap.find i c.c
let get i c = <span data-count="11795928">M</span>ap.find i c.c

let map f c = <span data-count="0">{</span> c with c = Map.ma<span data-count="0">p</span> f c.c }

module Tbl = Hashtbl.Make (struct
include Int

let hash x = <span data-count="337918">x</span>
let hash x = <span data-count="336095">x</span>
end)
</code></pre>
</div>
Expand Down
4 changes: 2 additions & 2 deletions coverage/src/data_structures/func_id.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,8 +105,8 @@ <h2>100.00%</h2>
<span data-count="6521">(</span>last, { c; last = suc<span data-count="6521">c</span> last })

let get i c =
<span data-count="24095">l</span>et v, _ = IMap.find i c.c in
<span data-count="24073">v</span>
<span data-count="24036">l</span>et v, _ = IMap.find i c.c in
<span data-count="24017">v</span>

let get_typ i c =
<span data-count="3514">l</span>et _, t = IMap.find i c.c in
Expand Down
40 changes: 20 additions & 20 deletions coverage/src/data_structures/stack.ml.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -581,13 +581,13 @@ <h2>82.76%</h2>

let empty = []

let push s v = <span data-count="83174758">v</span> :: s
let push s v = <span data-count="83169382">v</span> :: s

let push_bool s b = <span data-count="16210855">p</span>ush s (I32 (V.Bool.int3<span data-count="16210906">2</span> b))
let push_bool s b = <span data-count="16210500">p</span>ush s (I32 (V.Bool.int3<span data-count="16210566">2</span> b))

let push_const_i32 s i = <span data-count="6012149">p</span>ush s (I32 (V.const_i3<span data-count="6012235">2</span> i))
let push_const_i32 s i = <span data-count="6011126">p</span>ush s (I32 (V.const_i3<span data-count="6011205">2</span> i))

let push_i32 s i = <span data-count="5584032">p</span>ush s (I32 i)
let push_i32 s i = <span data-count="5581979">p</span>ush s (I32 i)

let push_i32_of_int s i = <span data-count="12">p</span>ush_const_i32 s (Int32.of_in<span data-count="12">t</span> i)

Expand All @@ -610,21 +610,21 @@ <h2>82.76%</h2>
let pp fmt (s : t) =
<span data-count="14">F</span>ormat.pp_list ~pp_sep:(fun fmt () -&gt; <span data-count="2">F</span>ormat.pp_string fmt " ; ") V.pp fmt s

let pop = function <span data-count="0">[</span>] -&gt; raise Empty | <span data-count="71433108">h</span>d :: tl -&gt; (hd, tl)
let pop = function <span data-count="0">[</span>] -&gt; raise Empty | <span data-count="71430458">h</span>d :: tl -&gt; (hd, tl)

let drop = function <span data-count="0">[</span>] -&gt; raise Empty | <span data-count="5964">_</span>hd :: tl -&gt; tl
let drop = function <span data-count="0">[</span>] -&gt; raise Empty | <span data-count="5925">_</span>hd :: tl -&gt; tl

let pop_i32 s =
<span data-count="5357964">l</span>et hd, tl = pop s in
<span data-count="5357895">m</span>atch hd with
| <span data-count="5357890">I</span>32 n -&gt; (n, tl)
<span data-count="5355358">l</span>et hd, tl = pop s in
<span data-count="5355246">m</span>atch hd with
| <span data-count="5355280">I</span>32 n -&gt; (n, tl)
| <span data-count="0">_</span> -&gt; Log.err "invalid type (expected i32)"

let pop2_i32 s =
<span data-count="8071611">l</span>et n2, s = pop s in
<span data-count="8071548">l</span>et n1, tl = pop s in
<span data-count="8071604">m</span>atch (n1, n2) with
| <span data-count="8071609">I</span>32 n1, I32 n2 -&gt; ((n1, n2), tl)
<span data-count="8070033">l</span>et n2, s = pop s in
<span data-count="8070428">l</span>et n1, tl = pop s in
<span data-count="8070527">m</span>atch (n1, n2) with
| <span data-count="8070573">I</span>32 n1, I32 n2 -&gt; ((n1, n2), tl)
| <span data-count="0">_</span> -&gt; Log.err "invalid type (expected i32)"

let pop_i64 s =
Expand Down Expand Up @@ -679,19 +679,19 @@ <h2>82.76%</h2>
| <span data-count="0">_</span> -&gt; Log.err "invalid type (expected ref)"

let pop_bool s =
<span data-count="16173547">l</span>et hd, tl = pop s in
<span data-count="16173530">m</span>atch hd with
| <span data-count="16173535">I</span>32 n -&gt; (V.I32.to_boo<span data-count="16173592">l</span> n, tl)
<span data-count="16173308">l</span>et hd, tl = pop s in
<span data-count="16173280">m</span>atch hd with
| <span data-count="16173293">I</span>32 n -&gt; (V.I32.to_boo<span data-count="16173382">l</span> n, tl)
| <span data-count="0">_</span> -&gt; Log.err "invalid type (expected i32 (bool))"

let pop_n s n =
<span data-count="11748117">(</span>List.filter<span data-count="11748112">i</span> (fun i _hd -&gt; <span data-count="11910098">i</span> &lt; n) s, List.filter<span data-count="11748116">i</span> (fun i _hd -&gt; <span data-count="11910076">i</span> &gt;= n) s)
<span data-count="11747935">(</span>List.filter<span data-count="11747942">i</span> (fun i _hd -&gt; <span data-count="11909759">i</span> &lt; n) s, List.filter<span data-count="11747941">i</span> (fun i _hd -&gt; <span data-count="11909712">i</span> &gt;= n) s)

let keep s n = <span data-count="3497449">L</span>ist.filteri (fun i _hd -&gt; <span data-count="527416">i</span> &lt; n) s
let keep s n = <span data-count="3496866">L</span>ist.filteri (fun i _hd -&gt; <span data-count="527264">i</span> &lt; n) s

let rec drop_n s n =
<span data-count="16745660">i</span>f n = 0 then <span data-count="15677263">s</span>
else <span data-count="1068404">m</span>atch s with <span data-count="0">[</span>] -&gt; invalid_arg "drop_n" | <span data-count="1068397">_</span> :: tl -&gt; drop_n tl (n - 1)
<span data-count="16744979">i</span>f n = 0 then <span data-count="15676821">s</span>
else <span data-count="1068169">m</span>atch s with <span data-count="0">[</span>] -&gt; invalid_arg "drop_n" | <span data-count="1068169">_</span> :: tl -&gt; drop_n tl (n - 1)
end
</code></pre>
</div>
Expand Down
Loading

0 comments on commit 759b65c

Please sign in to comment.