Open neoaggelos opened 2 years ago
This comment intends to serve as a reference of how map expressions and patterns match to c_map
and c_map_pair
nodes in the AST tree.
eval_expr
)% erlang map expression
- spec myfunc(float()) -> map().
myfunc(A) ->
#{A => value}.
The #{A => value}
expression matches the following AST:
{c_map,
[_Annotations], % annotations
{c_literal, [_As], #{}}, % operator that introduces the map, always `#{}`
[{c_map_pair, % list of key-value pairs
[_Annotations],
{c_literal, [], assoc}, % '=>' maps to 'assoc'
{c_var, ....}, % key expression
{c_literal, [], value}}], % value expression
false, % whether this map is a pattern (false for expressions)
}
eval_expr
c_map_pair
), evaluate symbolic and concrete values for the key and the value of the map pair separately (by recursively calling eval_expr
on each, then return mk_result({symbolic.key, symbolic.value}, {concrete.key, concrete.value})
c_map
), iterate over all map pairs, then return mk_result(maps:from_list(symbolic_keyvalue_pairs), maps:from_list(concrete_keyvalue_pairs)
#{}
, the map pair operator is not assoc
etc), mainly to protect our future selves.pattern_match
)-spec myfunc(map()) -> float().
myfunc(A) ->
case A of
#{ mkey := X } = A -> X;
_ -> 0
end.
The #{ mkey := X } = A
pattern matches the following AST (when A is bound):
{c_clause,
[Annotations],
[{c_map,
[Annotations],
{c_literal, [Annotations], #{}}, % the operator that introduces the map, always `#{}`
[{c_map_pair, % list of key-value pairs
[Annotations],
{c_literal, [], exact}, % ':=' maps to 'exact'
{c_literal, [Annotations], mkey}, % key; must be literal or a bound variable
{c_var, ...}}], % value; can be literal or variable
true} % this map is a pattern
],
....
}
#{key1 := Y, key2 => value}
syntax is not allowed by Erlang, #{key1 := Y, key2 := value}
should be used instead -> this can be a rule to disallow assoc
in map pairs when map is a pattern (and vice versa). #{Z := value} = #{key => value}
cannot be used to bind Z.pattern_match
:(Rough idea) The map keys in the pattern are always bound, so call match_pattern
for each map_pair_value
with the value in maps:get(Map, map_pair_key)
Support for generic map syntax (evaluate expressions and perform pattern matching) is implemented in https://github.com/cuter-testing/cuter/pull/185, along with test coverage. The PR contains further details, but in general the implementation proposed in this issue was followed.
Support for parsing specs including map types is implemented in #184, along with test coverage.
I am having quite a lot of trouble adding support for the maps standard library. Further, the maps
library is quite extensive, and quite a lot of the functions are built-ins that cannot be implemented in Erlang code (e.g. maps:iter
, maps:next
, ...).
As reference, I've been trying to add support for the ones where implementing in user-space code is possible, for example maps:from_list
. However, I keep bumping into issues stemming from the handling of symbolic values within cuter. It is not straightforward to me how to best handle this. Work is being done in https://github.com/neoaggelos/cuter/compare/map-eval-expr...neoaggelos:maps-from-list-problematic, which is based on top of #185.
The diff above contains a new test case using maps:from_list
, which fails. The debugging statements have been added to showcase the issue:
Included here for clarity, the test case is:
{
"module": "map",
"function": "fromlist",
"args": "[10,11]",
"depth": "30",
"errors": true,
"arity": 2,
"nondeterministic": true,
"xopts": "--disable-pmatch",
"solutions": [
"$2 == 0"
],
"skip": false
}
and the function definition is
-spec fromlist(atom(), integer()) -> float().
fromlist(X, Y) ->
Z = maps:from_list([{X, Y}]),
10 / maps:get(X, Z).
(venv) ubuntu@erlang:~/cuter$ make ftest no=111
ERLC src/cuter_symbolic.erl
ERLC test/ftest/src/map.erl
[Test #111]
/home/ubuntu/cuter/cuter map fromlist '[10,11]' -d 30 -p 2 -s 32 -pa /home/ubuntu/cuter/test/ftest/ebin --disable-pmatch -m --sorted-errors
map:fromlist(10, 11)
xxxx
OUTPUT MISMATCH
=================================================================
Testing map:fromlist/2 ...
*******************************
MAKE TUPLE
-- CONCRETE VALUE {10,11}
-- SYMBOLIC VALUES [{'__s',"0.1369584167.920125444.32051"},
{'__s',"0.1369584167.920125444.32052"}]
-- NEW SYMBOLIC VALUE {'__s',"0.1369584167.920125441.32302"}
*******************************
BREAK SYMBOLIC LIST/TUPLE
-- SYMBOLIC VALUE {'__s',"0.1369584167.920125444.32107"}
-- NEW SYMBOLIC VALUES [{'__s',"0.1369584167.920125444.32114"},
{'__s',"0.1369584167.920125444.32115"}]
*******************************
MATCH ATTEMPT
-- PATTERN {c_var,[938,{file,"src/cuter_erlang.erl"}],'Key'}
-- CONCRETE KEY 10
-- SYMBOLIC KEY {'__s',"0.1369584167.920125444.32051"}
-- CONCRETE VALUE #{10 => 11}
-- SYMBOLIC VALUE #{{'__s',"0.1369584167.920125444.32114"} =>
{'__s',"0.1369584167.920125444.32115"}}
-- CONCRETE ENV [{0,10},{1,#{10 => 11}},{'Key',10},{'Map',#{10 => 11}}]
-- SYMBOLIC ENV [{0,{'__s',"0.1369584167.920125444.32051"}},
{1,
#{{'__s',"0.1369584167.920125444.32114"} =>
{'__s',"0.1369584167.920125444.32115"}}},
{'Key',{'__s',"0.1369584167.920125444.32051"}},
{'Map',#{{'__s',"0.1369584167.920125444.32114"} =>
{'__s',"0.1369584167.920125444.32115"}}}]
*******************************
MAKE TUPLE
-- CONCRETE VALUE {badkey,10}
-- SYMBOLIC VALUES [badkey,{'__s',"0.1369584167.920125444.32051"}]
-- NEW SYMBOLIC VALUE {'__s',"0.1369584167.920125444.32126"}
=== Collected Metrics ===
[solver/status]
- UNSAT: 4
=== Inputs That Lead to Runtime Errors ===
#1 map:fromlist(10, 11)
I suppose the output is parsable by people familiar with cuter internals. Judging from it, it looks like creating and breaking a symbolic value in cuter does not return the original pair of symbolic values (which does make sense for cuter in general, it logs all necessary constraints for the Z3 solver to handle).
I would appreciate any pointers/help.
Summary
Add support for Erlang maps in cuter. Cuter already contains some of the required machinery needed for supporting maps, but it currently crashes when parsing code that uses maps.
TODO
This is a rough TODO of things that are required for maps support:
map()
type in specs (in progress)c_map
andc_map_pair
AST nodes in concolic execution, as well as pattern matching (ref https://github.com/erlang/otp/blob/master/lib/compiler/src/core_parse.hrl#L75-L84). This mainly revolves around extendingeval_expr/
andpattern_match/
. (in progress)maps:get
,maps:put
, ...).Notes
WIP
Some early work is in https://github.com/neoaggelos/cuter/tree/maps-support