Add binding to libpoly

colibri2.opam

@@ -20,7 +20,7 @@ depends: [
   "dolmen_loop" {>= "0.5~dev"}
   "cmdliner"
   "gen"
-  "dune" {>= "2.8"}
+  "dune" {>= "3.0"}
   "dune-build-info"
   "zarith"
   "ppx_deriving" {> "4.1.5"}
@@ -58,4 +58,5 @@ pin-depends: [
   [ "qcheck-alcotest.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-core.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-ounit.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
+  [ "ctypes.0.19.2~dev" "git@github.com:bobot/ocaml-ctypes.git#d9998549d8d69533c8479628040b035e42e75d1a" ]
 ]

colibrics.opam

@@ -12,7 +12,7 @@ depends: [
   "dolmen" {>= "0.5~dev"}
   "dolmen_type" {>= "0.5~dev"}
   "dolmen_loop" {>= "0.5~dev"}
-  "dune" {>= "2.8"}
+  "dune" {>= "3.0"}
   "zarith"
   "cmdliner"
   "ocaml" {>= "4.08"}
@@ -45,4 +45,5 @@ pin-depends: [
   [ "qcheck-alcotest.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-core.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-ounit.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
+  [ "ctypes.0.19.2~dev" "git@github.com:bobot/ocaml-ctypes.git#d9998549d8d69533c8479628040b035e42e75d1a" ]
 ]

dune-project

-(lang dune 2.8)
+(lang dune 3.0)
 
 (cram enable)
 (generate_opam_files true)
 (using coq 0.3)
+(using ctypes 0.1)
 
 (name colibrics)
 (package
@@ -71,3 +72,7 @@
 (package
  (name farith2)
  (synopsis "formaly verified floating-points valuations based on Flocq"))
+
+(package
+ (name ocaml_poly)
+ (synopsis "Binding on libpoly library implementing algebraic numbers"))

farith.opam

@@ -9,7 +9,7 @@ license: "LGPL-3.0-only"
 homepage: "https://git.frama-c.com/bobot/colibrics"
 bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.0"}
   "zarith"
   "odoc" {with-doc}
 ]

farith2.opam

@@ -4,7 +4,7 @@ synopsis: "formaly verified floating-points valuations based on Flocq"
 homepage: "https://git.frama-c.com/bobot/colibrics"
 bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.0"}
   "odoc" {with-doc}
 ]
 build: [

generic.opam.template

@@ -7,4 +7,5 @@ pin-depends: [
   [ "qcheck-alcotest.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-core.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
   [ "qcheck-ounit.0.18" "git+https://github.com/c-cube/qcheck.git#3999873752173b2802b3ee181beae554ef7fa113" ]
+  [ "ctypes.0.19.2~dev" "git@github.com:bobot/ocaml-ctypes.git#d9998549d8d69533c8479628040b035e42e75d1a" ]
 ]

libpoly/dune

+(rule
+ (alias libpoly)
+ (targets libpoly.a dllpoly.so poly.h algebraic_number.h output_language.h
+    dyadic_interval.h
+    dyadic_rational.h
+    integer.h version.h)
+ (deps (source_tree libpoly))
+ (action
+    (no-infer
+  (progn
+    (chdir libpoly/build
+     (progn
+      (run cmake .. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=../../install)
+      (run make static_poly poly)))
+    (copy libpoly/build/src/libpoly.a libpoly.a)
+    (copy libpoly/build/src/libpoly.so dllpoly.so)
+    (copy libpoly/include/poly.h poly.h)
+    (copy libpoly/include/algebraic_number.h algebraic_number.h)
+    (copy libpoly/include/version.h version.h)
+    (copy libpoly/include/output_language.h output_language.h)
+    (copy libpoly/include/dyadic_interval.h dyadic_interval.h)
+    (copy libpoly/include/dyadic_rational.h dyadic_rational.h)
+    (copy libpoly/include/integer.h integer.h)
+   )
+   )
+  )
+)
+
+; (foreign_library
+;  (archive_name libpoly)
+;  (language c)
+;  (names poly coefficient)
+;  (include_dirs libpoly/include/))
+
+(include_subdirs unqualified)
+
+(library
+ (name ocaml_poly)
+ (public_name ocaml_poly)
+ (foreign_archives poly)
+ (libraries zarith)
+ (flags -w -9-27)
+ (ctypes
+  (external_library_name libpoly)
+  (build_flags_resolver (vendored (c_flags ("-Ilibpoly/include/" "-Ilibpoly")) (c_library_flags "-lgmp")))
+  (headers (include "poly.h" "algebraic_number.h" "string.h" "zarith.h"))
+  (type_description
+   (instance Type)
+   (functor Type_description))
+  (function_description
+   (concurrency sequential)
+   (instance Function)
+   (functor Function_description))
+  (generated_types Types_generated)
+  (generated_entry_point C))
+)

libpoly/function_description.ml

+open Ctypes
+
+(* This Types_generated module is an instantiation of the Types
+   functor defined in the type_description.ml file. It's generated by
+   a C program that dune creates and runs behind the scenes. *)
+module Types = Types_generated
+
+module Functions (F : Ctypes.FOREIGN) = struct
+  open F
+  open Types
+
+  let lp_trace_enable =
+    foreign "lp_trace_enable" (ocaml_string @-> returning void)
+
+  let lp_trace_disable =
+    foreign "lp_trace_disable" (ocaml_string @-> returning void)
+
+  let lp_algebraic_number_sgn =
+    foreign "lp_algebraic_number_sgn" (ptr lp_algebraic_number @-> returning int)
+
+  let lp_algebraic_number_cmp =
+    foreign "lp_algebraic_number_cmp"
+      (ptr lp_algebraic_number @-> ptr lp_algebraic_number @-> returning int)
+
+  let lp_algebraic_number_cmp_integer =
+    foreign "lp_algebraic_number_cmp_integer"
+      (ptr lp_algebraic_number @-> mpz @-> returning int)
+
+  let lp_algebraic_number_to_double =
+    foreign "lp_algebraic_number_to_double"
+      (ptr lp_algebraic_number @-> returning double)
+
+  let lp_algebraic_number_construct_zero =
+    foreign "lp_algebraic_number_construct_zero"
+      (ptr lp_algebraic_number @-> returning void)
+
+  let lp_algebraic_number_destruct =
+    foreign "lp_algebraic_number_destruct"
+      (ptr lp_algebraic_number @-> returning void)
+
+  let lp_algebraic_number_construct_from_integer =
+    foreign "lp_algebraic_number_construct_from_integer"
+      (ptr lp_algebraic_number @-> mpz @-> returning void)
+
+  let lp_algebraic_number_div =
+    foreign "lp_algebraic_number_div"
+      (ptr lp_algebraic_number @-> ptr lp_algebraic_number
+     @-> ptr lp_algebraic_number @-> returning void)
+
+  let lp_algebraic_number_pow =
+    foreign "lp_algebraic_number_pow"
+      (ptr lp_algebraic_number @-> ptr lp_algebraic_number @-> ulong
+     @-> returning void)
+
+  let lp_algebraic_number_positive_root =
+    foreign "lp_algebraic_number_positive_root"
+      (ptr lp_algebraic_number @-> ptr lp_algebraic_number @-> ulong
+     @-> returning void)
+
+  let lp_algebraic_number_to_string =
+    foreign "lp_algebraic_number_to_string"
+      (ptr lp_algebraic_number @-> returning (ptr char))
+
+  let ml_z_mpz_init_set_z =
+    foreign "ml_z_mpz_init_set_z" (mpz @-> z @-> returning void)
+
+  let mpz_clear = foreign "mpz_clear" (mpz @-> returning void)
+
+  let free = foreign "free" (ptr char @-> returning void)
+
+  let strlen = foreign "strlen" (ptr char @-> returning size_t)
+end

libpoly @ b4b7b32f

+Subproject commit b4b7b32fb2abf5c33f5bc65d905cd25c4caa3493

libpoly/ocaml_poly.ml

+open Ctypes
+
+type t = C.Type.lp_algebraic_number structure ptr
+
+let trace_enable tag = C.Function.lp_trace_enable (ocaml_string_start tag)
+
+let trace_disable tag = C.Function.lp_trace_disable (ocaml_string_start tag)
+
+let mk () =
+  allocate_n
+    ~finalise:(fun p -> C.Function.lp_algebraic_number_destruct p)
+    C.Type.lp_algebraic_number ~count:1
+
+let zero () =
+  let a = mk () in
+  C.Function.lp_algebraic_number_construct_zero a;
+  a
+
+let compare a b = C.Function.lp_algebraic_number_cmp a b
+
+let equal a b = compare a b = 0
+
+let to_string a =
+  let c = C.Function.lp_algebraic_number_to_string a in
+  let s =
+    string_from_ptr c ~length:(Unsigned.Size_t.to_int (C.Function.strlen c))
+  in
+  C.Function.free c;
+  s
+
+let to_double a = C.Function.lp_algebraic_number_to_double a
+
+let of_bigint z =
+  let m = Ctypes.allocate_n C.Type.mpz_struct 1 in
+  C.Function.ml_z_mpz_init_set_z m z;
+  let a = mk () in
+  C.Function.lp_algebraic_number_construct_from_integer a m;
+  C.Function.mpz_clear m;
+  a
+
+let div a b =
+  let c = mk () in
+  C.Function.lp_algebraic_number_div c a b;
+  c
+
+let pow a n =
+  let b = mk () in
+  C.Function.lp_algebraic_number_pow b a (Unsigned.ULong.of_int n);
+  b
+
+let positive_root a n =
+  let b = mk () in
+  C.Function.lp_algebraic_number_positive_root b a (Unsigned.ULong.of_int n);
+  b

libpoly/ocaml_poly.mli

+type t
+
+val compare : t -> t -> int
+
+val equal : t -> t -> bool
+
+val zero : unit -> t
+
+val to_string : t -> string
+
+val to_double : t -> float
+
+val of_bigint : Z.t -> t
+
+val div : t -> t -> t
+
+val pow : t -> int -> t
+
+val positive_root : t -> int -> t
+
+val trace_enable : string -> unit
+
+val trace_disable : string -> unit

libpoly/tests/dune

+(include_subdirs unqualified)
+
+(test
+ (name unit)
+ (libraries ocaml_poly zarith)
+)

libpoly/tests/unit.expected

+0
+2
+<3*x + (-1), (1/4, 1/2)>
+4
+<1*x^2 + (-2), (5/4, 3/2)> 1.414214 1.414214
+2 true
+<1*x^4 + (-2), (1, 5/4)> 1.189207 1.189207
+<1*x^4 + (-2), (1, 5/4)> 1.189207 1.189207 true
+<1*x^21 + (-2022), (5/4, 3/2)> 1.436872 1.436872

libpoly/tests/unit.ml

+open Ocaml_poly
+
+(* let () = trace_enable "algebraic_number" *)
+
+let _ = print_endline (to_string (zero ()))
+
+let two = of_bigint (Z.of_int 2)
+
+let _ = print_endline (to_string two)
+
+let _ =
+  print_endline
+    (to_string (div (of_bigint (Z.of_int 1)) (of_bigint (Z.of_int 3))))
+
+let _ = print_endline (to_string (pow two 2))
+
+let r2 = positive_root two 2
+
+let _ = Printf.printf "%s %f %f\n" (to_string r2) (to_double r2) (2. ** 0.5)
+
+let _ =
+  let two' = pow r2 2 in
+  Printf.printf "%s %b\n" (to_string two') (equal two two')
+
+let rr2 = positive_root r2 2
+
+let _ = Printf.printf "%s %f %f\n" (to_string rr2) (to_double rr2) (2. ** 0.25)
+
+let rr2' = positive_root two 4
+
+let _ =
+  Printf.printf "%s %f %f %b\n" (to_string rr2) (to_double rr2) (2. ** 0.25)
+    (equal rr2 rr2')
+
+let r2022 = positive_root (of_bigint (Z.of_int 2022)) 21
+
+let _ =
+  Printf.printf "%s %f %f\n" (to_string r2022) (to_double r2022)
+    (2022. ** (1. /. 21.))

libpoly/type_description.ml

+open Ctypes
+
+module Types (F : Ctypes.TYPE) = struct
+  open F
+
+  (* let version_major = constant "LIBPOLY_VERSION_MAJOR" int
+   * 
+   * let version_minor = constant "LIBPOLY_VERSION_MINOR" int
+   * 
+   * let version_patch = constant "LIBPOLY_VERSION_PATCH" int *)
+
+  let libpoly_typedef_structure_nosize name =
+    typedef (structure (name ^ "_struct")) (name ^ "_t")
+
+  let libpoly_typedef_structure_sized name =
+    let s = structure (name ^ "_struct") in
+    seal s;
+    typedef s (name ^ "_t")
+
+  type lp_algebraic_number
+
+  let lp_algebraic_number : lp_algebraic_number structure typ =
+    libpoly_typedef_structure_sized "lp_algebraic_number"
+
+  type mpz_struct
+
+  let mpz_struct : mpz_struct structure typ =
+    let s = typedef (structure "__mpz_struct") "__mpz_struct" in
+    seal s;
+    s
+
+  let mpz = ptr mpz_struct
+
+  let z : Z.t typ = ocaml_value ~format:Z.pp_print "Z.t"
+end

libpoly/zarith.h

+/**
+  Public C interface for Zarith.
+
+  This is intended for C libraries that wish to convert between mpz_t and
+  Z.t objects.
+
+
+  This file is part of the Zarith library
+  http://forge.ocamlcore.org/projects/zarith .
+  It is distributed under LGPL 2 licensing, with static linking exception.
+  See the LICENSE file included in the distribution.
+
+  Copyright (c) 2010-2011 Antoine Miné, Abstraction project.
+  Abstraction is part of the LIENS (Laboratoire d'Informatique de l'ENS),
+  a joint laboratory by:
+  CNRS (Centre national de la recherche scientifique, France),
+  ENS (École normale supérieure, Paris, France),
+  INRIA Rocquencourt (Institut national de recherche en informatique, France).
+
+*/
+
+
+/* gmp.h or mpir.h must be included manually before zarith.h */
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <caml/mlvalues.h>
+
+/* sets rop to the value in op (limbs are copied) */
+void ml_z_mpz_set_z(mpz_t rop, value op);
+
+/* inits and sets rop to the value in op (limbs are copied) */
+void ml_z_mpz_init_set_z(mpz_t rop, value op);
+
+/* returns a new z objects equal to op (limbs are copied) */
+value ml_z_from_mpz(mpz_t op);
+
+#ifdef __cplusplus
+}
+#endif

ocaml_poly.opam

+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Binding on libpoly library implementing algebraic numbers"
+homepage: "https://git.frama-c.com/bobot/colibrics"
+bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
+depends: [
+  "dune" {>= "3.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"

src_colibri2/theories/LRA/realValue.ml

@@ -23,7 +23,7 @@ open Colibri2_popop_lib
 open Colibri2_stdlib.Std
 
 module Builtin = struct
-  type _ Expr.t += BV2Nat of int | Pow_int_int | Int2BV of int
+  type _ Expr.t += BV2Nat of int | Pow_int_int | Pow_real_int | Int2BV of int
 
   let parse_int _env _ast s =
     match int_of_string s with
@@ -60,6 +60,11 @@ module Builtin = struct
       (Dolmen_std.Path.global "colibri_pow_int_int")
       (Expr.Ty.arrow [ Expr.Ty.int; Expr.Ty.int ] Expr.Ty.int)
 
+  let colibri_pow_real_int =
+    Expr.Id.mk ~name:"colibri_pow_real_int" ~builtin:Pow_real_int
+      (Dolmen_std.Path.global "colibri_pow_real_int")
+      (Expr.Ty.arrow [ Expr.Ty.real; Expr.Ty.int ] Expr.Ty.real)
+
   let colibri_cdiv =
     Expr.Id.mk ~name:"colibri_cdiv" ~builtin:Expr.Div_t
       (Dolmen_std.Path.global "colibri_cdiv")
@@ -114,6 +119,9 @@ module Builtin = struct
         | Dolmen_loop.Typer.T.Id
             { ns = Term; name = Simple "colibri_pow_int_int" } ->
             app2 env s colibri_pow_int_int
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri_pow_real_int" } ->
+            app2 env s colibri_pow_real_int
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_cdiv" } ->
             app2 env s colibri_cdiv
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_ceil" } ->
@@ -310,8 +318,12 @@ module Check = struct
         let a, b = IArray.extract2_exn args in
         let a = !>a in
         let b = !>b in
-        if Q.sign b < 0 && Q.sign a = 0 then `Uninterp
-        else !<(Q.pow a (Q.to_int b))
+        if Q.sign b < 0 then `Uninterp else !<(Q.pow a (Q.to_int b))
+    | { app = { builtin = Builtin.Pow_real_int }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        let a = !>a in
+        let b = !>b in
+        if Q.sign b < 0 then `Uninterp else !<(Q.pow a (Q.to_int b))
     | { app = { builtin = Expr.Lt }; tyargs = []; args; ty = _ } ->
         let a, b = IArray.extract2_exn args in
         !<<(Q.lt !>a !>b)