From 60155e3bb6833b29d34fc6fa0904439c43fea189 Mon Sep 17 00:00:00 2001 From: Aggelos Kolaitis Date: Mon, 20 Sep 2021 23:10:40 +0300 Subject: [PATCH 1/3] Support map expressions and patterns (183) This commit introduces support for evaluating map expressions and matching patterns containing maps. It also adds initial support for the maps:get() and maps:put() standard library functions. --- Makefile.in | 3 +- src/cuter_cerl.erl | 11 ++- src/cuter_erlang.erl | 20 +++++ src/cuter_eval.erl | 41 +++++++++- src/cuter_mock.erl | 4 + test/ftest/src/map.erl | 85 +++++++++++++++++++++ test/ftests.json | 168 +++++++++++++++++++++++++++++++++++++++++ 7 files changed, 329 insertions(+), 3 deletions(-) create mode 100644 test/ftest/src/map.erl diff --git a/Makefile.in b/Makefile.in index 1725dd05..abedf833 100644 --- a/Makefile.in +++ b/Makefile.in @@ -110,7 +110,8 @@ FTEST_MODULES = \ collection \ funs \ sum \ - reduce_search_space + reduce_search_space \ + map PRIV_MODULES = \ cuter_io \ diff --git a/src/cuter_cerl.erl b/src/cuter_cerl.erl index f668b781..ef32ea1d 100644 --- a/src/cuter_cerl.erl +++ b/src/cuter_cerl.erl @@ -411,8 +411,17 @@ annotate(Tree, TagGen, InPats) -> cerl:update_c_values(Tree, Es); var -> Tree; + map -> + Es = annotate_all(cerl:map_es(Tree), TagGen, InPats), + Arg = annotate(cerl:map_arg(Tree), TagGen, InPats), + cerl:update_c_map(Tree, Arg, Es); + map_pair -> + Op = annotate(cerl:map_pair_op(Tree), TagGen, InPats), + Key = annotate(cerl:map_pair_key(Tree), TagGen, InPats), + Value = annotate(cerl:map_pair_val(Tree), TagGen, InPats), + cerl:update_c_map_pair(Tree, Op, Key, Value); _ -> - Tree %% TODO Ignore maps (for now) and modules. + Tree %% TODO Ignore modules (for now). end. annotate_all(Trees, TagGen, InPats) -> diff --git a/src/cuter_erlang.erl b/src/cuter_erlang.erl index 48b7309f..4879173d 100644 --- a/src/cuter_erlang.erl +++ b/src/cuter_erlang.erl @@ -29,6 +29,7 @@ , '++'/2, '--'/2, reverse/2, member/2, keyfind/3 , is_binary/1, bit_size/1, byte_size/1 , 'bsl'/2, 'bsr'/2, 'bnot'/1 + , maps_get/2, ismap/1, maps_put/3 ]). %% XXX When adding type constraints for spec, the overriding funs must be ignored @@ -926,6 +927,25 @@ keyfind(Key, N, [H|T]) when is_tuple(H) -> _ -> keyfind(Key, N, T) end. +%% ---------------------------------------------------------------------------- +%% MAP OPERATIONS +%% ---------------------------------------------------------------------------- + +-spec maps_get(any(), #{ any() => any() }) -> any(). +maps_get(Key, Map) when is_map(Map) -> + case Map of + #{ Key := Val } -> Val; + _ -> error({badkey, Key}) + end. + +-spec ismap(any()) -> boolean(). +ismap(#{}) -> true; +ismap(_) -> false. + +-spec maps_put(any(), any(), #{ any() => any() }) -> #{ any() => any() }. +maps_put(Key, Val, Map) when is_map(Map) -> + Map#{Key => Val}. + %% ---------------------------------------------------------------------------- %% BINARY / BITSTRING OPERATIONS %% ---------------------------------------------------------------------------- diff --git a/src/cuter_eval.erl b/src/cuter_eval.erl index 040d39be..f80f99e4 100644 --- a/src/cuter_eval.erl +++ b/src/cuter_eval.erl @@ -842,10 +842,27 @@ eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd) -> {ok, Sv} = cuter_env:get_value(Name, Senv), mk_result(Cv, Sv); +% c_map +eval_expr({c_map, _Anno, Arg, Entries, false}, M, Cenv, Senv, Servers, Fd) -> + Entries_ev = [eval_expr({c_map_pair, A, Op, K, V}, M, Cenv, Senv, Servers, Fd) || {c_map_pair, A, Op, K, V} <- Entries], + { C_ev, S_ev } = cuter_lib:unzip_with(fun to_tuple/1, Entries_ev), + { CArg, SArg } = to_tuple(eval_expr(Arg, M, Cenv, Senv, Servers, Fd)), + mk_result(maps:merge(CArg, maps:from_list(C_ev)), maps:merge(SArg, maps:from_list(S_ev))); + +% c_map_pair +eval_expr({c_map_pair, _Anno, Op, K, V}, M, Cenv, Senv, Servers, Fd) -> + case Op of + {c_literal, _, assoc} -> ok; + {c_literal, _, exact} -> exception(error, {bad_c_map_pair_op, not_allowed, Op}); + _ -> exception(error, {bad_c_map_pair_op, unknown, Op}) + end, + { Ck, Sk } = to_tuple(eval_expr(K, M, Cenv, Senv, Servers, Fd)), + { Cv, Sv } = to_tuple(eval_expr(V, M, Cenv, Senv, Servers, Fd)), + mk_result({Ck, Cv}, {Sk, Sv}); + eval_expr(Cerl, _M, _Cenv, _Senv, _Servers, _Fd) -> exception(error, {unknown_cerl, Cerl}). - %% -------------------------------------------------------- %% Evaluates a BIF call %% -------------------------------------------------------- @@ -1203,6 +1220,28 @@ pattern_match({c_alias, _Anno, Var, Pat}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, S {true, {Cs, Ss}} end; +%% Map pattern. +%% Evaluate symbolic and concrete value of key, and attempt to match with concrete and symbolic value. +pattern_match({c_map, As, Arg, [{c_map_pair, _Anno, _, Key, Val}|Entries], true}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) -> + { M, Cenv, Senv } = BitInfo, + { CKey, SKey } = to_tuple(eval_expr(Key, M, Cenv, Senv, Servers, Fd)), + case { Cv, Sv } of + % TODO: symbolic matching for maps + { #{ CKey := CVal }, #{ SKey := SVal } } -> + case pattern_match(Val, BitInfo, Mode, CVal, SVal, CMaps, SMaps, Servers, Fd) of + {true, {CMs, SMs}} -> pattern_match({c_map, As, Arg, Entries, true}, BitInfo, Mode, Cv, Sv, CMs, SMs, Servers, Fd); + false -> false + end; + _ -> false + end; +pattern_match({c_map, _Anno, _Arg, [], true}, _BitInfo, _Mode, Cv, _Sv, CMaps, SMaps, _Servers, _Fd) -> + % Empty map pattern matches any map + % TODO: symbolic matching for maps + case is_map(Cv) of + true -> {true, {CMaps, SMaps}}; + false -> false + end; + %% Binary pattern pattern_match({c_binary, Anno, Segments}, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd) -> bit_pattern_match(Anno, Segments, BitInfo, Mode, Cv, Sv, CMaps, SMaps, Servers, Fd). diff --git a/src/cuter_mock.erl b/src/cuter_mock.erl index cb497d2d..7e796e5b 100644 --- a/src/cuter_mock.erl +++ b/src/cuter_mock.erl @@ -78,6 +78,10 @@ override_mfa({erlang, trunc, 1}) -> {ok, {cuter_erlang, trunc, 1}}; override_mfa({lists, member, 2}) -> {ok, {cuter_erlang, member, 2}}; override_mfa({lists, reverse, 2}) -> {ok, {cuter_erlang, reverse, 2}}; override_mfa({lists, keyfind, 3}) -> {ok, {cuter_erlang, keyfind, 3}}; +%% Module maps. +override_mfa({erlang, is_map, 1}) -> {ok, {cuter_erlang, ismap, 1}}; +override_mfa({maps, get, 2}) -> {ok, {cuter_erlang, maps_get, 2}}; +override_mfa({maps, put, 3}) -> {ok, {cuter_erlang, maps_put, 3}}; %% Module math. override_mfa({math, pi, 0}) -> {ok, {math, pi, 0}}; %% The rest MFAs are not overriden. diff --git a/test/ftest/src/map.erl b/test/ftest/src/map.erl new file mode 100644 index 00000000..c076df98 --- /dev/null +++ b/test/ftest/src/map.erl @@ -0,0 +1,85 @@ +-module(map). +-export([ simple/1, simple_squared/1 + , simple_extend/1, extend_empty/1 + , simple_match/1, match_cases/1, match_many/2 + , match_lit/1, match_var/1, match_embed/1 + , maps_get/1, maps_put/1 + ]). + +-spec simple(integer()) -> #{value => float()}. +simple(X) -> + #{ value => 10 / (X + 4) }. + +-spec simple_squared(integer()) -> #{value => float()}. +simple_squared(X) -> + #{ value => 10 / (X*X - 4) }. + +-spec simple_extend(integer()) -> #{value => float()}. +simple_extend(X) -> + A = #{ a => X }, + A#{ value => 10 / (X*X - 4) }. + +-spec extend_empty(integer()) -> #{value => float()}. +extend_empty(X) -> + A = #{}, + A#{ value => 10 / (X*X - 4) }. + +-spec simple_match(integer()) -> float(). +simple_match(X) -> + #{ var := A } = #{ var => X + 2 }, + 10 / A. + +-spec match_cases(integer()) -> float(). +match_cases(X) -> + M = case X > 50 of + true -> #{var1 => X}; + false -> #{var2 => X} + end, + case M of + #{ var1 := A } -> 1 / (60 - A); + #{ var2 := A } -> 2 / (40 - A) + end. + +-spec match_many(integer(), integer()) -> float(). +match_many(X, Y) -> + case #{ a => X+2, b => Y+4, key => value } of + #{ a := A, b := B } -> 10 / (A + B); + _ -> 0 + end. + +-spec match_lit(integer()) -> float(). +match_lit(X) -> + case #{ val => X} of + #{ val := 100 } -> error(error); + _ -> ok + end. + +-spec match_var(integer()) -> float(). +match_var(X) -> + Y = 200, + case #{ val => X + 1 } of + #{ val := Y } -> error(error); + _ -> ok + end. + +-spec match_embed(integer()) -> float(). +match_embed(X) -> + Y = b, + M = #{ a => #{ b => X + 20 } }, + case M of + #{ a := #{ Y := A } } -> 10 / A; + _ -> 0 + end. + +-spec maps_get(integer()) -> float(). +maps_get(X) -> + M = #{var => X + 2}, + 10 / maps:get(var, M). + +-spec maps_put(integer()) -> float(). +maps_put(X) -> + M = #{}, + Z = maps:put(value, X, M), + Y = maps:get(value, Z), + 10 / (Y+1). + diff --git a/test/ftests.json b/test/ftests.json index aeca4bda..fafa3c21 100644 --- a/test/ftests.json +++ b/test/ftests.json @@ -1251,6 +1251,174 @@ "UNSAT": 6 }, "skip": false + }, + { + "module": "map", + "function": "simple", + "args": "[1]", + "depth": "20", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -4" + ], + "skip": false + }, + { + "module": "map", + "function": "simple_squared", + "args": "[10]", + "depth": "40", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -2 or $1 == 2" + ], + "skip": false + }, + { + "module": "map", + "function": "simple_extend", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch --suppress-unsupported", + "solutions": [ + "$1 == -2 or $1 == 2" + ], + "skip": false + }, + { + "module": "map", + "function": "extend_empty", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -2 or $1 == 2" + ], + "skip": false + }, + { + "module": "map", + "function": "simple_match", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -2" + ], + "skip": false + }, + { + "module": "map", + "function": "match_many", + "args": "[10,20]", + "depth": "30", + "errors": true, + "arity": 2, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == 0 and $2 == -6" + ], + "skip": false + }, + { + "module": "map", + "function": "match_cases", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == 60 or $1 == 40" + ], + "skip": false + }, + { + "module": "map", + "function": "match_lit", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == 100" + ], + "skip": false + }, + { + "module": "map", + "function": "match_var", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == 199" + ], + "skip": false + }, + { + "module": "map", + "function": "match_embed", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -20" + ], + "skip": false + }, + { + "module": "map", + "function": "maps_get", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -2" + ], + "skip": false + }, + { + "module": "map", + "function": "maps_put", + "args": "[10]", + "depth": "30", + "errors": true, + "arity": 1, + "nondeterministic": true, + "xopts": "--disable-pmatch", + "solutions": [ + "$1 == -1" + ], + "skip": false } ] } From bf197ba89a3f97e19dad87156d5659efa6767e8d Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 8 Feb 2022 21:02:05 +0100 Subject: [PATCH 2/3] Update cuter_cerl.erl --- src/cuter_cerl.erl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cuter_cerl.erl b/src/cuter_cerl.erl index ef32ea1d..a1dc79de 100644 --- a/src/cuter_cerl.erl +++ b/src/cuter_cerl.erl @@ -421,7 +421,7 @@ annotate(Tree, TagGen, InPats) -> Value = annotate(cerl:map_pair_val(Tree), TagGen, InPats), cerl:update_c_map_pair(Tree, Op, Key, Value); _ -> - Tree %% TODO Ignore modules (for now). + Tree %% TODO Ignore modules. end. annotate_all(Trees, TagGen, InPats) -> From fbc4ac7d6bf645957e1ff83031d180f827323b9a Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 8 Feb 2022 21:02:58 +0100 Subject: [PATCH 3/3] Update cuter_eval.erl --- src/cuter_eval.erl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cuter_eval.erl b/src/cuter_eval.erl index f80f99e4..760b6b94 100644 --- a/src/cuter_eval.erl +++ b/src/cuter_eval.erl @@ -842,14 +842,14 @@ eval_expr({c_var, _Anno, Name}, _M, Cenv, Senv, _Servers, _Fd) -> {ok, Sv} = cuter_env:get_value(Name, Senv), mk_result(Cv, Sv); -% c_map +%% c_map eval_expr({c_map, _Anno, Arg, Entries, false}, M, Cenv, Senv, Servers, Fd) -> Entries_ev = [eval_expr({c_map_pair, A, Op, K, V}, M, Cenv, Senv, Servers, Fd) || {c_map_pair, A, Op, K, V} <- Entries], { C_ev, S_ev } = cuter_lib:unzip_with(fun to_tuple/1, Entries_ev), { CArg, SArg } = to_tuple(eval_expr(Arg, M, Cenv, Senv, Servers, Fd)), mk_result(maps:merge(CArg, maps:from_list(C_ev)), maps:merge(SArg, maps:from_list(S_ev))); -% c_map_pair +%% c_map_pair eval_expr({c_map_pair, _Anno, Op, K, V}, M, Cenv, Senv, Servers, Fd) -> case Op of {c_literal, _, assoc} -> ok;