aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-27 16:45:47 +0100
committerMaxime Dénès2017-11-27 16:45:47 +0100
commitdafdd0fc40a27cd487380072bcb8cb96e1a2b3a1 (patch)
treec9900732a9eccdaf6f6abde3a7072541c9e2c9f4
parent58353f74e986f6b03c5eb232f19f431f43def1c5 (diff)
parent7b3caccd054b6c912d4ded5c93d6b603c94904d2 (diff)
Merge PR #6226: Enhance votour
-rw-r--r--checker/votour.ml48
1 files changed, 32 insertions, 16 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 0998bb94b1..b7c898232b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,6 +10,8 @@ open Values
(** {6 Interactive visit of a vo} *)
+let max_string_length = 1024
+
let rec read_num max =
let quit () =
Printf.printf "\nGoodbye!\n%!";
@@ -81,22 +83,25 @@ struct
let ws = Sys.word_size / 8
- let rec init_size seen = function
- | Int _ | Atm _ | Fun _ -> 0
+ let rec init_size seen k = function
+ | Int _ | Atm _ | Fun _ -> k 0
| Ptr p ->
- if seen.(p) then 0
+ if seen.(p) then k 0
else
let () = seen.(p) <- true in
match (!memory).(p) with
| Struct (tag, os) ->
- let fold accu o = accu + 1 + init_size seen o in
- let size = Array.fold_left fold 1 os in
- let () = (!sizes).(p) <- size in
- size
+ let len = Array.length os in
+ let rec fold i accu k =
+ if i == len then k accu
+ else
+ init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
+ in
+ fold 0 1 (fun size -> let () = (!sizes).(p) <- size in k size)
| String s ->
let size = 2 + (String.length s / ws) in
let () = (!sizes).(p) <- size in
- size
+ k size
let size = function
| Int _ | Atm _ | Fun _ -> 0
@@ -116,7 +121,7 @@ struct
let () = memory := mem in
let () = sizes := Array.make (Array.length mem) (-1) in
let seen = Array.make (Array.length mem) false in
- let _ = init_size seen obj in
+ let () = init_size seen ignore obj in
obj
let oid = function
@@ -155,7 +160,8 @@ let get_string_in_tuple o =
for i = 0 to Array.length o - 1 do
match Repr.repr o.(i) with
| STRING s ->
- raise (TupleString (Printf.sprintf " [..%s..]" s))
+ let len = min max_string_length (String.length s) in
+ raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len)))
| _ -> ()
done;
""
@@ -165,7 +171,8 @@ let get_string_in_tuple o =
let rec get_details v o = match v, Repr.repr o with
| (String | Any), STRING s ->
- Printf.sprintf " [%s]" (String.escaped s)
+ let len = min max_string_length (String.length s) in
+ Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len))
|Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o
|(Sum _|Any), BLOCK (tag, _) ->
Printf.sprintf " [tag=%i]" tag
@@ -192,13 +199,13 @@ let access_children vs os pos =
else raise Exit
let access_list v o pos =
- let rec loop o pos = match Repr.repr o with
- | INT 0 -> []
+ let rec loop o pos accu = match Repr.repr o with
+ | INT 0 -> List.rev accu
| BLOCK (0, [|hd; tl|]) ->
- (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+ loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
| _ -> raise Exit
in
- Array.of_list (loop o pos)
+ Array.of_list (loop o pos [])
let access_block o = match Repr.repr o with
| BLOCK (tag, os) -> (tag, os)
@@ -227,7 +234,16 @@ let rec get_children v o pos = match v with
| BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
| _ -> raise Exit
end
- |String | Int -> [||]
+ | String ->
+ begin match Repr.repr o with
+ | STRING _ -> [||]
+ | _ -> raise Exit
+ end
+ | Int ->
+ begin match Repr.repr o with
+ | INT _ -> [||]
+ | _ -> raise Exit
+ end
|Annot (s,v) -> get_children v o pos
|Any -> raise Exit
|Dyn ->