Upstream/vm dynload

library/system/foreign.lean

@@ -0,0 +1,176 @@
+namespace foreign
+
+open nat
+
+def bounded (a p q : ℤ) := p ≤ a ∧ a < q
+
+structure irange (l u : ℤ) :=
+(val : ℤ)
+(bounded : bounded val l u)
+
+namespace irange
+
+protected def lt {p q} (a b : irange p q) : Prop :=
+a.val < b.val
+
+protected def le {p q} (a b : irange p q) : Prop :=
+a.val ≤ b.val
+
+instance {p q} : has_lt (irange p q)  := ⟨irange.lt⟩
+instance {p q} : has_le (irange p q)  := ⟨irange.le⟩
+
+instance decidable_lt {p q} (a b : irange p q) :  decidable (a < b) :=
+int.decidable_lt _ _
+
+instance decidable_le {p q} (a b : irange p q) : decidable (a ≤ b) :=
+int.decidable_le _ _
+
+def {u} elim0 {α : Sort u} {p} : irange p p → α
+| ⟨_, h₀, h₁⟩ := false.elim (not_lt_of_ge h₀ h₁)
+
+variable {n : nat}
+
+lemma eq_of_veq {p q} : ∀ {i j : irange p q}, (val i) = (val j) → i = j
+| ⟨iv, ilt₁, glt₁⟩ ⟨.(iv), ilt₂, glt₂⟩ rfl := rfl
+
+lemma veq_of_eq {p q} : ∀ {i j : irange p q}, i = j → (val i) = (val j)
+| ⟨iv, ilt, igt⟩ .(_) rfl := rfl
+
+lemma ne_of_vne {p q} {i j : irange p q} (h : val i ≠ val j) : i ≠ j :=
+λ h', absurd (veq_of_eq h') h
+
+lemma vne_of_ne {p q} {i j : irange p q} (h : i ≠ j) : val i ≠ val j :=
+λ h', absurd (eq_of_veq h') h
+
+end irange
+
+open irange
+
+instance (p q : ℤ) : decidable_eq (irange p q) :=
+λ i j, decidable_of_decidable_of_iff
+  (int.decidable_eq i.val j.val) ⟨eq_of_veq, veq_of_eq⟩
+
+namespace irange
+open int
+variables {p q : int}
+
+protected def succ : irange p q → irange p (q+1)
+| ⟨a, h, h'⟩ := ⟨a+1, le_trans h (le_add_of_nonneg_right zero_le_one), add_lt_add_right h' _⟩
+
+section truncate
+
+def truncate (x p q : ℤ) := (x - p) % (q - p) + p
+
+variables {x : ℤ} {p q}
+variables (y : ℤ) (h : p ≤ y) (h' : y < q)
+
+private lemma pos_q_sub_p : 0 < (q - p) :=
+sub_pos_of_lt (lt_of_le_of_lt h h')
+
+private lemma q_sub_p_ne_zero :  (q - p) ≠ 0 :=
+ne_of_gt (pos_q_sub_p _ h h')
+
+lemma le_truncate : p ≤ truncate x p q :=
+le_add_of_sub_right_le $
+suffices 0 ≤ (x - p) % (q - p), by simp * at *,
+int.nonneg_mod (q_sub_p_ne_zero _ h h')
+
+lemma truncate_lt : truncate x p q < q :=
+add_lt_of_lt_sub_right $ int.mod_lt $ pos_q_sub_p y h h'
+
+lemma bounded_truncate (h : foreign.bounded y p q) : foreign.bounded (truncate x p q) p q :=
+⟨ le_truncate _ h.1 h.2, truncate_lt _ h.1 h.2 ⟩
+
+lemma bounded_zero {p q : ℕ} : foreign.bounded 0 (-p) q.succ :=
+⟨ neg_le_of_neg_le (coe_nat_le_coe_nat_of_le $ nat.zero_le _), coe_nat_lt_coe_nat_of_lt (nat.zero_lt_succ _) ⟩
+
+end truncate
+
+def of_int {p q : ℕ} (a : int) : irange (- p) q.succ :=
+⟨ truncate a (-p) (succ q), bounded_truncate 0 bounded_zero ⟩
+
+protected def add : irange p q → irange p q → irange p q
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a + b) p q, bounded_truncate _ h⟩
+
+protected def mul : irange p q → irange p q → irange p q
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a * b) p q, bounded_truncate _ h⟩
+
+protected def sub : irange p q → irange p q → irange p q
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a - b) p q, bounded_truncate _ h⟩
+
+protected def mod : irange p q → irange p q → irange p q
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a % b) p q, bounded_truncate _ h⟩
+
+protected def div : irange p q → irange p q → irange p q
+| ⟨a, h⟩ ⟨b, _⟩ := ⟨truncate (a / b) p q, bounded_truncate _ h⟩
+
+instance {p q : ℕ} : has_zero (irange (-p) q.succ) := ⟨of_int 0⟩
+instance {p q : ℕ} : has_one (irange (-p) q.succ) := ⟨of_int 1⟩
+instance : has_add (irange p q)         := ⟨irange.add⟩
+instance : has_sub (irange p q)         := ⟨irange.sub⟩
+instance : has_mul (irange p q)         := ⟨irange.mul⟩
+instance : has_mod (irange p q)         := ⟨irange.mod⟩
+instance : has_div (irange p q)         := ⟨irange.div⟩
+instance : has_repr (irange p q)        := ⟨repr ∘ irange.val⟩
+
+lemma of_int_zero {p q : ℕ} : @of_int p q 0 = 0 := rfl
+
+lemma add_def (a b : irange p q) : (a + b).val = truncate (a.val + b.val) p q :=
+show (irange.add a b).val = truncate (a.val + b.val) p q, from
+by cases a; cases b; simp [irange.add]
+
+lemma mul_def (a b : irange p q) : (a * b).val = truncate (a.val * b.val) p q :=
+show (irange.mul a b).val = truncate (a.val * b.val) p q, from
+by cases a; cases b; simp [irange.mul]
+
+lemma sub_def (a b : irange p q) : (a - b).val = truncate (a.val - b.val) p q :=
+show (irange.sub a b).val = truncate (a.val - b.val) p q, from
+by cases a; cases b; simp [irange.sub]
+
+lemma mod_def (a b : irange p q) : (a % b).val = truncate (a.val % b.val) p q :=
+show (irange.mod a b).val = truncate (a.val % b.val) p q, from
+by cases a; cases b; simp [irange.mod]
+
+lemma div_def (a b : irange p q) : (a / b).val = truncate (a.val / b.val) p q :=
+show (irange.div a b).val = truncate (a.val / b.val) p q, from
+by cases a; cases b; simp [irange.div]
+
+lemma lt_def (a b : irange p q) : (a < b) = (a.val < b.val) :=
+show (irange.lt a b) = (a.val < b.val), from
+by cases a; cases b; simp [irange.lt]
+
+lemma le_def (a b : irange p q) : (a ≤ b) = (a.val ≤ b.val) :=
+show (irange.le a b) = (a.val ≤ b.val), from
+by cases a; cases b; simp [irange.le]
+
+lemma val_zero {p q : ℕ} : (0 : irange (-p) q.succ).val = 0 :=
+show truncate 0 _ _ = 0, from
+sub_eq_zero_of_eq $
+begin
+  suffices : p % (q.succ + p) = p,
+  { conv { to_rhs, rw ← this }, simp, refl },
+  apply mod_eq_of_lt, apply lt_add_of_zero_lt_right,
+  apply zero_lt_succ,
+end
+
+end irange
+
+@[reducible]
+def uint_8 := fin $ succ 255
+@[reducible]
+def uint_16 := fin $ succ 65535
+@[reducible]
+def uint_32 := unsigned
+@[reducible]
+def uint_64 := fin $ succ 18446744073709551615
+
+@[reducible]
+def int_8 := irange (-succ 127) (succ 127)
+@[reducible]
+def int_16 := irange (-succ 32767) (succ 32767)
+@[reducible]
+def int_32 := irange (-succ 2147483647) (succ 2147483647)
+@[reducible]
+def int_64 := irange (-succ 9223372036854775807) (succ 9223372036854775807)
+
+end foreign

src/library/tactic/vm_monitor.cpp

@@ -191,7 +191,6 @@ vm_obj _vm_decl_kind(vm_obj const & d) {
     case vm_decl_kind::Bytecode: return mk_vm_simple(0);
     case vm_decl_kind::Builtin:  return mk_vm_simple(1);
     case vm_decl_kind::CFun:     return mk_vm_simple(2);
-    case vm_decl_kind::FFICall:  return mk_vm_simple(3);
     }
     lean_unreachable();
 }

src/library/vm/vm.cpp

@@ -8,7 +8,11 @@ Author: Leonardo de Moura
 #include <string>
 #include <algorithm>
 #include <vector>
-#include <ffi/ffi.h>
+#ifdef __linux__
+  #include <ffi.h>
+#else
+  #include <ffi/ffi.h>
+#endif
 #include <unordered_map>
 #include <unordered_set>
 #include <iomanip>
@@ -1180,7 +1184,7 @@ struct vm_decls : public environment_extension {
 
     void bind_foreign_symbol(name const & obj, name const & decl, string const & c_fun, buffer<expr> const & args, expr const & t) {
         auto idx = get_vm_index(decl);
-        m_decls.insert(idx, m_foreign[obj]->get_cfun(decl, idx, c_fun, args, t));
+        m_decls.insert(idx, m_foreign[obj].get_cfun(decl, idx, c_fun, args, t));
     }
 
     unsigned reserve(name const & n, unsigned arity) {
@@ -1804,9 +1808,6 @@ vm_obj vm_state::invoke_closure(vm_obj const & fn, unsigned DEBUG_CODE(nargs)) {
     case vm_decl_kind::CFun:
         invoke_cfun(d);
         break;
-    case vm_decl_kind::FFICall:
-        invoke_ffi_call(d);
-        break;
     }
     m_pc     = saved_pc;
     vm_obj r = m_stack.back();
@@ -2955,18 +2956,6 @@ void vm_state::invoke_cfun(vm_decl const & d) {
     }
 }
 
-void vm_state::invoke_ffi_call(vm_decl const & d) {
-    if (m_profiling) {
-        unique_lock<mutex> lk(m_call_stack_mtx);
-        push_frame_core(0, 0, d.get_idx());
-    }
-    invoke_ffi_call(d.get_cfn(), d.m_sig);
-    if (m_profiling) {
-        unique_lock<mutex> lk(m_call_stack_mtx);
-        m_call_stack.pop_back();
-    }
-}
-
 void vm_state::invoke(vm_decl const & d) {
     switch (d.kind()) {
     case vm_decl_kind::Bytecode:

src/library/vm/vm.h

@@ -10,10 +10,10 @@ Author: Leonardo de Moura
 #include <vector>
 #include <string>
 #include <cstdint>
-#ifdef USE_FFI_FFI_H
-#include <ffi/ffi.h>
-#else
+#ifdef __linux__
 #include <ffi.h>
+#else
+#include <ffi/ffi.h>
 #endif
 #include "util/debug.h"
 #include "util/compiler_hints.h"

src/library/vm/vm_environment.cpp

@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_pos_info.h"
 #include "library/vm/vm_rb_map.h"
 #include "frontends/lean/structure_cmd.h"
+#include "util/path.h"
 
 namespace lean {
 struct vm_environment : public vm_external {
@@ -319,7 +320,7 @@ vm_obj environment_load_foreign_object(vm_obj const & _env, vm_obj const & _n, v
     environment env = to_env(_env);
     name n = to_name(_n);
     std::string file_name = to_string(_file_name);
-    return to_obj(load_foreign_object(env,n,file_name));
+    return to_obj(load_foreign_object(env, n, normalize_path(file_name)));
 }
 
 void initialize_vm_environment() {

src/library/vm/vm_ffi.cpp

@@ -6,7 +6,11 @@ Author: James King <james@agenultra.com>, Simon Hudon
 */
 
 #include <dlfcn.h>
-#include <ffi/ffi.h>
+#ifdef __linux__
+  #include <ffi.h>
+#else
+  #include <ffi/ffi.h>
+#endif
 #include <string>
 
 #include "util/lean_path.h"
@@ -150,52 +154,4 @@ namespace lean {
         delete g_int64_name;
     }
 
-    static name * g_vm_ffi;
-    struct vm_ffi_attribute_data : public attr_data {
-        name m_obj;
-        optional<name> m_c_fun;
-        vm_ffi_attribute_data() {}
-        // vm_ffi_attribute_data(name const & n) : m_name(n) {}
-        // virtual unsigned hash() const override {return m_name.hash();}
-        void write(serializer & s) const {s << m_obj << m_c_fun;}
-        void read(deserializer & d) {
-            d >> m_obj >> m_c_fun;
-        }
-        void parse(abstract_parser & p) override {
-            lean_assert(dynamic_cast<parser *>(&p));
-            auto & p2 = *static_cast<parser *>(&p);
-            m_obj = p2.check_constant_next("not a constant");
-            if (p2.curr_is_identifier()) {
-                m_c_fun = optional<name>(p2.get_name_val());
-                p2.next();
-            } else {
-                m_c_fun = optional<name>();
-            }
-        }
-    };
-    // bool operator==(vm_ffi_attribute_data const & d1, vm_ffi_attribute_data const & d2) {
-    //     return d1.m_name == d2.m_name;
-    // }
-
-    template class typed_attribute<vm_ffi_attribute_data>;
-    typedef typed_attribute<vm_ffi_attribute_data> vm_ffi_attribute;
-
-    static vm_ffi_attribute const & get_vm_ffi_attribute() {
-        return static_cast<vm_ffi_attribute const &>(get_system_attribute(*g_vm_ffi));
-    }
-
-
-    void initialize_vm_ffi() {
-        register_system_attribute(basic_attribute(
-            "ffi", "Registers a binding to a foreign function.",
-            [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment {
-                auto data = get_vm_ffi_attribute().get(env, d);
-                name sym = data->m_c_fun? *data->m_c_fun : data->m_obj;
-                return add_foreign_symbol(env, d, data->m_obj, sym.to_string());
-            }));
-    }
-
-    void finalize_vm_ffi() {
-    }
-
 }

tests/lean/ffi.lean

@@ -22,8 +22,9 @@ do
      io.env.set_cwd "vm_dynload",
      b ← io.fs.file_exists "some_file.so",
      if b then io.fs.remove "some_file.so" else pure (),
-     (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln },
-   load_foreign_object `foo "vm_dynload/some_file.so",
+     (io.cmd { cmd := "make", args := ["some_file.so"] }) >>= io.print_ln,
+     io.env.set_cwd ".." },
+   load_foreign_object `foo "./vm_dynload/some_file.so",
    -- bind_foreign_symbol `foo `main 2 "main",
    return ()
 

tests/lean/vm_dynload/Makefile

@@ -12,4 +12,4 @@ some_file.so: some_file.o
 	gcc some_file.o -shared -o some_file.so
 
 client: client.c
-	gcc client.c -o client  -I$(INCLUDES) -lffi
+	gcc client.c -o client  -I$(INCLUDES) -lffi -ldl

tests/lean/vm_dynload/client.c

@@ -29,7 +29,7 @@ void call(main_fn fn, int x, int y) {
 
 int main () {
     main_fn my_main;
-    void* handle = dlopen("some_file.so", RTLD_LAZY);
+    void* handle = dlopen("./some_file.so", RTLD_LAZY);
     if (!handle) {
         printf("Cannot load library: %s", dlerror());
         return -1;