Remove uncessary stuff and fix rebase

formalsec · Jun 21, 2024 · b1c2116 · b1c2116
1 parent 58c4339
commit b1c2116
Show file tree

Hide file tree

Showing 9 changed files with 46 additions and 80 deletions.
diff --git a/lib/colibri2_mappings.default.ml b/lib/colibri2_mappings.default.ml
@@ -184,7 +184,7 @@ module Fresh = struct
       | Ty_bitv 64 -> DTy.bitv 64
       | Ty_fp 32 -> float32_ty
       | Ty_fp 64 -> float64_ty
-      | Ty_fp _ | Ty_bitv _ | Ty_list | Ty_array | Ty_tuple -> assert false
+      | Ty_fp _ | Ty_bitv _ | Ty_list | Ty_app -> assert false
 
     let tty_to_etype (ty : DTerm.ty) : Ty.t =
       match ty with
@@ -412,7 +412,6 @@ module Fresh = struct
         let op' =
           match op with
           | At -> assert false
-          | Concat -> assert false
           | String_prefix -> assert false
           | String_suffix -> assert false
           | String_contains -> assert false
@@ -657,7 +656,9 @@ module Fresh = struct
       | Ty.Ty_str -> Str.encode_unop
       | Ty.Ty_bitv _ -> Bv.encode_unop
       | Ty.Ty_fp _ -> Fp.encode_unop
-      | Ty.Ty_list | Ty_array | Ty_tuple -> assert false
+      | (Ty.Ty_list | Ty_app) as op ->
+        err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp
+          op
 
     let encode_binop = function
       | Ty.Ty_int -> I.encode_binop
@@ -666,7 +667,9 @@ module Fresh = struct
       | Ty.Ty_str -> Str.encode_binop
       | Ty.Ty_bitv _ -> Bv.encode_binop
       | Ty.Ty_fp _ -> Fp.encode_binop
-      | Ty.Ty_list | Ty_array | Ty_tuple -> assert false
+      | (Ty.Ty_list | Ty_app) as op ->
+        err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp
+          op
 
     let encode_triop = function
       | Ty.Ty_int -> I.encode_triop
@@ -675,7 +678,9 @@ module Fresh = struct
       | Ty.Ty_str -> Str.encode_triop
       | Ty.Ty_bitv _ -> Bv.encode_triop
       | Ty.Ty_fp _ -> Fp.encode_triop
-      | Ty.Ty_list | Ty_array | Ty_tuple -> assert false
+      | (Ty.Ty_list | Ty_app) as op ->
+        err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp
+          op
 
     let encode_relop = function
       | Ty.Ty_int -> I.encode_relop
@@ -684,7 +689,9 @@ module Fresh = struct
       | Ty.Ty_str -> Str.encode_relop
       | Ty.Ty_bitv _ -> Bv.encode_relop
       | Ty.Ty_fp _ -> Fp.encode_relop
-      | Ty.Ty_list | Ty_array | Ty_tuple -> assert false
+      | (Ty.Ty_list | Ty_app) as op ->
+        err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp
+          op
 
     let encode_cvtop = function
       | Ty.Ty_int -> I.encode_cvtop
@@ -693,7 +700,9 @@ module Fresh = struct
       | Ty.Ty_str -> Str.encode_cvtop
       | Ty.Ty_bitv sz -> Bv.encode_cvtop sz
       | Ty.Ty_fp sz -> Fp.encode_cvtop sz
-      | Ty.Ty_list | Ty_array | Ty_tuple -> assert false
+      | (Ty.Ty_list | Ty_app) as op ->
+        err "Colibri2_mappings: Trying to code unsupported op of type %a" Ty.pp
+          op
 
     (*let symbol_to_var v =
       DExpr.Term.Var.mk (Symbol.to_string v) (tty_of_etype (Symbol.type_of v))*)
@@ -719,6 +728,10 @@ module Fresh = struct
           let base' = encode_val (Num (I32 base)) in
           let offset' = aux offset in
           DTerm.Bitv.add base' offset'
+        | Symbol s ->
+          let cst = tcst_of_symbol s in
+          record_sym cst;
+          DTerm.of_cst cst
         | Unop (ty, op, e) ->
           let e' = aux e in
           encode_unop ty op e'
@@ -738,18 +751,15 @@ module Fresh = struct
         | Cvtop (ty, op, e) ->
           let e' = aux e in
           encode_cvtop ty op e'
-        | Symbol s ->
-          let cst = tcst_of_symbol s in
-          record_sym cst;
-          DTerm.of_cst cst
+        | Naryop _ -> err "Colibri2_mappings: Trying to encode naryop"
         | Extract (e, h, l) ->
           let e' = aux e in
           DTerm.Bitv.extract ((h * 8) - 1) (l * 8) e'
         | Concat (e1, e2) ->
           let e1' = aux e1
           and e2' = aux e2 in
           DTerm.Bitv.concat e1' e2'
-        | List _ | Array _ | Tuple _ | App _ -> assert false
+        | List _ | App _ -> assert false
         (* | Quantifier (t, vars, body, patterns) -> (
            let body' = aux body in
            let encode_pattern (p : t list) =
@@ -1024,7 +1034,9 @@ module Fresh = struct
                | 64 ->
                  F64 (Int64.bits_of_float (Farith.F.to_float Farith.Mode.NE a))
                | _ -> assert false ) ) )
-      | Ty_str | Ty_list | Ty_array | Ty_tuple -> assert false
+      | Ty_str | Ty_list | Ty_app ->
+        err "Colibri2_mappings2: Unsuppoted model generation of type %a" Ty.pp
+          ty
 
     (* let value_of_const ((d, _l) : model) (e : Expr.t) : Value.t option =
        let e' = encore_expr_aux e in

diff --git a/lib/cvc5_mappings.default.ml b/lib/cvc5_mappings.default.ml
@@ -174,7 +174,7 @@ module Fresh_cvc5 () = struct
       let one = Term.mk_int tm 1 in
       Term.mk_term tm Kind.String_substr [| t; pos; one |]
 
-    let concat t1 t2 = Term.mk_term tm Kind.String_concat [| t1; t2 |]
+    let concat ts = Term.mk_term tm Kind.String_concat (Array.of_list ts)
 
     let contains t1 ~sub = Term.mk_term tm Kind.String_contains [| t1; sub |]
 

diff --git a/lib/eval.ml b/lib/eval.ml
@@ -972,7 +972,7 @@ let op int real bool str lst i32 i64 f32 f64 ty op =
   | Ty_bitv 64 -> i64 op
   | Ty_fp 32 -> f32 op
   | Ty_fp 64 -> f64 op
-  | Ty_bitv _ | Ty_fp _ | Ty_array | Ty_tuple | Ty_app -> assert false
+  | Ty_bitv _ | Ty_fp _ | Ty_app -> assert false
 [@@inline]
 
 let unop =

diff --git a/lib/expr.ml b/lib/expr.ml
@@ -25,8 +25,6 @@ and expr =
   | Ptr of int32 * t
   | Symbol of Symbol.t
   | List of t list
-  | Array of t array
-  | Tuple of t list
   | App : [> `Op of string ] * t list -> expr
   | Unop of Ty.t * unop * t
   | Binop of Ty.t * binop * t * t
@@ -49,9 +47,6 @@ module Expr = struct
     | Ptr (b1, o1), Ptr (b2, o2) -> b1 = b2 && o1 == o2
     | Symbol s1, Symbol s2 -> Symbol.equal s1 s2
     | List l1, List l2 -> list_eq l1 l2
-    | Array a1, Array a2 ->
-      Array.(length a1 = length a2) && Array.for_all2 ( == ) a1 a2
-    | Tuple l1, Tuple l2 -> list_eq l1 l2
     | App (`Op x1, l1), App (`Op x2, l2) -> String.equal x1 x2 && list_eq l1 l2
     | Unop (t1, op1, e1), Unop (t2, op2, e2) ->
       Ty.equal t1 t2 && op1 = op2 && e1 == e2
@@ -77,8 +72,6 @@ module Expr = struct
     | Ptr (b, o) -> h (b, o.tag)
     | Symbol s -> h s
     | List v -> h v
-    | Array es -> h es
-    | Tuple es -> h es
     | App (x, es) -> h (x, es)
     | Unop (ty, op, e) -> h (ty, op, e.tag)
     | Cvtop (ty, op, e) -> h (ty, op, e.tag)
@@ -114,8 +107,6 @@ let rec ty (hte : t) : Ty.t =
   | Ptr _ -> Ty_bitv 32
   | Symbol x -> Symbol.type_of x
   | List _ -> Ty_list
-  | Array _ -> Ty_array
-  | Tuple _ -> Ty_tuple
   | App _ -> assert false
   | Unop (ty, _, _) -> ty
   | Binop (ty, _, _, _) -> ty
@@ -134,8 +125,7 @@ let rec is_symbolic (v : t) : bool =
   | Val _ -> false
   | Symbol _ -> true
   | Ptr (_, offset) -> is_symbolic offset
-  | List vs | Tuple vs -> List.exists is_symbolic vs
-  | Array vs -> Array.exists is_symbolic vs
+  | List vs -> List.exists is_symbolic vs
   | App (_, vs) -> List.exists is_symbolic vs
   | Unop (_, _, v) -> is_symbolic v
   | Binop (_, _, v1, v2) -> is_symbolic v1 || is_symbolic v2
@@ -154,8 +144,7 @@ let get_symbols (hte : t list) =
     | Val _ -> ()
     | Ptr (_, offset) -> symbols offset
     | Symbol s -> Hashtbl.replace tbl s ()
-    | List es | Tuple es -> List.iter symbols es
-    | Array es -> Array.iter symbols es
+    | List es -> List.iter symbols es
     | App (_, es) -> List.iter symbols es
     | Unop (_, _, e1) -> symbols e1
     | Binop (_, _, e1, e2) ->
@@ -198,21 +187,12 @@ let negate_relop (hte : t) : (t, string) Result.t =
 module Pp = struct
   open Format
 
-  let pp_print_array pp_v fmt v =
-    let is_first = ref true in
-    Array.iter
-      (fun v ->
-        if !is_first then is_first := false else pp_print_string fmt " ";
-        pp_v fmt v )
-      v
-
   let rec pp fmt (hte : t) =
     match view hte with
     | Val v -> Value.pp fmt v
     | Ptr (base, offset) -> fprintf fmt "(Ptr (i32 %ld) %a)" base pp offset
     | Symbol s -> Symbol.pp fmt s
-    | List v | Tuple v -> fprintf fmt "(%a)" (pp_print_list pp) v
-    | Array v -> fprintf fmt "(%a)" (pp_print_array pp) v
+    | List v -> fprintf fmt "(%a)" (pp_print_list pp) v
     | App (`Op x, v) -> fprintf fmt "(%s %a)" x (pp_print_list pp) v
     | Unop (ty, op, e) -> fprintf fmt "(%a.%a %a)" Ty.pp ty pp_unop op pp e
     | Binop (ty, op, e1, e2) ->
@@ -486,8 +466,6 @@ let rec simplify_expr ?(rm_extract = true) (hte : t) : t =
   | Val _ | Symbol _ -> hte
   | Ptr (base, offset) -> make @@ Ptr (base, simplify_expr offset)
   | List es -> make @@ List (List.map simplify_expr es)
-  | Array es -> make @@ Array (Array.map simplify_expr es)
-  | Tuple es -> make @@ Tuple (List.map simplify_expr es)
   | App (x, es) -> make @@ App (x, List.map simplify_expr es)
   | Unop (ty, op, e) ->
     let e = simplify_expr e in

diff --git a/lib/expr.mli b/lib/expr.mli
@@ -24,8 +24,6 @@ and expr =
   | Ptr of int32 * t
   | Symbol of Symbol.t
   | List of t list
-  | Array of t array
-  | Tuple of t list
   | App : [> `Op of string ] * t list -> expr
   | Unop of Ty.t * Ty.unop * t
   | Binop of Ty.t * Ty.binop * t * t

diff --git a/lib/mappings.ml b/lib/mappings.ml
@@ -63,8 +63,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_bitv 64 -> i64
       | Ty_fp 32 -> f32
       | Ty_fp 64 -> f64
-      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let make_symbol (symbol_table : sym_tbl) (s : Symbol.t) : M.term =
       match Hashtbl.find_opt symbol_table s with
@@ -487,8 +486,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.unop
       | Ty.Ty_fp 32 -> Float32_impl.unop
       | Ty.Ty_fp 64 -> Float64_impl.unop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let binop = function
       | Ty.Ty_int -> Int_impl.binop
@@ -500,8 +498,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.binop
       | Ty.Ty_fp 32 -> Float32_impl.binop
       | Ty.Ty_fp 64 -> Float64_impl.binop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let triop = function
       | Ty.Ty_int | Ty.Ty_real -> assert false
@@ -512,8 +509,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.triop
       | Ty.Ty_fp 32 -> Float32_impl.triop
       | Ty.Ty_fp 64 -> Float64_impl.triop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let relop = function
       | Ty.Ty_int -> Int_impl.relop
@@ -525,8 +521,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.relop
       | Ty.Ty_fp 32 -> Float32_impl.relop
       | Ty.Ty_fp 64 -> Float64_impl.relop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let cvtop = function
       | Ty.Ty_int -> Int_impl.cvtop
@@ -538,8 +533,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.cvtop
       | Ty.Ty_fp 32 -> Float32_impl.cvtop
       | Ty.Ty_fp 64 -> Float64_impl.cvtop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let naryop = function
       | Ty.Ty_str -> String_impl.naryop
@@ -582,7 +576,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let e1 = encode_expr symbol_table e1 in
         let e2 = encode_expr symbol_table e2 in
         M.Bitv.concat e1 e2
-      | List _ | Array _ | Tuple _ | App _ -> assert false
+      | List _ |  App _ -> assert false
 
     (* TODO: pp_smt *)
     let pp_smt ?status:_ _ _ = assert false
@@ -611,8 +605,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_fp 64 ->
         let float = M.Interp.to_float v 11 53 in
         Value.Num (F64 (Int64.bits_of_float float))
-      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_array | Ty_tuple | Ty_app ->
-        assert false
+      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app -> assert false
 
     let value ({ model = m; symbol_table } : model) (c : Expr.t) : Value.t =
       value_of_term m (Expr.ty c) (encode_expr symbol_table c)

diff --git a/lib/ty.ml b/lib/ty.ml
@@ -33,8 +33,6 @@ type t =
   | Ty_bitv of int
   | Ty_fp of int
   | Ty_list
-  | Ty_tuple
-  | Ty_array
   | Ty_app
 
 type unop =
@@ -274,8 +272,6 @@ let pp fmt = function
   | Ty_bitv n -> fprintf fmt "i%d" n
   | Ty_fp n -> fprintf fmt "f%d" n
   | Ty_list -> pp_string fmt "list"
-  | Ty_tuple -> pp_string fmt "tuple"
-  | Ty_array -> pp_string fmt "array"
   | Ty_app -> pp_string fmt "app"
 
 let pp_logic fmt : logic -> unit = function
@@ -319,4 +315,4 @@ let size (ty : t) : int =
   match ty with
   | Ty_bitv n | Ty_fp n -> n / 8
   | Ty_int | Ty_bool -> 4
-  | Ty_real | Ty_str | Ty_list | Ty_array | Ty_tuple | Ty_app -> assert false
+  | Ty_real | Ty_str | Ty_list | Ty_app -> assert false
diff --git a/lib/ty.mli b/lib/ty.mli
@@ -29,8 +29,6 @@ type t =
   | Ty_bitv of int
   | Ty_fp of int
   | Ty_list
-  | Ty_tuple
-  | Ty_array
   | Ty_app
 
 type unop =