Evaluate map expression and pattern matching

Makefile.in

@@ -110,7 +110,8 @@ FTEST_MODULES = \
 	collection \
 	funs \
 	sum \
-	reduce_search_space
+	reduce_search_space \
+	map
 
 PRIV_MODULES = \
 	cuter_io \

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.
   end.
 
 annotate_all(Trees, TagGen, InPats) ->

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
 %% ----------------------------------------------------------------------------

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).

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.

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).
+

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
         }
     ]
 }