From e1d568c81e70d99dde9f42493f9f09a5c721b80a Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 20 Jan 2024 17:27:30 +0100 Subject: [PATCH 01/14] Add colibri2 support --- bin/main.ml | 89 +++- dune-project | 1 + encoding.opam | 4 + encoding.opam.template | 3 + lib/colibri2_mappings.ml | 989 ++++++++++++++++++++++++++++++++++++++ lib/colibri2_mappings.mli | 1 + lib/dune | 15 +- lib/mappings_intf.ml | 1 + lib/z3_mappings.ml | 2 + 9 files changed, 1079 insertions(+), 26 deletions(-) create mode 100644 lib/colibri2_mappings.ml create mode 100644 lib/colibri2_mappings.mli diff --git a/bin/main.ml b/bin/main.ml index 06bbd0b2..c189e5dd 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,8 +1,4 @@ open Encoding -open Cmdliner -module Z3_batch = Solver.Batch (Z3_mappings) -module Z3_incremental = Solver.Incremental (Z3_mappings) -module Interpret = Interpret.Make (Z3_batch) let get_contents = function | "-" -> In_channel.input_all In_channel.stdin @@ -14,27 +10,72 @@ let get_contents = function let parse_file file = get_contents file |> Parse.from_string -let main files = - match files with - | [] -> - let ast = parse_file "-" in - ignore @@ Interpret.start ast - | _ -> - ignore - @@ List.fold_left - (fun state file -> - let ast = Parse.from_file ~filename:file in - Some (Interpret.start ?state ast) ) - None files +type prover = + | Z3_prover + | Colibri2_prover -let files = - let doc = "source files" in - Arg.(value & pos_all non_dir_file [] & info [] ~doc) +let prover_conv = + Cmdliner.Arg.conv + ( (fun str -> + try + Ok + ( match str with + | "Z3" | "z3" -> Z3_prover + | "Colibri2" | "colibri2" -> Colibri2_prover + | _ -> + failwith (Fmt.str "Unsupported prover %s, try Z3 or Colibri2" str) + ) + with Failure s -> Error (`Msg s) ) + , fun fmt -> function + | Z3_prover -> Fmt.pf fmt "Z3" + | Colibri2_prover -> Fmt.pf fmt "Colibri2" ) -let cli = - let info = Cmd.info "smtml" ~version:"%%VERSION%%" in - Cmd.v info Term.(const main $ files) +let parse_cmdline = + let aux files prover incremental debug = + let module Mappings = + ( val match prover with + | Z3_prover -> (module Z3_mappings) + | Colibri2_prover -> (module Colibri2_mappings) + : Mappings_intf.S ) + in + Mappings.set_debug debug; + let module Interpret = + ( val if incremental then + (module Interpret.Make (Solver.Incremental (Mappings))) + else (module Interpret.Make (Solver.Batch (Mappings))) + : Interpret_intf.S ) + in + match files with + | [] -> + let ast = parse_file "-" in + ignore @@ Interpret.start ast + | _ -> + ignore + @@ List.fold_left + (fun state file -> + let ast = Parse.from_file ~filename:file in + Some (Interpret.start ?state ast) ) + None files + in + let open Cmdliner in + let files = + Arg.(value & pos_all string [] & info [] ~docv:"files" ~doc:"files to read") + and prover = + Arg.( + value & opt prover_conv Z3_prover + & info [ "p"; "prover" ] ~doc:"SMT solver to use" ) + and incremental = + Arg.( + value & flag + & info [ "incremental" ] ~doc:"Use the SMT solver in the incremental mode" ) + and debug = + Arg.(value & flag & info [ "debug" ] ~doc:"Print debugging messages") + in + Cmd.v + (Cmd.info "smtml" ~version:"%%VERSION%%") + Term.(const aux $ files $ prover $ incremental $ debug) let () = - Printexc.record_backtrace true; - exit @@ Cmd.eval cli + match Cmdliner.Cmd.eval_value parse_cmdline with + | Error (`Parse | `Term | `Exn) -> exit 2 + | Ok (`Ok () | `Version | `Help) -> () diff --git a/dune-project b/dune-project index 95683222..46f1218d 100644 --- a/dune-project +++ b/dune-project @@ -25,6 +25,7 @@ (ocaml (>= "4.14.0")) ocaml_intrinsics (z3 (and (>= "4.12.2") (< "4.13"))) + colibri2 (menhir (and :build diff --git a/encoding.opam b/encoding.opam index f02ad9f0..b0a0d633 100644 --- a/encoding.opam +++ b/encoding.opam @@ -13,6 +13,7 @@ depends: [ "ocaml" {>= "4.14.0"} "ocaml_intrinsics" "z3" {>= "4.12.2" & < "4.13"} + "colibri2" "menhir" {build & >= "20220210"} "cmdliner" {>= "1.2.0"} "zarith" {>= "1.5"} @@ -36,3 +37,6 @@ build: [ ] dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" +pin-depends: [ + [ "colibri2" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] +] \ No newline at end of file diff --git a/encoding.opam.template b/encoding.opam.template index ba82cad3..626fe0c1 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1 +1,4 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" +pin-depends: [ + [ "colibri2" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] +] \ No newline at end of file diff --git a/lib/colibri2_mappings.ml b/lib/colibri2_mappings.ml new file mode 100644 index 00000000..fd995cdd --- /dev/null +++ b/lib/colibri2_mappings.ml @@ -0,0 +1,989 @@ +module Fresh = struct + module DExpr = Colibri2_core.Expr + module DTy = DExpr.Ty + module DTerm = DExpr.Term + module A = Colibri2_stdlib.Std.A + module LRA = Colibri2_theories_LRA + module Scheduler = Colibri2_solver.Scheduler + module Context = Colibri2_stdlib.Context + module Interp = Colibri2_core.Interp + module Uninterp = Colibri2_theories_quantifiers.Uninterp + module Ground = Colibri2_core.Ground + module IArray = Colibri2_popop_lib.IArray + module Egraph = Colibri2_core.Egraph + + module Var = struct + include DTerm.Var + + let is_int _ = false + let print = pp + end + + module Ex = struct + type t = unit + + let print fmt () = Fmt.pf fmt "()" + let empty = () + let union () () = () + end + + module Rat = struct + include A + + let m_one = A.minus_one + let print = A.pp + let is_int = A.is_integer + let is_zero v = A.equal v A.zero + let is_one v = A.equal v A.one + let mult = A.mul + let minus = A.neg + let is_m_one v = A.equal v m_one + let ceiling = ceil + end + + let err = Log.err + + module Make () = struct + exception Error of string + + type expr = DTerm.t + + type model = + Colibri2_core.Egraph.wt * (DTerm.Const.t * Colibri2_core.Value.t) list + + module Sim = OcplibSimplex.Basic.Make (Var) (Rat) (Ex) + + type optimize = Sim.Core.t + type handle = optimize * (Sim.Core.P.t * bool) option + + type solver = + { mutable scheduler : Scheduler.t + ; mutable pushpop : Scheduler.bp list + ; mutable state : + [ `Sat of Colibri2_core.Egraph.wt + | `Unknown of Colibri2_core.Egraph.wt + | `Search + | `Unsat + | `StepLimitReached + ] + ; mutable status_colibri : + [ `No | `Sat | `Unsat | `Unknown | `StepLimitReached ] Context.Ref.t + ; mutable decls : DTerm.Const.S.t + } + + type status = + [ `Sat of Colibri2_core.Egraph.wt + | `Unknown of Colibri2_core.Egraph.wt + | `Search + | `Unsat + | `StepLimitReached + ] + + (* additional builtins *) + + let string_ty_cst : DExpr.Term.ty_const = + DExpr.Id.mk ~builtin:DExpr.Base + (Dolmen_std.Path.global "StringTy") + DExpr.{ arity = 0; alias = No_alias } + + let string_ty = DTy.apply string_ty_cst [] + let float32_ty = DTy.float 8 24 + let float64_ty = DTy.float 11 53 + + let int_to_string : DExpr.term_cst = + DExpr.Id.mk ~name:"IntToString" ~builtin:DExpr.Base + (Dolmen_std.Path.global "IntToString") + (DTy.arrow [ DTy.int ] string_ty) + + let string_to_int : DExpr.term_cst = + DExpr.Id.mk ~name:"StringToInt" ~builtin:DExpr.Base + (Dolmen_std.Path.global "StringToInt") + (DTy.arrow [ string_ty ] DTy.int) + + let real_to_string : DExpr.term_cst = + DExpr.Id.mk ~name:"RealToString" ~builtin:DExpr.Base + (Dolmen_std.Path.global "RealToString") + (DTy.arrow [ DTy.real ] string_ty) + + let string_to_real : DExpr.term_cst = + DExpr.Id.mk ~name:"StringToReal" ~builtin:DExpr.Base + (Dolmen_std.Path.global "StringToReal") + (DTy.arrow [ string_ty ] DTy.real) + + let real_to_uint32 : DExpr.term_cst = + DExpr.Id.mk ~name:"RealToUInt32" ~builtin:DExpr.Base + (Dolmen_std.Path.global "RealToUInt32") + (DTy.arrow [ DTy.real ] DTy.real) + + let trim_string : DExpr.term_cst = + DExpr.Id.mk ~name:"TrimString" ~builtin:DExpr.Base + (Dolmen_std.Path.global "TrimString") + (DTy.arrow [ string_ty ] string_ty) + + let f32_to_string : DExpr.term_cst = + DExpr.Id.mk ~name:"F32ToString" ~builtin:DExpr.Base + (Dolmen_std.Path.global "F32ToString") + (DTy.arrow [ float32_ty ] string_ty) + + let string_to_f32 : DExpr.term_cst = + DExpr.Id.mk ~name:"StringToF32" ~builtin:DExpr.Base + (Dolmen_std.Path.global "StringToF32") + (DTy.arrow [ string_ty ] float32_ty) + + let f64_to_string : DExpr.term_cst = + DExpr.Id.mk ~name:"F64ToString" ~builtin:DExpr.Base + (Dolmen_std.Path.global "F64ToString") + (DTy.arrow [ float64_ty ] string_ty) + + let string_to_f64 : DExpr.term_cst = + DExpr.Id.mk ~name:"StringToF64" ~builtin:DExpr.Base + (Dolmen_std.Path.global "StringToF64") + (DTy.arrow [ string_ty ] float64_ty) + + module SHT = Hashtbl.Make (struct + include Symbol + + let hash _ = assert false + end) + + let tty_of_etype (e : Ty.t) : DTerm.ty = + match e with + | Ty_int -> DTy.int + | Ty_real -> DTy.real + | Ty_bool -> DTy.bool + | Ty_str -> string_ty + | Ty_bitv S8 -> assert false + | Ty_bitv S32 -> DTy.bitv 32 + | Ty_bitv S64 -> DTy.bitv 64 + | Ty_fp S8 -> assert false + | Ty_fp S32 -> float32_ty + | Ty_fp S64 -> float64_ty + + let tty_to_etype (ty : DTerm.ty) : Ty.t = + match ty with + | { ty_descr = TyApp ({ builtin = DExpr.Int; _ }, _); _ } -> Ty_int + | { ty_descr = TyApp ({ builtin = DExpr.Real; _ }, _); _ } -> Ty_real + | { ty_descr = TyApp ({ builtin = DExpr.Prop; _ }, _); _ } -> Ty_bool + | { ty_descr = + TyApp + ( { builtin = DExpr.Base + ; path = Absolute { name = "StringTy"; _ } + ; _ + } + , _ ) + ; _ + } -> + Ty_str + | { ty_descr = TyApp ({ builtin = DExpr.Bitv 32; _ }, _); _ } -> + Ty_bitv S32 + | { ty_descr = TyApp ({ builtin = DExpr.Bitv 64; _ }, _); _ } -> + Ty_bitv S64 + | { ty_descr = TyApp ({ builtin = DExpr.Float (8, 24); _ }, _); _ } -> + Ty_fp S32 + | { ty_descr = TyApp ({ builtin = DExpr.Float (11, 53); _ }, _); _ } -> + Ty_fp S64 + | _ -> assert false + + let sym_cache = SHT.create 17 + + let tcst_of_symbol (s : Symbol.t) = + match SHT.find_opt sym_cache s with + | None -> + let x = Symbol.to_string s + and t = Symbol.type_of s in + let cst = DTerm.Const.mk (Dolmen_std.Path.global x) (tty_of_etype t) in + SHT.add sym_cache s cst; + cst + | Some c -> c + + let tcst_to_symbol (c : DExpr.term_cst) : Symbol.t = + match c with + | { builtin = DExpr.Base + ; path = Local { name } | Absolute { name; _ } + ; id_ty + ; _ + } -> + Symbol.mk_symbol (tty_to_etype id_ty) name + | _ -> assert false + + module I : + Op_intf.S + with type v := int + and type t := expr + and type unop := Ty.unop + and type binop := Ty.binop + and type relop := Ty.relop + and type cvtop := Ty.cvtop + and type triop := Ty.triop = struct + open Ty + + let encode_val i = DTerm.Int.mk (Int.to_string i) + + let encode_unop op e = + let op' = + match op with + | Neg -> DTerm.Int.minus + | _ -> err {|Int: Unsupported Z3 unop operator "%a"|} Ty.pp_unop op + in + op' e + + let encode_binop op e1 e2 = + let op' = + match op with + | Add -> DTerm.Int.add + | Sub -> DTerm.Int.sub + | Mul -> DTerm.Int.mul + | Div -> DTerm.Int.div + | Rem -> DTerm.Int.rem + | Pow -> + fun e1 e2 -> + DTerm.apply_cst + Colibri2_theories_LRA.RealValue.Builtin.colibri_pow_int_int [] + [ e1; e2 ] + | _ -> raise (Error "Unsupported integer operations") + in + op' e1 e2 + + let encode_relop op e1 e2 = + let op' = + match op with + | Eq -> DTerm.eq + | Ne -> DTerm.neq + | Lt -> DTerm.Int.lt + | Gt -> DTerm.Int.gt + | Le -> DTerm.Int.le + | Ge -> DTerm.Int.ge + | _ -> + err {|Arith: Unsupported Z3 relop operator "%a"|} Ty.pp_relop op + in + op' e1 e2 + + let encode_cvtop op e = + let op' = + match op with + | ToString -> fun v -> DTerm.apply_cst int_to_string [] [ v ] + | OfString -> fun v -> DTerm.apply_cst string_to_int [] [ v ] + | _ -> err {|Int: Unsupported Z3 cvtop operator "%a"|} Ty.pp_cvtop op + in + op' e + + let encode_triop op _ _ _ = + err {|Arith: Unsupported Z3 triop operator "%a"|} Ty.pp_triop op + end + + module Real : + Op_intf.S + with type v := float + and type t := expr + and type unop := Ty.unop + and type binop := Ty.binop + and type relop := Ty.relop + and type cvtop := Ty.cvtop + and type triop := Ty.triop = struct + open Ty + + let encode_val f = DTerm.Real.mk (Float.to_string f) + + let encode_unop op e = + let op' = + match op with + | Neg -> DTerm.Real.minus + | Abs -> assert false + | Sqrt -> assert false + | Ceil -> + fun e -> + DTerm.apply_cst + Colibri2_theories_LRA.RealValue.Builtin.colibri_ceil [] [ e ] + | Floor -> DTerm.Real.floor + | Nearest | Is_nan | _ -> + err {|Real: Unsupported Z3 cvtop operator "%a"|} Ty.pp_unop op + in + op' e + + let encode_binop op e1 e2 = + let op' = + match op with + | Add -> DTerm.Real.add + | Sub -> DTerm.Real.sub + | Mul -> DTerm.Real.mul + | Div -> DTerm.Real.div + | Min -> fun e1 e2 -> DTerm.ite (DTerm.Real.le e1 e2) e1 e2 + | Max -> fun e1 e2 -> DTerm.ite (DTerm.Real.le e1 e2) e2 e1 + | _ -> err {|Real: Unsupported Z3 binop operator "%a"|} Ty.pp_binop op + in + op' e1 e2 + + let encode_relop op e1 e2 = + let op' = + match op with + | Eq -> DTerm.eq + | Ne -> DTerm.neq + | Lt -> DTerm.Real.lt + | Gt -> DTerm.Real.gt + | Le -> DTerm.Real.le + | Ge -> DTerm.Real.ge + | _ -> + err {|Arith: Unsupported Z3 relop operator "%a"|} Ty.pp_relop op + in + op' e1 e2 + + let encode_cvtop op e = + let op' = + match op with + | ToString -> fun v -> DTerm.apply_cst real_to_string [] [ v ] + | OfString -> fun v -> DTerm.apply_cst string_to_real [] [ v ] + | ConvertUI32 -> fun t -> DTerm.apply_cst real_to_uint32 [] [ t ] + | Reinterpret_int -> DTerm.Int.to_real + | _ -> err {|Real: Unsupported Z3 cvtop operator "%a"|} Ty.pp_cvtop op + in + op' e + + let encode_triop op _ _ _ = + err {|Arith: Unsupported Z3 triop operator "%a"|} Ty.pp_triop op + end + + module Boolean = struct + open Ty + + let encode_unop op e = + let op' = match op with Not -> DTerm.neg | _ -> assert false in + op' e + + let encode_binop op e1 e2 = + let op' = + match op with + | And -> fun a b -> DTerm._and [ a; b ] + | Or -> fun a b -> DTerm._or [ a; b ] + | Xor -> DTerm.xor + | _ -> assert false + in + op' e1 e2 + + let encode_relop op e1 e2 = + let op' = + match op with Eq -> DTerm.eq | Ne -> DTerm.neq | _ -> assert false + in + op' e1 e2 + + let encode_cvtop _op _e = assert false + + let encode_triop op e1 e2 e3 = + let op' = match op with Ite -> DTerm.ite | _ -> assert false in + op' e1 e2 e3 + end + + module Str = struct + open Ty + + let encode_unop op e = + let op' = + match op with + | Len -> assert false + | Trim -> fun _v -> assert false + | _ -> assert false + in + op' e + + let encode_binop op _e1 _e2 = + let op' = + match op with + | Nth -> assert false + | Concat -> assert false + | _ -> assert false + in + op' + + let encode_relop op = + let op' = + match op with + | Eq -> DTerm.eq + | Ne -> DTerm.neq + | _ -> err {|Str: Unsupported Z3 relop operator "%a"|} Ty.pp_relop op + in + op' + + let encode_triop op _e1 _e2 _e3 = + let op' = + match op with + | Substr -> assert false + | _ -> err {|Str: Unsupported Z3 triop operator "%a"|} Ty.pp_triop op + in + op' + + let encode_cvtop _op _e = assert false + end + + module Bv = struct + open Ty + + let encode_val (type a) (cast : a Ty.cast) (i : a) = + match cast with + | C8 -> + let n = if i >= 0 then i else i land ((1 lsl 8) - 1) in + (* necessary to have the same behaviour as Z3 *) + DTerm.Bitv.mk + (Dolmen_type.Misc.Bitv.parse_decimal ("bv" ^ Int.to_string n) 8) + | C32 -> + let iint = Int32.to_int i in + let n = if iint >= 0 then iint else iint land ((1 lsl 32) - 1) in + (* necessary to have the same behaviour as Z3 *) + DTerm.Bitv.mk + (Dolmen_type.Misc.Bitv.parse_decimal ("bv" ^ Int.to_string n) 32) + | C64 -> + let n = + if Int64.compare i Int64.zero >= 0 then Z.of_int64 i + else Z.logand (Z.of_int64 i) (Z.sub (Z.( lsl ) Z.one 64) Z.one) + in + (* necessary to have the same behaviour as Z3 *) + DTerm.Bitv.mk + (Dolmen_type.Misc.Bitv.parse_decimal ("bv" ^ Z.to_string n) 64) + + let encode_unop op e = + let op' = + match op with + | Not -> DTerm.Bitv.not + | Neg -> DTerm.Bitv.neg + | _ -> err {|Bv: Unsupported Z3 unary operator "%a"|} Ty.pp_unop op + in + op' e + + let encode_binop op e1 e2 = + let op' = + match op with + | Add -> DTerm.Bitv.add + | Sub -> DTerm.Bitv.sub + | Mul -> DTerm.Bitv.mul + | Div -> DTerm.Bitv.sdiv + | DivU -> DTerm.Bitv.udiv + | And -> DTerm.Bitv.and_ + | Xor -> DTerm.Bitv.xor + | Or -> DTerm.Bitv.or_ + | ShrA -> DTerm.Bitv.ashr + | ShrL -> DTerm.Bitv.lshr + | Shl -> DTerm.Bitv.shl + | Rem -> DTerm.Bitv.srem + | RemU -> DTerm.Bitv.urem + | _ -> err {|Bv: Unsupported Z3 binary operator "%a"|} Ty.pp_binop op + in + op' e1 e2 + + let encode_triop op _ = + err {|Bv: Unsupported Z3 triop operator "%a"|} Ty.pp_triop op + + let encode_relop op e1 e2 = + let op' = + match op with + | Eq -> DTerm.eq + | Ne -> DTerm.neq + | Lt -> DTerm.Bitv.slt + | LtU -> DTerm.Bitv.ult + | Le -> DTerm.Bitv.sle + | LeU -> DTerm.Bitv.ule + | Gt -> DTerm.Bitv.sgt + | GtU -> DTerm.Bitv.ugt + | Ge -> DTerm.Bitv.sge + | GeU -> DTerm.Bitv.uge + in + op' e1 e2 + + let encode_cvtop sz op e = + let op' = + match sz with + | Ty.S8 -> assert false + | Ty.S32 -> ( + match op with + | ExtS n -> DTerm.Bitv.sign_extend n + | ExtU n -> DTerm.Bitv.zero_extend n + | WrapI64 -> assert false + | TruncSF32 | TruncSF64 -> + DTerm.Float.to_sbv 32 DTerm.Float.roundTowardZero + | TruncUF32 | TruncUF64 -> + DTerm.Float.to_ubv 32 DTerm.Float.roundTowardZero + | Reinterpret_float -> DTerm.Float.ieee_format_to_fp 8 24 + | ToBool -> encode_relop Ne (encode_val C32 0l) + | OfBool -> + fun e -> DTerm.ite e (encode_val C32 1l) (encode_val C32 0l) + | _ -> assert false ) + | Ty.S64 -> ( + match op with + | ExtS n -> DTerm.Bitv.sign_extend n + | ExtU n -> DTerm.Bitv.zero_extend n + | TruncSF32 | TruncSF64 -> + DTerm.Float.to_sbv 64 DTerm.Float.roundTowardZero + | TruncUF32 | TruncUF64 -> + DTerm.Float.to_ubv 64 DTerm.Float.roundTowardZero + | Reinterpret_float -> DTerm.Float.ieee_format_to_fp 11 51 + | ToBool -> encode_relop Ne (encode_val C64 0L) + | OfBool -> + fun e -> DTerm.ite e (encode_val C64 1L) (encode_val C64 0L) + | _ -> assert false ) + in + op' e + end + + module Fp = struct + open Ty + + let encode_val (type a) (sz : a Ty.cast) (f : a) = + match sz with + | C8 -> err "Unable to create FP numeral using 8 bits" + | C32 -> DTerm.Float.ieee_format_to_fp 8 24 (Bv.encode_val C32 f) + | C64 -> DTerm.Float.ieee_format_to_fp 11 53 (Bv.encode_val C64 f) + + let encode_unop op e = + let op' = + match op with + | Neg -> DTerm.Float.neg + | Abs -> DTerm.Float.abs + | Sqrt -> DTerm.Float.sqrt DTerm.Float.roundNearestTiesToEven + | Is_nan -> DTerm.Float.isNaN + | Ceil -> DTerm.Float.roundToIntegral DTerm.Float.roundTowardPositive + | Floor -> DTerm.Float.roundToIntegral DTerm.Float.roundTowardNegative + | Trunc -> DTerm.Float.roundToIntegral DTerm.Float.roundTowardZero + | Nearest -> + DTerm.Float.roundToIntegral DTerm.Float.roundNearestTiesToEven + | _ -> err {|Fp: Unsupported Z3 unary operator "%a"|} Ty.pp_unop op + in + op' e + + let encode_binop op e1 e2 = + let op' = + match op with + | Add -> DTerm.Float.add DTerm.Float.roundNearestTiesToEven + | Sub -> DTerm.Float.sub DTerm.Float.roundNearestTiesToEven + | Mul -> DTerm.Float.mul DTerm.Float.roundNearestTiesToEven + | Div -> DTerm.Float.div DTerm.Float.roundNearestTiesToEven + | Min -> DTerm.Float.min + | Max -> DTerm.Float.max + | Rem -> DTerm.Float.rem + | _ -> err {|Fp: Unsupported Z3 binop operator "%a"|} Ty.pp_binop op + in + op' e1 e2 + + let encode_triop op _ = + err {|Fp: Unsupported Z3 triop operator "%a"|} Ty.pp_triop op + + let encode_relop op e1 e2 = + let op' = + match op with + | Eq -> DTerm.eq + | Ne -> DTerm.neq + | Lt -> DTerm.Float.lt + | Le -> DTerm.Float.leq + | Gt -> DTerm.Float.gt + | Ge -> DTerm.Float.geq + | _ -> err {|Fp: Unsupported Z3 relop operator "%a"|} Ty.pp_relop op + in + op' e1 e2 + + let encode_cvtop sz op e = + let op' = + match sz with + | Ty.S8 -> assert false + | Ty.S32 -> ( + match op with + | DemoteF64 -> DTerm.Float.ieee_format_to_fp 8 24 + | ConvertSI32 | ConvertSI64 -> + DTerm.Float.sbv_to_fp 8 24 DTerm.Float.roundNearestTiesToEven + | ConvertUI32 | ConvertUI64 -> + DTerm.Float.ubv_to_fp 8 24 DTerm.Float.roundNearestTiesToEven + | Reinterpret_int -> assert false + | ToString -> fun v -> DTerm.apply_cst f32_to_string [] [ v ] + | OfString -> fun v -> DTerm.apply_cst string_to_f32 [] [ v ] + | _ -> assert false ) + | Ty.S64 -> ( + match op with + | DemoteF64 -> DTerm.Float.ieee_format_to_fp 11 51 + | ConvertSI32 | ConvertSI64 -> + DTerm.Float.sbv_to_fp 11 51 DTerm.Float.roundNearestTiesToEven + | ConvertUI32 | ConvertUI64 -> + DTerm.Float.ubv_to_fp 11 51 DTerm.Float.roundNearestTiesToEven + | Reinterpret_int -> assert false + | ToString -> fun v -> DTerm.apply_cst f64_to_string [] [ v ] + | OfString -> fun v -> DTerm.apply_cst string_to_f64 [] [ v ] + | _ -> assert false ) + in + op' e + end + + let encode_val : Value.t -> expr = function + | True -> DTerm.of_cst DTerm.Const._true + | False -> DTerm.of_cst DTerm.Const._false + | Int v -> I.encode_val v + | Real v -> Real.encode_val v + | Str _ -> assert false + | Num (I8 x) -> Bv.encode_val C8 x + | Num (I32 x) -> Bv.encode_val C32 x + | Num (I64 x) -> Bv.encode_val C64 x + | Num (F32 x) -> Fp.encode_val C32 x + | Num (F64 x) -> Fp.encode_val C64 x + + let encode_unop = function + | Ty.Ty_int -> I.encode_unop + | Ty.Ty_real -> Real.encode_unop + | Ty.Ty_bool -> Boolean.encode_unop + | Ty.Ty_str -> Str.encode_unop + | Ty.Ty_bitv _ -> Bv.encode_unop + | Ty.Ty_fp _ -> Fp.encode_unop + + let encode_binop = function + | Ty.Ty_int -> I.encode_binop + | Ty.Ty_real -> Real.encode_binop + | Ty.Ty_bool -> Boolean.encode_binop + | Ty.Ty_str -> Str.encode_binop + | Ty.Ty_bitv _ -> Bv.encode_binop + | Ty.Ty_fp _ -> Fp.encode_binop + + let encode_triop = function + | Ty.Ty_int -> I.encode_triop + | Ty.Ty_real -> Real.encode_triop + | Ty.Ty_bool -> Boolean.encode_triop + | Ty.Ty_str -> Str.encode_triop + | Ty.Ty_bitv _ -> Bv.encode_triop + | Ty.Ty_fp _ -> Fp.encode_triop + + let encode_relop = function + | Ty.Ty_int -> I.encode_relop + | Ty.Ty_real -> Real.encode_relop + | Ty.Ty_bool -> Boolean.encode_relop + | Ty.Ty_str -> Str.encode_relop + | Ty.Ty_bitv _ -> Bv.encode_relop + | Ty.Ty_fp _ -> Fp.encode_relop + + let encode_cvtop = function + | Ty.Ty_int -> I.encode_cvtop + | Ty.Ty_real -> Real.encode_cvtop + | Ty.Ty_bool -> Boolean.encode_cvtop + | Ty.Ty_str -> Str.encode_cvtop + | Ty.Ty_bitv sz -> Bv.encode_cvtop sz + | Ty.Ty_fp sz -> Fp.encode_cvtop sz + + (*let symbol_to_var v = + DExpr.Term.Var.mk (Symbol.to_string v) (tty_of_etype (Symbol.type_of v))*) + + (* let encode_unviversal_quantifier (vars_list : Symbol.t list) (body : expr) + (_patterns : expr list) : expr = + (* TODO: support triggers *) + let vars = List.map symbol_to_var vars_list in + DTerm.all ([], vars) body + + let encore_existential_quantifier (vars_list : Symbol.t list) (body : expr) + (_patterns : expr list) : expr = + (* TODO: support triggers *) + let vars = List.map symbol_to_var vars_list in + DTerm.ex ([], vars) body + *) + let encore_expr_aux ?(record_sym = fun _ -> ()) (e : Expr.t) : expr = + let open Expr in + let rec aux ({ e; ty } : t) = + match e with + | Val v -> encode_val v + | Ptr (base, offset) -> + let base' = encode_val (Num (I32 base)) in + let offset' = aux offset in + DTerm.Bitv.add base' offset' + | Unop (op, e) -> + let e' = aux e in + encode_unop ty op e' + | Binop (op, e1, e2) -> + let e1' = aux e1 in + let e2' = aux e2 in + encode_binop ty op e1' e2' + | Triop (op, e1, e2, e3) -> + let e1' = aux e1 + and e2' = aux e2 + and e3' = aux e3 in + encode_triop ty op e1' e2' e3' + | Relop (op, e1, e2) -> + let e1' = aux e1 + and e2' = aux e2 in + encode_relop ty op e1' e2' + | Cvtop (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 + | 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' + (* | Quantifier (t, vars, body, patterns) -> ( + let body' = aux body in + let encode_pattern (p : t list) = + DTerm.multi_trigger (List.map aux p) + in + let patterns' = List.map encode_pattern patterns in + match t with + | Forall -> encode_unviversal_quantifier vars body' patterns' + | Exists -> encore_existential_quantifier vars body' patterns' ) *) + in + aux e + + let () = + let term_app1 env s f = + Dolmen_loop.Typer.T.builtin_term + (Dolmen_type.Base.term_app1 + (module Dolmen_loop.Typer.T) + env s + (fun a -> DExpr.Term.apply_cst f [ a.DExpr.term_ty ] [ a ]) ) + in + DExpr.add_builtins (fun env s -> + match s with + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToInt" } -> + term_app1 env s string_to_int + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "RealToString" } + -> + term_app1 env s real_to_string + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToReal" } + -> + term_app1 env s string_to_real + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "TrimString" } -> + term_app1 env s trim_string + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F32ToString" } -> + term_app1 env s f32_to_string + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF32" } -> + term_app1 env s string_to_f32 + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "F64ToString" } -> + term_app1 env s f64_to_string + | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "StringToF64" } -> + term_app1 env s string_to_f64 + | _ -> `Not_found ) + + let update_param_value _ _ = () + + (* let add_default_axioms env = + (* string_to_alpha (alpha_to_string x) = x + alpha_to_string (string_to_alpha x) = x *) + let add_string_axiom = + let convert ~subst env = + Colibri2_theories_quantifiers.Subst.convert ~subst_new:subst env + in + let mk_eq env subst t1 t2 = + let n1 = convert ~subst env t1 in + let n2 = convert ~subst env t2 in + Egraph.register env n1; + Egraph.register env n2; + let eq = Colibri2_theories_bool.Equality.equality env [ n1; n2 ] in + Egraph.register env eq; + Colibri2_theories_bool.Boolean.set_true env eq + in + fun env to_string of_string ty -> + let x_str = DTerm.Var.mk "x_str" string_ty in + let xt_str = DTerm.of_var x_str in + let term_str = + DTerm.apply_cst to_string [] + [ DTerm.apply_cst of_string [] [ xt_str ] ] + in + let x = DTerm.Var.mk "x" ty in + let xt = DTerm.of_var x in + let term = + DTerm.apply_cst of_string [] [ DTerm.apply_cst to_string [] [ xt ] ] + in + let pattern_1 = + Colibri2_theories_quantifiers.Pattern.of_term_exn term_str + in + let pattern_2 = + Colibri2_theories_quantifiers.Pattern.of_term_exn term + in + let run_1 env subst = mk_eq env subst xt_str term_str in + let run_2 env subst = mk_eq env subst xt term in + Colibri2_theories_quantifiers.InvertedPath.add_callback env pattern_1 + run_1; + Colibri2_theories_quantifiers.InvertedPath.add_callback env pattern_2 + run_2 + in + add_string_axiom env int_to_string string_to_int DTy.int; + add_string_axiom env real_to_string string_to_real DTy.real; + add_string_axiom env f32_to_string string_to_f32 float32_ty; + add_string_axiom env f64_to_string string_to_f64 float64_ty *) + + let encode_expr e = encore_expr_aux e + let pp_smt ?status:_ _ _ = () + let interrupt () = () + + module Solver = struct + let mk_scheduler () = + let scheduler = Scheduler.new_solver ~learning:false () in + Scheduler.init_theories + ~theories: + ( Colibri2_theories_bool.Ite.th_register :: LRA.LRA.th_register + :: Colibri2_theories_fp.Fp.th_register + :: Colibri2_core.ForSchedulers.default_theories () ) + scheduler; + scheduler + + let make ?logic:_ () = + let scheduler = mk_scheduler () in + let ctx = Scheduler.get_context scheduler in + { scheduler + ; pushpop = [] + ; state = `Search + ; status_colibri = Context.Ref.create ctx `No + ; decls = DTerm.Const.S.empty + } + + let add_simplifier s = s + + let clone { pushpop; state; status_colibri; decls; _ } = + let scheduler = mk_scheduler () in + { scheduler; pushpop; state; status_colibri; decls } + + let push st = st.pushpop <- Scheduler.push st.scheduler :: st.pushpop + + let rec pop st i = + assert (0 <= i); + match (i, st.pushpop) with + | 0, _ -> () + | _, [] -> assert false + | 1, bp :: l -> + st.pushpop <- l; + Scheduler.pop_to st.scheduler bp + | n, _ :: l -> + st.pushpop <- l; + pop st (n - 1) + + let reset s = + let scheduler = mk_scheduler () in + let ctx = Scheduler.get_context scheduler in + s.scheduler <- scheduler; + s.pushpop <- []; + s.state <- `Search; + s.status_colibri <- Context.Ref.create ctx `No; + s.decls <- DTerm.Const.S.empty + + let add s es = + Scheduler.add_assertion s.scheduler (fun d -> + let es' = + List.map + (encore_expr_aux ~record_sym:(fun c -> + s.decls <- DTerm.Const.S.add c s.decls ) ) + es + in + List.iter + (fun e -> + let n = Colibri2_core.Ground.convert d e in + Colibri2_core.Egraph.register d n; + Colibri2_theories_bool.Boolean.set_true d n ) + es' ) + + let check s es = + add s es; + Scheduler.check_sat s.scheduler + + let model s : model option = + match Scheduler.check_sat s.scheduler with + | `Sat d | `Unknown d -> + let l = + DTerm.Const.S.fold_left + (fun acc c -> + let e = DExpr.Term.of_cst c in + let v = Interp.interp d e in + (c, v) :: acc ) + [] s.decls + in + Some (d, l) + | `Unsat -> assert false + | `StepLimitReached -> assert false + | `Search -> assert false + + let pp_statistics _ _ = () + end + + module Optimizer = struct + let make () : optimize = Sim.Core.empty ~is_int:false ~check_invs:false + let push _ = () + let pop _ = () + let add _ _ = assert false + let check _ = assert false + + let model o = + match Sim.Result.get None o with + | Sim.Core.Sat s -> + let _model = (Lazy.force s).Sim.Core.main_vars in + (* let l = List.map (fun (n, av) -> (n, LRA.RealValue.of_value av)) model in + Some l *) + None + | Sim.Core.Unknown | Sim.Core.Unsat _ | Sim.Core.Unbounded _ + | Sim.Core.Max (_, _) -> + None + + let maximize _ _ = assert false + let minimize _ _ = assert false + let pp_statistics _ _ = () + end + + let c2value_to_value (ty : Ty.t) (v : Colibri2_core.Value.t) = + match ty with + | Ty_bool -> ( + match + Colibri2_core.Value.value Colibri2_theories_bool.Boolean.BoolValue.key + v + with + | Some true -> Some Value.True + | Some false -> Some Value.False + | None -> None ) + | Ty_int | Ty_real -> ( + match + Colibri2_core.Value.value Colibri2_theories_LRA.RealValue.key v + with + | Some a when A.is_integer a -> Some (Value.Int (A.to_int a)) + | Some a when A.is_real a -> + Some (Value.Real (Stdlib.Float.of_string (A.to_string a))) + | Some _ | None -> None ) + | Ty_bitv S8 | Ty_bitv S32 | Ty_bitv S64 -> assert false + | Ty_fp S8 | Ty_fp S32 | Ty_fp S64 -> assert false + | Ty_str -> assert false + + (* let value_of_const ((d, _l) : model) (e : Expr.t) : Value.t option = + let e' = encore_expr_aux e in + let v = Colibri2_core.Interp.interp d e' in + c2value_to_value e.ty v *) + + let value (e, _) (c : Expr.t) : Value.t = + let c2v = Interp.interp e (encode_expr c) in + match c2value_to_value c.ty c2v with None -> assert false | Some v -> v + + let values_of_model ?(symbols : Symbol.t list option) ((_, model) : model) : + Model.t = + let m = Hashtbl.create 512 in + match symbols with + | Some symbols -> + List.iter + (fun sy -> + let c = tcst_of_symbol sy in + match List.assoc_opt c model with + | Some v -> ( + match c2value_to_value (tty_to_etype c.DExpr.id_ty) v with + | Some data -> Hashtbl.add m (tcst_to_symbol c) data + | None -> () ) + | _ -> () ) + symbols; + m + | None -> + List.iter + (fun (c, v) -> + match c2value_to_value (tty_to_etype c.DExpr.id_ty) v with + | Some data -> Hashtbl.add m (tcst_to_symbol c) data + | None -> () ) + model; + m + + let satisfiability = + let open Mappings_intf in + function + | `Sat _ -> Satisfiable + | `Unknown _ -> Unknown + | `Unsat -> Unsatisfiable + | `Search -> assert false + | `StepLimitReached -> assert false + + let set_debug = Colibri2_stdlib.Debug.set_info_flags + end +end + +include Fresh.Make () diff --git a/lib/colibri2_mappings.mli b/lib/colibri2_mappings.mli new file mode 100644 index 00000000..126b91ad --- /dev/null +++ b/lib/colibri2_mappings.mli @@ -0,0 +1 @@ +include Mappings_intf.S diff --git a/lib/dune b/lib/dune index 0b5b2d10..6b808e23 100644 --- a/lib/dune +++ b/lib/dune @@ -30,8 +30,19 @@ symbol ty value - z3_mappings) + z3_mappings + colibri2_mappings) (private_modules lexer parser) - (libraries hc z3 ocaml_intrinsics) + (libraries + hc + z3 + ocaml_intrinsics + colibri2.core + colibri2.solver + colibri2.theories.bool + colibri2.theories.quantifiers + colibri2.theories.LRA + colibri2.theories.LRA.stages.stage2 + colibri2.theories.fp) (instrumentation (backend bisect_ppx))) diff --git a/lib/mappings_intf.ml b/lib/mappings_intf.ml index 72575269..44ae48bc 100644 --- a/lib/mappings_intf.ml +++ b/lib/mappings_intf.ml @@ -16,6 +16,7 @@ module type S = sig val value : model -> Expr.t -> Value.t val values_of_model : ?symbols:Symbol.t list -> model -> Model.t val pp_smt : ?status:bool -> Format.formatter -> Expr.t list -> unit + val set_debug : bool -> unit module Solver : sig val make : ?logic:Solver_intf.logic -> unit -> solver diff --git a/lib/z3_mappings.ml b/lib/z3_mappings.ml index bb6912e1..101ec875 100644 --- a/lib/z3_mappings.ml +++ b/lib/z3_mappings.ml @@ -828,6 +828,8 @@ module Fresh = struct Hashtbl.replace m sym v ) symbols'; m + + let set_debug _ = () end end From 815c1da53382d9fa3e2b12cefea54b253c96e567 Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:27:45 +0000 Subject: [PATCH 02/14] Update encoding.opam.template --- encoding.opam.template | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam.template b/encoding.opam.template index 626fe0c1..b1d225ea 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1,4 +1,4 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.master" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From fc3f4ebb4c77fe0c54eb616d1f736d8bd9a74d6b Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:27:50 +0000 Subject: [PATCH 03/14] Update encoding.opam --- encoding.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam b/encoding.opam index b0a0d633..be1d4330 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.master" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From c4c54f23a8fde41211202b52f2371ffe9e1f5097 Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:32:39 +0000 Subject: [PATCH 04/14] Update encoding.opam.template --- encoding.opam.template | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam.template b/encoding.opam.template index b1d225ea..370e3e24 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1,4 +1,4 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.master" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.master" "https://git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From 0e9f034eb0f50d0cdf2329f90e43c5ba1988b6c4 Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:32:52 +0000 Subject: [PATCH 05/14] Update encoding.opam --- encoding.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam b/encoding.opam index be1d4330..327984fa 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.master" "git+ssh://git@git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.master" "https://git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From 26362461aa631a9b7cc7adf48c2552203e0ce02c Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:38:30 +0000 Subject: [PATCH 06/14] Update encoding.opam --- encoding.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam b/encoding.opam index 327984fa..1223f37a 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.master" "https://git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.master" "git+https://git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From 112c22d8fafcd80abc12e9a5239a701a5aaa42db Mon Sep 17 00:00:00 2001 From: filipeom <33165733+filipeom@users.noreply.github.com> Date: Tue, 23 Jan 2024 14:45:36 +0000 Subject: [PATCH 07/14] Update encoding.opam --- encoding.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/encoding.opam b/encoding.opam index 1223f37a..910f53ef 100644 --- a/encoding.opam +++ b/encoding.opam @@ -39,4 +39,5 @@ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ [ "colibri2.master" "git+https://git.frama-c.com/pub/colibrics.git#master"] + [ "colibrilib.master" "git+https://git.frama-c.com/pub/colibrics.git#master"] ] \ No newline at end of file From 7b6851a01f2fd5802b4cd9fa1d10813f267d6ef5 Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:11:52 +0100 Subject: [PATCH 08/14] Make colibri2 compatible with ocaml 5.1.0 --- encoding.opam | 3 +-- encoding.opam.template | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/encoding.opam b/encoding.opam index 910f53ef..f8e4afc9 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,6 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.master" "git+https://git.frama-c.com/pub/colibrics.git#master"] - [ "colibrilib.master" "git+https://git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.5.1.0" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file diff --git a/encoding.opam.template b/encoding.opam.template index 370e3e24..39069cfe 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1,4 +1,4 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.master" "https://git.frama-c.com/pub/colibrics.git#master"] + [ "colibri2.5.1.0" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From 17d55b732bb8e4f63c190125123809d8321799cb Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:20:23 +0100 Subject: [PATCH 09/14] fix colibri2 pin --- encoding.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam b/encoding.opam index f8e4afc9..48d31003 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.5.1.0" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.dev" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From 08562d5ae94ecf2fb26198b81da555bf3acfc7f3 Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:30:09 +0100 Subject: [PATCH 10/14] Add `git+` to the pin --- encoding.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/encoding.opam b/encoding.opam index 48d31003..fae7daf1 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,5 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.dev" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.dev" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From a900a024774c047f2750fef65e8f6a712aee228d Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:44:47 +0100 Subject: [PATCH 11/14] more colibri2 pin fix attempts --- encoding.opam | 3 ++- encoding.opam.template | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/encoding.opam b/encoding.opam index fae7daf1..f1bbbda4 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,5 +38,6 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.dev" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibrilib.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file diff --git a/encoding.opam.template b/encoding.opam.template index 39069cfe..d1829483 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1,4 +1,5 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.5.1.0" "https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibrilib.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From cf6f4b4ef4b546047bb649fa94edfe3ec34e6da9 Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:52:05 +0100 Subject: [PATCH 12/14] more colibri2 pin fix attempts --- encoding.opam.template | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/encoding.opam.template b/encoding.opam.template index d1829483..4b81d3ad 100644 --- a/encoding.opam.template +++ b/encoding.opam.template @@ -1,5 +1,5 @@ available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] - [ "colibrilib.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From 77c5222bed07daeb12491c9dbdd5c04a3d7cb404 Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 16:57:55 +0100 Subject: [PATCH 13/14] update opam file --- encoding.opam | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/encoding.opam b/encoding.opam index f1bbbda4..f50d1c47 100644 --- a/encoding.opam +++ b/encoding.opam @@ -38,6 +38,6 @@ build: [ dev-repo: "git+https://github.com/formalsec/encoding.git" available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32" pin-depends: [ - [ "colibri2.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] - [ "colibrilib.dev" "git+ssh://git@git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] + [ "colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"] ] \ No newline at end of file From 2854f01033a4038d6c918d2aa3aba148c169cc10 Mon Sep 17 00:00:00 2001 From: hra687261 Date: Sat, 27 Jan 2024 17:00:33 +0100 Subject: [PATCH 14/14] Update colibri2_mappings to use ht_expr --- lib/colibri2_mappings.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/lib/colibri2_mappings.ml b/lib/colibri2_mappings.ml index fd995cdd..04e15e7b 100644 --- a/lib/colibri2_mappings.ml +++ b/lib/colibri2_mappings.ml @@ -675,8 +675,8 @@ module Fresh = struct *) let encore_expr_aux ?(record_sym = fun _ -> ()) (e : Expr.t) : expr = let open Expr in - let rec aux ({ e; ty } : t) = - match e with + let rec aux (hte : t) = + match e.node.e with | Val v -> encode_val v | Ptr (base, offset) -> let base' = encode_val (Num (I32 base)) in @@ -684,23 +684,23 @@ module Fresh = struct DTerm.Bitv.add base' offset' | Unop (op, e) -> let e' = aux e in - encode_unop ty op e' + encode_unop hte.node.ty op e' | Binop (op, e1, e2) -> let e1' = aux e1 in let e2' = aux e2 in - encode_binop ty op e1' e2' + encode_binop hte.node.ty op e1' e2' | Triop (op, e1, e2, e3) -> let e1' = aux e1 and e2' = aux e2 and e3' = aux e3 in - encode_triop ty op e1' e2' e3' + encode_triop hte.node.ty op e1' e2' e3' | Relop (op, e1, e2) -> let e1' = aux e1 and e2' = aux e2 in - encode_relop ty op e1' e2' + encode_relop hte.node.ty op e1' e2' | Cvtop (op, e) -> let e' = aux e in - encode_cvtop ty op e' + encode_cvtop hte.node.ty op e' | Symbol s -> let cst = tcst_of_symbol s in record_sym cst; @@ -946,7 +946,9 @@ module Fresh = struct let value (e, _) (c : Expr.t) : Value.t = let c2v = Interp.interp e (encode_expr c) in - match c2value_to_value c.ty c2v with None -> assert false | Some v -> v + match c2value_to_value c.node.ty c2v with + | None -> assert false + | Some v -> v let values_of_model ?(symbols : Symbol.t list option) ((_, model) : model) : Model.t =