parapluu / Concuerror

Concuerror is a stateless model checking tool for Erlang programs.
http://parapluu.github.io/Concuerror
BSD 2-Clause "Simplified" License
333 stars 41 forks source link

In memory modules aren't supported #299

Open hauleth opened 5 years ago

hauleth commented 5 years ago

Describe the bug

Concuerror silently fails on in-memory modules.

To Reproduce

%% Define module in memory

Module = erl_syntax:attribute(erl_syntax:atom(module),[erl_syntax:atom(sample)]).
ModForm =  erl_syntax:revert(Module).

Export = erl_syntax:attribute(erl_syntax:atom(export),[erl_syntax:list([erl_syntax:arity_qualifier(erl_syntax:atom(test),erl_syntax:integer(0))])]).
ExportForm = erl_syntax:revert(Export).

% define the function body
Body = erl_syntax:atom(nil).

% define the first clause
Clause =  erl_syntax:clause([],[],[Body]).

% define the function
Function =  erl_syntax:function(erl_syntax:atom(test),[Clause]).
FunctionForm = erl_syntax:revert(Function).

{ok, Mod, Bin1} = compile:forms([ModForm,ExportForm, FunctionForm]).
code:load_binary(Mod, [], Bin1).

%% Now run concuerror on it

concuerror:run([{module, sample}]).

This will success but there will be information that module cannot be loaded, which in fact mean that it silently does nothing.

Expected behavior

It should run tests.

It could fail, but it would be infeasible, as Elixir tests are defined in way similar to this, which makes testing them with concuerror quite troublesome (you need to create additional module in separate file (that is compiled) and only then you can run test on it).

Environment (please complete the following information):

Additional context

This was found when tried to run Concuerror tests on Elixir tests.

Example Elixir code:

defmodule ConcuerrorElixirExampleTest do
  def message_test do
    this = self()
    spawn(fn -> send(this, :foo) end)
    spawn(fn -> send(this, :bar) end)

    receive do
      msg -> :foo = msg
    end
  end
end

:ok = :concuerror.run(module: ConcuerrorElixirExampleTest, test: :message_test)

This must be saved as file with .exs extension and ran via elixir file.exs to reproduce error.

aronisstav commented 5 years ago

Hi @hauleth ! Interesting (and hard) case! Thank you for spending time to make an Erlang equivalent.

Concuerror needs the abstract syntax tree of a module in order to instrument it, so it will be infeasible to fix this problem if that tree is not available in any way from Elixir script files.

As a line of investigation for you, is it possible to get coverage information for .exs files? If so, is cover used for that? cover is also instrumenting using the AST, so perhaps a similar approach can be followed to send a test to Concuerror.

hauleth commented 5 years ago

@aronisstav I have found the problematic line and it seems that it cannot be solved right now due to Erlang issue (ERL-805). And no, cover:compile(Mod) do not work as well on such module.

aronisstav commented 5 years ago

@hauleth Right, but I am afraid that this is a design decision: there are no such introspection capabilities (i.e. "show me the abstract code of this loaded beam for which I have no file on disk") on the Erlang/OTP VM.

hauleth commented 5 years ago

@aronisstav the point is that you can get that data, what is more, you get it each time when you build your module in-memory in Elixir (it doesn't fully work in Erlang version, probably there are other steps involved there) you get that data back:

{:module, ConcuerrorElixirExampleTest, bin, _} =
  defmodule ConcuerrorElixirExampleTest do
    def message_test do
      this = self()
      spawn(fn -> send(this, :foo) end)
      spawn(fn -> send(this, :bar) end)

      receive do
        msg -> :foo = msg
      end
    end
  end

IO.inspect :beam_lib.chunks(bin, [:abstract_code])

So this need to be stored somewhere (for example for error reporting), so it need to be fetchable in some way, the question is how.

hauleth commented 5 years ago

@aronisstav temporary workaround could be if you would expose API that accept compiled module binary or AST instead of requiring module name. That would allow me to create few Elixir hacks to get it working.

aronisstav commented 5 years ago

@hauleth Such an API can be built by:

hauleth commented 5 years ago

I have achieved some success with this code:

defmodule ConcuerrorElixirExampleTest do
  use ExUnit.Case, async: true
  doctest ConcuerrorElixirExample

  @after_compile __MODULE__

  def message_test do
    this = self()
    spawn(fn -> send(this, :foo) end)
    spawn(fn -> send(this, :bar) end)

    receive do
      msg -> assert :foo == msg
    end
  end

  test "Foo" do
    beam = Agent.get(:conc_mod, fn beam -> beam end)
    :concuerror_loader.initialize([])
    :concuerror_loader.load_binary(__MODULE__, to_charlist(__ENV__.file), beam)
    :concuerror.run(module: __MODULE__, test: :message_test)
  end

  def __after_compile__(_env, beam) do
    Agent.start(fn -> beam end, name: :conc_mod)
  end
end

This raises another question #300.

Nezteb commented 1 year ago

https://github.com/erlang/otp/issues/3755 was closed, though I can't tell if it was actually fixed. Is this still an issue? 🤔

hauleth commented 1 year ago

@Nezteb yes, it is still issue. It was not fixed and will not be fixed. I have an idea for workaround, but never had time to sit and write that code.