Understanding Ref Counting

Stream: lean4

[Marcus Rossel]

This is a minimized standalone version of this question.

I'm running into error 139 (probably a segfault) when using MetaM in the FFI, which I believe is related to reference counting. Here's a minimal setup:

Lean Code

import Lean
open Lean Meta Tactic

-- Note: the following two functions have to be in a separate file for this to build. Otherwise Lake can't find the symbols when building the `check_str` elaborator.

@[export check_str_impl]
def checkStrImpl (s : String) : MetaM Bool := do
  return (← getLCtx).usesUserName (.mkSimple s)

@[extern "check_str"]
opaque checkStr : String → MetaM Bool

elab "check_str" s:str : tactic => do
  logInfo s!"{← checkStr s.getString}"

example (h : True) : True := by
  check_str "h"
  constructor

C Code

#include <lean/lean.h>
#include <stdlib.h>

extern lean_obj_res check_str_impl(
    lean_object* str,
    lean_object* x1,
    lean_object* x2,
    lean_object* x3,
    lean_object* x4,
    lean_object* x5
);

_Bool call_check_str_impl(lean_object* str, lean_object* x1, lean_object* x2, lean_object* x3, lean_object* x4, lean_object* x5) {
    lean_obj_res o = check_str_impl(str, x1, x2, x3, x4, x5);

    switch (o->m_tag) {
        /* EStateM.Result.ok */ case 0: {
            lean_obj_res b = lean_ctor_get(o, 0);
            size_t result = lean_unbox(b);
            return result != 0;
        }
        default: {
            exit(1);
        }
    }
}

// PROBLEM: If we call `call_check_str_impl` twice, we get error 139!
lean_obj_res check_str(lean_obj_arg str, lean_obj_arg x1, lean_obj_arg x2, lean_obj_arg x3, lean_obj_arg x4, lean_obj_arg x5) {
    _Bool result1 = call_check_str_impl(str, x1, x2, x3, x4, x5);
    // _Bool result2 = call_check_str_impl(str, x1, x2, x3, x4, x5);
    lean_object* boolean = lean_box(result1);
    lean_object* metam_state = lean_alloc_ctor(0, 2, 0);
    lean_ctor_set(metam_state, 0, boolean);
    lean_ctor_set(metam_state, 1, x5);
    return metam_state;
}

The problem I'm running into is that when check_str_impl is called more than once, then error 139 occurs. I'm guessing this is because I'm violating the following responsibility stated in the FFI section of the Lean Manual:

By default, all lean_object * parameters of an @[extern] function are considered owned, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via lean_dec.

What would I need to do in order to pass these "virtual RC tokens" to check_str_impl more than once? Or how can I make check_str_impl non-consuming (and what does that mean exactly)?

[Rudi Schneider]

I could imagine that we'd need to call lean_inc on the objects that we pass to check_str_impl?
At least I assume that check_str_impl will "drop" its inputs, and thus call lean_dec on them.

[Henrik Böving]

Yes if you look at the IR you can see

[result]
def checkStrImpl (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : obj) (x_6 : obj) : obj :=
  dec x_5;
  dec x_4;
  dec x_3;
  let x_7 : obj := proj[2] x_2;
  inc x_7;
  dec x_2;
  let x_8 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_9 : obj := Lean.Name.str._override x_8 x_1;
  let x_10 : u8 := Lean.LocalContext.usesUserName x_7 x_9;
  dec x_9;
  dec x_7;
  let x_11 : obj := box x_10;
  let x_12 : obj := ctor_0[EStateM.Result.ok] x_11 x_6;
  ret x_12

[Marcus Rossel]

Oh my god, it works! Thank you :)