add revisions

lib/eval.ml

@@ -110,7 +110,6 @@ module Int = struct
   let of_bool : Value.t -> int = function
     | True -> 1
     | False -> 0
-    | Int i -> i
     | _ -> assert false
   [@@inline]
 
@@ -230,10 +229,12 @@ module Bool = struct
   let naryop (op : naryop) (vs : Value.t list) : Value.t =
     let b =
       match op with
-      | AndN ->
-        List.fold_left ( && ) true (List.map (of_value 0 (`Naryop op)) vs)
-      | OrN ->
-        List.fold_left ( || ) false (List.map (of_value 0 (`Naryop op)) vs)
+      | Logand ->
+        List.fold_left ( && ) true
+          (List.mapi (fun i -> of_value i (`Naryop op)) vs)
+      | Logor ->
+        List.fold_left ( || ) false
+          (List.mapi (fun i -> of_value i (`Naryop op)) vs)
       | _ -> Log.err {|naryop: Unsupported bool operator "%a"|} Ty.pp_naryop op
     in
     to_value b
@@ -381,19 +382,19 @@ module Lst = struct
     | List_set ->
       let lst = of_value 1 op' v1 in
       let i = Int.of_value 2 op' v2 in
-      let rec set i lst v =
+      let rec set i lst v acc =
         match (i, lst) with
-        | 0, _ :: tl -> v :: tl
-        | i, hd :: tl -> hd :: set (i - 1) tl v
+        | 0, _ :: tl -> List.rev_append acc (v :: tl)
+        | i, hd :: tl -> set (i - 1) tl v (hd :: acc)
         | _, [] -> raise IndexOutOfBounds
       in
-      List (set i lst v3)
+      List (set i lst v3 [])
     | _ -> Log.err {|triop: Unsupported list operator "%a"|} Ty.pp_triop op
 
   let naryop (op : naryop) (vs : Value.t list) : Value.t =
     let op' = `Naryop op in
     match op with
-    | Concat -> List (List.concat (List.map (of_value 0 op') vs))
+    | Concat -> List (List.concat_map (of_value 0 op') vs)
     | _ -> Log.err {|naryop: Unsupported list operator "%a"|} Ty.pp_naryop op
 end
 

lib/expr.ml

@@ -219,7 +219,7 @@ module Pp = struct
       fprintf fmt "(%a.%a %a %a)" Ty.pp ty pp_relop op pp e1 pp e2
     | Cvtop (ty, op, e) -> fprintf fmt "(%a.%a %a)" Ty.pp ty pp_cvtop op pp e
     | Naryop (ty, op, es) ->
-      fprintf fmt "(%a.%a %a)" Ty.pp ty pp_naryop op (pp_print_list pp) es
+      fprintf fmt "(%a.%a (%a))" Ty.pp ty pp_naryop op (pp_print_list pp) es
     | Extract (e, h, l) -> fprintf fmt "(extract %a %d %d)" pp e l h
     | Concat (e1, e2) -> fprintf fmt "(++ %a %a)" pp e1 pp e2
     | App _ -> assert false
@@ -259,19 +259,15 @@ let unop' (ty : Ty.t) (op : unop) (hte : t) : t = make (Unop (ty, op, hte))
 [@@inline]
 
 let unop (ty : Ty.t) (op : unop) (hte : t) : t =
-  match view hte with
-  | Val v -> value (Eval.unop ty op v)
-  | Unop (_, op', hte') -> (
-    match (op, op') with
-    | Not, Not | Neg, Neg | Reverse, Reverse -> hte'
-    | _, _ -> unop' ty op hte )
-  | List es -> (
-    match op with
-    | Head when List.length es <> 0 -> List.hd es
-    | Tail when List.length es > 1 -> make (List (List.tl es))
-    | Reverse -> make (List (List.rev es))
-    | Length -> value (Int (List.length es))
-    | _ -> unop' ty op hte )
+  match (op, view hte) with
+  | _, Val v -> value (Eval.unop ty op v)
+  | Not, Unop (_, Not, hte') -> hte'
+  | Neg, Unop (_, Neg, hte') -> hte'
+  | Reverse, Unop (_, Reverse, hte') -> hte'
+  | Head, List (hd :: _) -> hd
+  | Tail, List (_ :: tl) -> make (List tl)
+  | Reverse, List es -> make (List (List.rev es))
+  | Length, List es -> value (Int (List.length es))
   | _ -> unop' ty op hte
 
 let binop' (ty : Ty.t) (op : binop) (hte1 : t) (hte2 : t) : t =
@@ -338,10 +334,8 @@ let rec binop ty (op : binop) (hte1 : t) (hte2 : t) : t =
       let v = value (Eval.binop ty Mul v1 v2) in
       binop' ty Mul v x
     | _, _ -> binop' ty op hte1 hte2 )
-  | List es, Val (Int n) when n >= 0 && n < List.length es -> (
-    match op with
-    | At -> List.nth es n
-    | _ -> binop' ty op hte1 hte2 )
+  | List es, Val (Int n) -> (
+    match op with At -> List.nth es n | _ -> binop' ty op hte1 hte2 )
   (* FIXME: this seems wrong? *)
   (* | Binop (_, And, _, _), Val (Num (I32 1l)) -> hte1 *)
   (* | Val (Num (I32 1l)), Binop (_, And, _, _) -> hte2 *)

lib/ty.ml

@@ -84,7 +84,6 @@ type binop =
   | String_suffix
   | String_contains
   | String_last_index
-  | String_split
 
 type relop =
   | Eq
@@ -134,8 +133,8 @@ type cvtop =
   | String_to_float
 
 type naryop =
-  | AndN
-  | OrN
+  | Logand
+  | Logor
   | Concat
 
 type logic =
@@ -211,7 +210,6 @@ let pp_binop fmt (op : binop) =
   | String_suffix -> pp_string fmt "suffixof"
   | String_contains -> pp_string fmt "contains"
   | String_last_index -> pp_string fmt "last_indexof"
-  | String_split -> pp_string fmt "split"
 
 let pp_triop fmt (op : triop) =
   match op with
@@ -263,8 +261,8 @@ let pp_cvtop fmt (op : cvtop) =
 
 let pp_naryop fmt (op : naryop) =
   match op with
-  | AndN -> pp_string fmt "and"
-  | OrN -> pp_string fmt "or"
+  | Logand -> pp_string fmt "and"
+  | Logor -> pp_string fmt "or"
   | Concat -> pp_string fmt "++"
 
 let pp fmt = function

lib/ty.mli

@@ -80,7 +80,6 @@ type binop =
   | String_suffix (* (str.suffixof String String Bool) *)
   | String_contains (* (str.contains String String Bool) *)
   | String_last_index
-  | String_split
 
 type relop =
   | Eq
@@ -130,8 +129,8 @@ type cvtop =
   | String_to_float
 
 type naryop =
-  | AndN
-  | OrN
+  | Logand
+  | Logor
   | Concat
 
 type logic =

lib/z3_mappings.ml

@@ -197,8 +197,8 @@ module Fresh = struct
 
       let encode_naryop op es =
         match op with
-        | AndN -> Boolean.mk_and ctx es
-        | OrN -> Boolean.mk_or ctx es
+        | Logand -> Boolean.mk_and ctx es
+        | Logor -> Boolean.mk_or ctx es
         | _ -> err {|Bool: Unsupported Z3 naryop operator "%a"|} Ty.pp_naryop op
     end
 

test/unit/test_cvtop.ml

@@ -36,7 +36,7 @@ let () =
   assert (cvtop Ty_str String_to_int (str "42") = int 42);
   assert (cvtop Ty_str String_from_int (int 42) = str "42");
   assert (cvtop Ty_str String_to_float (str "1.") = real 1.)
-  
+
 (* i32 *)
 let () =
   assert (cvtop (Ty_bitv 32) TruncSF32 (f32 8.5) = i32 8l);

test/unit/test_naryop.ml

@@ -7,10 +7,10 @@ open Value
 let () =
   let t = value True in
   let f = value False in
-  assert (naryop Ty_bool AndN [ t; t; t; t ] = t);
-  assert (naryop Ty_bool OrN [ f; f; f; f ] = f);
-  assert (naryop Ty_bool AndN [ t; f; t ] = f);
-  assert (naryop Ty_bool OrN [ f; t; f ] = t)
+  assert (naryop Ty_bool Logand [ t; t; t; t ] = t);
+  assert (naryop Ty_bool Logor [ f; f; f; f ] = f);
+  assert (naryop Ty_bool Logand [ t; f; t ] = f);
+  assert (naryop Ty_bool Logor [ f; t; f ] = t)
 
 (* str *)
 let () =