Skip to content

Commit 54a9b71

Browse files
UncleGrumpyUncleGrumpy
authored
Merge pull request #48 from UncleGrumpy/dialyze
Add atomvm dialyzer provider
2 parents 89ee367 + 1074a41 commit 54a9b71

File tree

4 files changed

+376
-0
lines changed

4 files changed

+376
-0
lines changed

‎CHANGELOG.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,11 @@ All notable changes to this project will be documented in this file.
1111
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
1212
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
1313

14+
## [0.7.6] (unreleased)
15+
16+
### Added
17+
- Added dialyzer task to simplify running dialyzer on AtomVM applications.
18+
1419
## [0.7.5] (2025.05.27)
1520

1621
### Fixed

‎README.md‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ The [`rebar3`](https://rebar3.org) plugin provides the following tasks under the
6363
* `pico_flash` Flash "packed" uf2 files to RP2040 (RPi Pico) devices by copying to FATfs.
6464
* `version` Print the version of the [`atomvm_rebar3_plugin`](https://atomvm.github.io/atomvm_rebar3_plugin) to the console.
6565
* `bootstrap` Compile Erlang files that `rebar3` otherwise cannot compile. Typically, such files include modules from the OTP `kernel` or `stdlib` application that `rebar3` uses internally for its own implementation.
66+
* `dialyzer` Use dialyzer for static analysis of AtomVM applications.
6667

6768
> IMPORTANT! Some of the above tasks were previously located under the default [`rebar3`](https://rebar3.org) namespace; however, the commands under the default namespace have been DEPRECATED. Users will get a warning message on the console when using deprecated tasks, and any deprecated tasks may be removed in the future without warning. Be sure to migrate any scripts or code you have to use the `atomvm` namespace.
6869
@@ -515,6 +516,39 @@ Any setting specified on the command line take precedence over entries in `rebar
515516

516517
The `uf2create` task depends on the `packbeam` task, so the packbeam file will get automatically built if any changes have been made to its dependencies.
517518

519+
### The `dialyzer` task
520+
521+
Use the `dialyzer` task to check applications for type discrepancies. To use the example just run:
522+
523+
```shell
524+
$ rebar3 atomvm dialyzer
525+
```
526+
527+
This task requires a complete AtomVM installation. This includes the AtomVM binary, the standard atomvmlib libraries, compiled beam files, and the `atomvm`
528+
launcher script. The `atomvm` launcher script should be in your PATH. This is all taken care of with a MacOS install using MacPorts, or Homebrew.
529+
Linux users will need to build from source and use the cmake "install" target. If you have "installed" AtomVM to a non-standard location (i.e. /otp/atomvm)
530+
and the `atomvm` launcher script is not in your PATH you must supply the install location containing the AtomVM libraries using the `--atomvm_root` option
531+
when using this task. For example:
532+
533+
```
534+
$ rebar3 atomvm dialyzer --atomvm_root /opt/atomvm
535+
```
536+
537+
This option may also be supplied in the `atomvm_rebar3_plugin` configuration options in rebar.conf. Example:
538+
539+
```erlang
540+
{atomvm_rebar3_plugin, [{dialyzer, [{atomvm_root, "/opt/atomvm"}]}]}.
541+
```
542+
543+
Options available from the command line, or rebar3.conf are:
544+
545+
| Key | Type | Default | Description |
546+
|-----|------|---------|-------------|
547+
| `base_plt_location` |`string()` \| `binary()` | "$HOME/.cache/rebar3" | Location of base PLT |
548+
| `plt_location` | `string()` \| `binary()` | build profile base directory | Location of application PLT |
549+
| `plt_prefix` | `string()` | application name | The base name of the application plt |
550+
| `atomvm_root` | `string()` \| `binary()` | detected | If the `atomvm` launcher script is in PATH this will be detected automatically, otherwise specify the atomvm base directory containing the atomvm libraries |
551+
518552
### The `version` task
519553

520554
use the `version` task to print the current version of the [`atomvm_rebar3_plugin`](https://atomvm.github.io/atomvm_rebar3_plugin) to the console.

‎src/atomvm_dialyzer_provider.erl‎

Lines changed: 336 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,336 @@
1+
%% Copyright (c) 2025 Uncle Grumpy <winford@object.stream>
2+
%% All rights reserved.
3+
%%
4+
%% Licensed under the Apache License, Version 2.0 (the "License");
5+
%% you may not use this file except in compliance with the License.
6+
%% You may obtain a copy of the License at
7+
%%
8+
%% http://www.apache.org/licenses/LICENSE-2.0
9+
%%
10+
%% Unless required by applicable law or agreed to in writing, software
11+
%% distributed under the License is distributed on an "AS IS" BASIS,
12+
%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
%% See the License for the specific language governing permissions and
14+
%% limitations under the License.
15+
%%
16+
%%
17+
%% SPDX-License-Identifier: Apache-2.0 OR LGPL-2.1-or-later
18+
%%
19+
-module(atomvm_dialyzer_provider).
20+
21+
-behaviour(provider).
22+
23+
-export([init/1, do/1, format_error/1]).
24+
25+
-define(PROVIDER, dialyzer).
26+
-define(DEPS, [{default, compile}, {default, app_discovery}]).
27+
-define(OPTS, [
28+
%% TODO: implement incremental PLTs
29+
{base_plt_location, undefined, "base-plt-location", string,
30+
"The location of base PLT file, defaults to $HOME/.cache/rebar3"},
31+
{plt_location, undefined, "plt-location", string,
32+
"The location of the PLT file, defaults to the profile's base directory"},
33+
{plt_prefix, undefined, "plt-prefix", string,
34+
"The prefix to the PLT file, defaults to application name"},
35+
{atomvm_root, undefined, "atomvm_root", string,
36+
"Base path to AtomVM install directory (i.e. /opt/atomvm), only needed if the \"atomvm\" launcher script is not in PATH."}
37+
%% TODO: implement statistics
38+
%{statistics, undefined, "statistics", boolean, "Print information about the progress of execution. Default: false" }]
39+
]).
40+
-define(LIBS, [alisp, eavmlib, estdlib, etest]).
41+
42+
%% ===================================================================
43+
%% Public API
44+
%% ===================================================================
45+
%%
46+
%% provider implementation
47+
%%
48+
-spec init(rebar_state:t()) -> {ok, rebar_state:t()}.
49+
init(State) ->
50+
Provider = providers:create([
51+
% The atomvm namespace
52+
{namespace, atomvm},
53+
% The 'user friendly' name of the task
54+
{name, ?PROVIDER},
55+
% The module implementation of the task
56+
{module, ?MODULE},
57+
% The task can be run by the user, always true
58+
{bare, true},
59+
% The list of dependencies
60+
{deps, ?DEPS},
61+
% How to use the plugin
62+
{example, "rebar3 atomvm dialyzer"},
63+
% list of options understood by the plugin
64+
{opts, ?OPTS},
65+
{short_desc, "Dialyze an AtomVM application"},
66+
{desc,
67+
"~n"
68+
"Use this plugin to check an AtomVM application for type discrepancies.~n"
69+
"This plugin depends on an installed atomvm launcher in the users PATH.~n"}
70+
]),
71+
{ok, rebar_state:add_provider(State, Provider)}.
72+
73+
-spec do(rebar_state:t()) -> {ok, rebar_state:t()} | {error, string()}.
74+
do(State) ->
75+
% no plugins in analysis
76+
rebar_paths:unset_paths([plugins], State),
77+
rebar_paths:set_paths([deps], State),
78+
try
79+
Config = get_opts(State),
80+
rebar_api:debug("Effective opts for ~p: ~p", [?PROVIDER, Config]),
81+
ok = do_dialize(Config, State),
82+
{ok, State}
83+
catch
84+
C:E:S ->
85+
rebar_api:error(
86+
"An error occurred in the ~p task. Class=~p Error=~p Stacktrace=~p~n", [
87+
?PROVIDER, C, E, S
88+
]
89+
),
90+
{error, E}
91+
end.
92+
93+
-spec format_error(any()) -> iolist().
94+
format_error(Reason) ->
95+
io_lib:format("~p", [Reason]).
96+
97+
%% ===================================================================
98+
%% Internal functions
99+
%% ===================================================================
100+
101+
%% @private
102+
-spec get_opts(State :: rebar_state:t()) -> map().
103+
get_opts(State) ->
104+
{ParsedArgs, _} = rebar_state:command_parsed_args(State),
105+
RebarOpts = atomvm_rebar3_plugin:get_atomvm_rebar_provider_config(State, ?PROVIDER),
106+
ParsedOpts = atomvm_rebar3_plugin:proplist_to_map(ParsedArgs),
107+
maps:merge(RebarOpts, ParsedOpts).
108+
109+
%% @private
110+
-spec print_warnings(Warnings :: [any(), ...]) -> ok.
111+
print_warnings(Warnings) ->
112+
lists:foreach(
113+
fun(Warning) ->
114+
io:format("~s", [dialyzer:format_warning(Warning)])
115+
end,
116+
Warnings
117+
),
118+
ok.
119+
120+
%% @private
121+
do_dialize(Config, State) ->
122+
%% check base_plt exists and is up to date
123+
BasePLT = base_plt_absname(Config),
124+
case dialyzer:plt_info(BasePLT) of
125+
{ok, _} ->
126+
check_base_plt(Config);
127+
_ ->
128+
do_build_base_plt(Config)
129+
end,
130+
131+
%% dialyze sources
132+
PLT = plt_absolute_name(State),
133+
case dialyzer:plt_info(PLT) of
134+
{ok, _} ->
135+
check_app_plt(Config, State);
136+
_ ->
137+
do_build_plt(Config, State)
138+
end,
139+
AppBEAMs = get_app_beam_abspath(State),
140+
rebar_api:info("Analyzing application with dialyzer...", []),
141+
try
142+
dialyzer:run([
143+
{analysis_type, succ_typings}, {files_rec, [AppBEAMs]}, {plts, [PLT, BasePLT]}
144+
])
145+
of
146+
[] ->
147+
rebar_api:info("No problems found by dialyzer.~n", []),
148+
ok;
149+
Problems ->
150+
print_warnings(Problems)
151+
catch
152+
throw:{dialyzer_error, Reason} ->
153+
rebar_api:error("Dialyzer failed! reason: ~p.~n", [Reason])
154+
end,
155+
ok.
156+
157+
% @private
158+
check_base_plt(Config) ->
159+
rebar_api:info("Checking AtomVM base PLT...", []),
160+
PLT = base_plt_absname(Config),
161+
BEAMdir = get_base_beam_path(Config),
162+
try
163+
dialyzer:run([
164+
{analysis_type, plt_check}, {plts, [PLT]}, {output_plt, PLT}, {files_rec, BEAMdir}
165+
])
166+
of
167+
[] ->
168+
ok;
169+
_ ->
170+
do_build_base_plt(Config)
171+
catch
172+
throw:{dialyzer_error, _} ->
173+
do_build_base_plt(Config)
174+
end,
175+
ok.
176+
177+
% @private
178+
base_plt_absname(Config) ->
179+
Home =
180+
case os:getenv("HOME") of
181+
false ->
182+
rebar_api:error("Unable to locate users home directory");
183+
Path ->
184+
string:trim(Path)
185+
end,
186+
Base = maps:get(base_plt_location, Config, filename:join(Home, ".cache/rebar3")),
187+
[Version, _] = string:split(string:trim(os:cmd("atomvm -version")), "+"),
188+
BasePLT = filename:absname_join(filename:absname(Base), "AtomVM-" ++ Version ++ ".plt"),
189+
rebar_api:debug("Base PLT file: ~p", [BasePLT]),
190+
string:trim(BasePLT).
191+
192+
% @private
193+
do_build_base_plt(Config) ->
194+
rebar_api:info("Building AtomVM base PLT...", []),
195+
%% build plt
196+
BEAMdir = get_base_beam_path(Config),
197+
PLT = base_plt_absname(Config),
198+
try
199+
dialyzer:run([
200+
{analysis_type, plt_build}, {init_plt, PLT}, {output_plt, PLT}, {files_rec, BEAMdir}
201+
])
202+
of
203+
[] ->
204+
ok;
205+
Failure ->
206+
print_warnings(Failure),
207+
rebar_api:error("Failed to create project plt!~n")
208+
catch
209+
throw:{dialyzer_error, Error} ->
210+
rebar_api:error("Failed to crete plt, error:~p~n", [Error])
211+
end,
212+
ok.
213+
214+
% @private
215+
check_app_plt(Config, State) ->
216+
rebar_api:info("Checking application PLT...", []),
217+
PLT = plt_absolute_name(State),
218+
try dialyzer:run([{analysis_type, plt_check}, {plts, [PLT]}]) of
219+
_ ->
220+
ok
221+
catch
222+
throw:{dialyzer_error, _} ->
223+
do_build_plt(Config, State)
224+
end,
225+
ok.
226+
227+
% @private
228+
do_build_plt(Config, State) ->
229+
rebar_api:info("Building application PLT...", []),
230+
%% build plt
231+
BEAMdir = string:trim(get_app_beam_abspath(State)),
232+
PLT = string:trim(plt_absolute_name(State)),
233+
BasePLT = base_plt_absname(Config),
234+
try
235+
dialyzer:run([
236+
{analysis_type, plt_build},
237+
{init_plt, PLT},
238+
{plts, [BasePLT]},
239+
{output_plt, PLT},
240+
{files_rec, [BEAMdir]}
241+
])
242+
of
243+
[] ->
244+
ok;
245+
Failure ->
246+
print_warnings(Failure),
247+
rebar_api:error("Failed to create project plt!~n")
248+
catch
249+
throw:{dialyzer_error, Error} ->
250+
rebar_api:error("Failed to crete plt, error:~p~n", [Error])
251+
end,
252+
ok.
253+
254+
%% @private
255+
plt_absolute_name(State) ->
256+
{App, Path} = app_profile_abs_dir(State),
257+
ProjectPLT = filename:absname_join(Path, App ++ ".plt"),
258+
rebar_api:debug("Project plt: ~p~n", [ProjectPLT]),
259+
string:trim(ProjectPLT).
260+
261+
%% @private
262+
get_base_beam_path(Config) ->
263+
Path =
264+
case maps:get(atomvm_root, Config, []) of
265+
[] ->
266+
default_base_beam_path();
267+
Base ->
268+
get_base_beam_path_list(filename:absname(Base))
269+
end,
270+
rebar_api:debug("AtomVM beam PATH: ~p", [Path]),
271+
Path.
272+
273+
%% @private
274+
get_app_beam_abspath(State) ->
275+
{App, WorkDir} = app_profile_abs_dir(State),
276+
BEAMdir = filename:absname_join(WorkDir, "lib/" ++ App ++ "/ebin"),
277+
rebar_api:debug("App beam path for plt: ~p", [BEAMdir]),
278+
BEAMdir.
279+
280+
%% @private
281+
atomvm_install_path() ->
282+
BinPath =
283+
case os:find_executable("atomvm") of
284+
false ->
285+
rebar_api:error("Path to AtomVM installation not found!");
286+
AtomVM ->
287+
AtomVM
288+
end,
289+
[Base, _] = string:split(BinPath, "bin"),
290+
filename:join(filename:absname(Base), "lib/atomvm").
291+
292+
%% @private
293+
default_base_beam_path() ->
294+
AVMpath = atomvm_install_path(),
295+
get_base_beam_path_list(AVMpath).
296+
297+
%% @private
298+
get_base_beam_path_list(Base) ->
299+
Libs =
300+
case [filelib:wildcard(Base ++ "/lib/" ++ atom_to_list(Lib) ++ "*/ebin") || Lib <- ?LIBS] of
301+
[] ->
302+
[filename:join(Base, atom_to_list(Lib2) ++ "/src/beams") || Lib2 <- ?LIBS];
303+
Paths ->
304+
Paths
305+
end,
306+
rebar_api:debug("AtomVM libraries to add to plt: ~p~n", [Libs]),
307+
case Libs of
308+
[] ->
309+
rebar_api:error("Unable to locate AtomVM beams in path"),
310+
{error, no_beams_found};
311+
Ebins ->
312+
Ebins
313+
end.
314+
315+
% @private
316+
app_profile_abs_dir(State) ->
317+
Profile =
318+
case rebar_state:current_profiles(State) of
319+
[Prof0 | _] ->
320+
Prof0;
321+
Prof1 when is_atom(Prof1) ->
322+
Prof1;
323+
Arg ->
324+
rebar_api:error("Unable to determine rebar3 profile, got badarg ~p", [Arg]),
325+
{error, bad_rebar_profile}
326+
end,
327+
WorkDir = filename:absname(filename:join("_build", Profile)),
328+
ok = filelib:ensure_path(WorkDir),
329+
[App | _] =
330+
case rebar_state:current_app(State) of
331+
undefined ->
332+
rebar_state:project_apps(State);
333+
AppInfo ->
334+
[AppInfo]
335+
end,
336+
{binary_to_list(rebar_app_info:name(App)), WorkDir}.

0 commit comments

Comments
 (0)