Annotations rebased

Makefile.in

@@ -82,7 +82,11 @@ SRC_MODULES = \
 	cuter_strategy \
 	cuter_bfs_strategy \
 	cuter_metrics \
-	cuter_config
+	cuter_config \
+	cuter_spec_checker \
+	cuter_graphs \
+	cuter_maybe_error_annotation \
+	cuter_type_dependent_functions
 
 UTEST_MODULES = \
 	cuter_tests_lib \
@@ -100,7 +104,11 @@ UTEST_MODULES = \
 	types_and_specs \
 	types_and_specs2 \
 	cuter_metrics_tests \
-	cuter_config_tests
+	cuter_config_tests \
+	cuter_graphs_tests \
+	callgraph_examples \
+	examples_for_spec_conversion \
+	examples_for_spec_conversion_pair
 
 FTEST_MODULES = \
 	bitstr \

cuter

@@ -38,6 +38,7 @@ def main():
   parser.add_argument("-m", "--metrics", action='store_true', help="report collected metrics")
   parser.add_argument("--debug-keep-traces", action='store_true', help="keep execution traces for debugging")
   parser.add_argument("--debug-solver-fsm", action='store_true', help="output debug logs for the solver FSM")
+  parser.add_argument("-ps", "--prune-safe", action='store_true', help="prune safe paths and stop the execution early")
 
   # Parse the arguments
   args = parser.parse_args()
@@ -109,6 +110,8 @@ def main():
     opts.append("debug_keep_traces")
   if args.debug_solver_fsm:
     opts.append("debug_solver_fsm")
+  if args.prune_safe:
+    opts.append("prune_safe")
   strOpts = ",".join(opts)
 
   # Run CutEr

include/cuter_macros.hrl

@@ -89,6 +89,8 @@
 -define(NUM_SOLVERS, number_of_solvers).
 %% Sets the number of concurrent concolic execution processes.
 -define(NUM_POLLERS, number_of_pollers).
+%% Prune safe paths.
+-define(PRUNE_SAFE, prune_safe).
 
 -type runtime_options() :: {?Z3_TIMEOUT, pos_integer()} 
                          | ?REPORT_METRICS
@@ -104,6 +106,7 @@
                          | {?NUM_SOLVERS, pos_integer()}
                          | {?NUM_POLLERS, pos_integer()}
                          | {?WORKING_DIR, file:filename()}
+			 | ?PRUNE_SAFE
                          .
 
 %%====================================================================
@@ -156,3 +159,10 @@
 
 %% Empty tag ID
 -define(EMPTY_TAG_ID, 0).
+
+%%====================================================================
+%% Miscellaneous stored values in cuter config
+%%====================================================================
+
+%% Entry point for concolic testing
+-define(ENTRY_POINT, entry_point).

src/cuter.erl

@@ -48,7 +48,7 @@ run(M, F, As, Depth, Options) ->
   Seeds = [{M, F, As, Depth}],
   run(Seeds, Options).
 
--spec run([seed()], options()) -> erroneous_inputs().
+-spec run([seed(),...], options()) -> erroneous_inputs().
 %% Runs CutEr on multiple units.
 run(Seeds, Options) ->
   State = state_from_options_and_seeds(Options, Seeds),
@@ -90,7 +90,8 @@ run_from_file(File, Options) ->
 %% The tasks to run during the app initialization.
 init_tasks() ->
   [fun ensure_exported_entry_points/1,
-   fun compute_callgraph/1].
+   fun compute_callgraph/1,
+   fun annotate_for_possible_errors/1].
 
 -spec init(state()) -> ok | error.
 init(State) ->
@@ -131,10 +132,17 @@ compute_callgraph(State) ->
   Mfas = mfas_from_state(State),
   cuter_codeserver:calculate_callgraph(State#st.codeServer, Mfas).
 
-
 mfas_from_state(State) ->
   [{M, F, length(As)} || {M, F, As, _} <- State#st.seeds].
 
+annotate_for_possible_errors(State) ->
+  case cuter_config:fetch(?PRUNE_SAFE) of
+    {ok, true} ->
+      cuter_codeserver:annotate_for_possible_errors(State#st.codeServer);
+    _ ->
+      ok
+  end.
+
 %% ----------------------------------------------------------------------------
 %% Manage the concolic executions
 %% ----------------------------------------------------------------------------
@@ -146,8 +154,7 @@ start(State) ->
 -spec start([seed()], state()) -> state().
 start([], State) ->
   State;
-start([{M, F, As, Depth}|Seeds], State) ->
-  CodeServer = State#st.codeServer,
+start([{M, F, As, Depth}|Seeds], State) ->  CodeServer = State#st.codeServer,
   Scheduler = State#st.scheduler,
   Errors = start_one(M, F, As, Depth, CodeServer, Scheduler),
   NewErrors = [{{M, F, length(As)}, Errors}|State#st.errors],
@@ -242,19 +249,19 @@ stop(State) ->
 %% Generate the system state
 %% ----------------------------------------------------------------------------
 
--spec state_from_options_and_seeds(options(), [seed()]) -> state().
+-spec state_from_options_and_seeds(options(), [seed(),...]) -> state().
 state_from_options_and_seeds(Options, Seeds) ->
   process_flag(trap_exit, true),
   error_logger:tty(false),  %% disable error_logger
   ok = cuter_config:start(),
   ok = cuter_metrics:start(),
   ok = define_metrics(),
   enable_debug_config(Options),
-  enable_runtime_config(Options),
+  enable_runtime_config(Options, Seeds),
   ok = cuter_pp:start(),
   CodeServer = cuter_codeserver:start(),
   SchedPid = cuter_scheduler:start(?DEFAULT_DEPTH, CodeServer),
-  #st{ codeServer = CodeServer, scheduler = SchedPid, seeds = Seeds }.
+  #st{codeServer = CodeServer, scheduler = SchedPid, seeds = Seeds}.
 
 define_metrics() ->
   define_distribution_metrics().
@@ -268,8 +275,8 @@ enable_debug_config(Options) ->
   cuter_config:store(?DEBUG_SMT, proplists:get_bool(?DEBUG_SMT, Options)),
   cuter_config:store(?DEBUG_SOLVER_FSM, proplists:get_bool(?DEBUG_SOLVER_FSM, Options)).
 
--spec enable_runtime_config(options()) -> ok.
-enable_runtime_config(Options) ->
+-spec enable_runtime_config(options(), [seed(),...]) -> ok.
+enable_runtime_config(Options, [{M, F, I, _D}|_]) ->
   {ok, CWD} = file:get_cwd(),
   cuter_config:store(?WORKING_DIR,
                      cuter_lib:get_tmp_dir(proplists:get_value(?WORKING_DIR, Options, CWD))),
@@ -287,7 +294,9 @@ enable_runtime_config(Options) ->
   cuter_config:store(?SORTED_ERRORS, proplists:get_bool(?SORTED_ERRORS, Options)),
   cuter_config:store(?WHITELISTED_MFAS, whitelisted_mfas(Options)),
   cuter_config:store(?NUM_SOLVERS, proplists:get_value(?NUM_SOLVERS, Options, ?ONE)),
-  cuter_config:store(?NUM_POLLERS, proplists:get_value(?NUM_POLLERS, Options, ?ONE)).
+  cuter_config:store(?NUM_POLLERS, proplists:get_value(?NUM_POLLERS, Options, ?ONE)),
+  cuter_config:store(?PRUNE_SAFE, proplists:get_bool(?PRUNE_SAFE, Options)),
+  cuter_config:store(?ENTRY_POINT, {M, F, length(I)}).
 
 verbosity_level(Options) ->
   Default = cuter_pp:default_reporting_level(),

src/cuter_cerl.erl

@@ -12,7 +12,7 @@
          node_types_conditions/0, node_types_conditions_nocomp/0,
          node_types_paths/0, node_types_paths_nocomp/0]).
 %% kfun API.
--export([kfun/2, kfun_code/1, kfun_is_exported/1]).
+-export([kfun/2, kfun_code/1, kfun_is_exported/1, kfun_update_code/2]).
 %% kmodule API.
 -export([kmodule_spec_forms/1, kmodule_record_forms/1, kmodule_type_forms/1, kmodule_exported_types/1, kmodule_name/1, destroy_kmodule/1, kmodule/3, kmodule_kfun/2, kmodule_mfa_spec/2,
   kmodule_specs/1, kmodule_types/1, kmodule_update_kfun/3, kmodule_mfas_with_kfuns/1,
@@ -25,13 +25,12 @@
 
 -include("include/cuter_macros.hrl").
 
--export_type([compile_error/0, cerl_attr_spec/0, cerl_attr_type/0,
+-export_type([compile_error/0, cerl_spec_form/0, cerl_attr_type/0,
 	      cerl_bounded_func/0, cerl_constraint/0, cerl_func/0,
-	      cerl_recdef/0, cerl_record_field/0, cerl_spec/0,
+	      cerl_record_field/0, cerl_spec/0,
 	      cerl_spec_func/0, cerl_type/0, cerl_typedef/0,
 	      cerl_type_record_field/0, node_types/0,
-	      tagID/0, tag/0, tag_generator/0, visited_tags/0,
-	      spec_info/0]).
+	      tagID/0, tag/0, tag_generator/0, visited_tags/0]).
 
 -export_type([extracted_record_form/0, extracted_type_form/0]).
 
@@ -70,17 +69,15 @@
 -type name() :: atom().
 -type fa() :: {name(), arity()}.
 -type cerl_attr_type() :: cerl_recdef() | cerl_typedef().
--type cerl_attr_spec() :: cerl_specdef().
 
--type cerl_recdef() :: {name(), [cerl_record_field()]} % for OTP 19.x
-                     | {{'record', name()}, [cerl_record_field()], []}. % for OTP 18.x or earlier
+-type cerl_recdef() :: {name(), [cerl_record_field()]}.
 -type cerl_record_field() :: cerl_untyped_record_field() | cerl_typed_record_field().
 -type cerl_untyped_record_field() :: {'record_field', lineno(), {'atom', lineno(), name()}}
                                    | {'record_field', lineno(), {'atom', lineno(), name()}, any()}.
 -type cerl_typed_record_field() :: {'typed_record_field', cerl_untyped_record_field(), cerl_type()}.
 -type cerl_typedef() :: {name(), cerl_type(), [cerl_type_var()]}.
 
--type cerl_specdef() :: {fa(), cerl_spec()}.
+-type cerl_spec_form() :: {fa(), cerl_spec()}.
 -type cerl_spec() :: [cerl_spec_func(), ...].
 -type cerl_spec_func() :: cerl_func() | cerl_bounded_func().
 
@@ -273,7 +270,7 @@ is_mfa({M, F, A}) when is_atom(M), is_atom(F), is_integer(A), A >= 0 -> true;
 is_mfa(_Mfa) -> false.
 
 %% Returns the unprocessed specs of a kmodule (as forms).
--spec kmodule_spec_forms(kmodule()) -> [cerl:cerl()].
+-spec kmodule_spec_forms(kmodule()) -> [cerl_spec_form()].
 kmodule_spec_forms(Kmodule) ->
   [{spec_forms, SpecsForms}] = ets:lookup(Kmodule, spec_forms),
   SpecsForms.
@@ -310,6 +307,9 @@ kfun_is_exported(#{is_exported := IsExported}) -> IsExported.
 -spec kfun_code(kfun()) -> code().
 kfun_code(#{code := Code}) -> Code.
 
+-spec kfun_update_code(kfun(), code()) -> kfun().
+kfun_update_code(Fun, Code) -> Fun#{code=>Code}.
+
 %% ===================================================================
 %% Internal functions
 %% ===================================================================
@@ -320,8 +320,8 @@ extract_exports(M, AST) ->
   [mfa_from_var(M, E) || E <- Exports].
 
 extract_exported_types(Mod, Attrs) ->
-  Filtered = [T || {#c_literal{val = export_type}, #c_literal{val = T}} <- Attrs],
-  sets:from_list(lists:append([{Mod, Tname, Tarity} || {Tname, Tarity} <- Filtered])).
+  ExpTypes = lists:append([Ts || {#c_literal{val = export_type}, #c_literal{val = Ts}} <- Attrs]),
+  sets:from_list([{Mod, Tname, Tarity} || {Tname, Tarity} <- ExpTypes]).
 
 -spec process_fundef({cerl:c_var(), code()}, [mfa()], module(), tag_generator()) -> {mfa(), kfun()}.
 process_fundef({FunVar, Def}, Exports, M, TagGen) ->
@@ -375,8 +375,6 @@ get_abstract_code(Mod, Beam) ->
     _ -> throw(cuter_pp:abstract_code_missing(Mod))
   end.
 
--type spec_info() :: cerl_attr_spec().
-
 %% Extracts the record definitions (as forms) from the annotations of a module.
 %% The relevant annotations have the following structure in OTP 19.x and newer:
 %%     {#c_atom{val=record}, #c_literal{val=[{Name, Fields}]}}

src/cuter_codeserver.erl

@@ -10,6 +10,8 @@
          visit_tag/2, calculate_callgraph/2,
          %% Work with module cache
          merge_dumped_cached_modules/2, modules_of_dumped_cache/1,
+	 %% Code annotations
+	 annotate_for_possible_errors/1,
          %% Access logs
          cachedMods_of_logs/1, visitedTags_of_logs/1, tagsAddedNo_of_logs/1,
          unsupportedMfas_of_logs/1, loadedMods_of_logs/1]).
@@ -19,6 +21,8 @@
 %% Counter of branches & Tag generator.
 -export([get_branch_counter/0, init_branch_counter/0, generate_tag/0]).
 
+-export([convert_specs/1]).
+
 -include("include/cuter_macros.hrl").
 
 -export_type([cached_modules/0, codeserver/0, counter/0, logs/0]).
@@ -27,7 +31,7 @@
 -define(BRANCH_COUNTER_PREFIX, '__branch_count').
 
 -type counter() :: non_neg_integer().
--type cached_module_data() :: any().
+-type cached_module_data() :: any().   % XXX: refine
 -type cached_modules() :: dict:dict(module(), cached_module_data()).
 
 -type cache() :: ets:tid().
@@ -46,20 +50,20 @@
 }).
 -type logs() :: #logs{}.
 
-%% Internal type declarations
+%% Internal type declarations.
 -type load_reply() :: {ok, cuter_cerl:kmodule()} | cuter_cerl:compile_error() | {error, (preloaded | cover_compiled | non_existing)}.
 -type spec_reply() :: {ok, cuter_types:erl_spec()} | error.
 -type from() :: {pid(), reference()}.
 
-%% Finding the remote dependencies of a spec.
+%% Remote dependencies of a spec.
 -type remote_type()     :: {cuter:mod(), atom(), byte()}.
 -type module_deps()     :: ordsets:ordset(cuter:mod()).
 -type visited_remotes() :: ordsets:ordset(remote_type()).
 
 -type codeserver() :: pid().
 -type codeserver_args() :: #{}.
 
-%% Server's state
+%% Server's state.
 -record(st, {
   %% Acts as a reference table for looking up the ETS table that holds a module's extracted code.
   %% It stores tuples {Module :: module(), ModuleDb :: ets:tid()}.
@@ -137,11 +141,20 @@ get_whitelist(CodeServer) ->
 calculate_callgraph(CodeServer, Mfas) ->
   gen_server:call(CodeServer, {calculate_callgraph, Mfas}).
 
+-spec convert_specs(codeserver()) -> ok.
+convert_specs(CodeServer) ->
+  gen_server:call(CodeServer, convert_specs).
+
 %% Gets the feasible tags.
 -spec get_feasible_tags(codeserver(), cuter_cerl:node_types()) -> cuter_cerl:visited_tags().
 get_feasible_tags(CodeServer, NodeTypes) ->
   gen_server:call(CodeServer, {get_feasible_tags, NodeTypes}).
 
+%% Annotates the code for possible errors.
+-spec annotate_for_possible_errors(codeserver()) -> ok.
+annotate_for_possible_errors(CodeServer) ->
+  gen_server:call(CodeServer, annotate_for_possible_errors).
+
 %% ----------------------------------------------------------------------------
 %% gen_server callbacks (Server Implementation)
 %% ----------------------------------------------------------------------------
@@ -182,6 +195,7 @@ handle_info(_Msg, State) ->
                ; (get_whitelist, from(), state()) -> {reply, cuter_mock:whitelist(), state()}
                ; ({get_feasible_tags, cuter_cerl:node_types()}, from(), state()) -> {reply, cuter_cerl:visited_tags(), state()}
                ; ({calculate_callgraph, [mfa()]}, from(), state()) -> {reply, ok, state()}
+	             ; (annotate_for_possible_errors, from(), state()) -> {reply, ok, state()}
                .
 handle_call({load, M}, _From, State) ->
   {reply, try_load(M, State), State};
@@ -231,7 +245,28 @@ handle_call({calculate_callgraph, Mfas}, _From, State=#st{whitelist = Whitelist}
                 end,
       cuter_callgraph:foreachModule(LoadFn, Callgraph),
       {reply, ok, State#st{callgraph = Callgraph}}
-  end.
+  end;
+handle_call(annotate_for_possible_errors, _From, State=#st{db = Db}) ->
+  Fn = fun({_M, Kmodule}, KfunAcc) ->
+      KfunMappings = cuter_cerl:kmodule_mfas_with_kfuns(Kmodule),
+      TrivialMergeFn = fun(_K, V1, _V2) -> V1 end,
+      dict:merge(TrivialMergeFn, KfunAcc, KfunMappings)
+    end,
+  Fn2 = fun({_M, Kmodule}, Acc) ->
+	    [Kmodule|Acc]
+	end,
+  Kmodules = ets:foldl(Fn2, [], Db),
+  {ok, EntryPoint} = cuter_config:fetch(?ENTRY_POINT),
+  MfasToKfuns = ets:foldl(Fn, dict:new(), Db),
+  MfasToSpecs = cuter_types:specs_as_erl_types(Kmodules),
+  UpdatedKfuns = cuter_maybe_error_annotation:preprocess(EntryPoint, MfasToKfuns, MfasToSpecs),
+  RFn = fun({M, F, A}, Kfun, _Acc) ->
+	   [{_M, Kmodule}] = ets:lookup(Db, M),
+	    cuter_cerl:kmodule_update_kfun(Kmodule, {M, F, A}, Kfun)
+	end,
+  dict:fold(RFn, ok, UpdatedKfuns),
+  {reply, ok, State}.
+
 
 %% gen_server callback : handle_cast/2
 -spec handle_cast(stop, state()) -> {stop, normal, state()} | {noreply, state()}
@@ -254,10 +289,10 @@ handle_cast({visit_tag, Tag}, State=#st{tags = Tags}) ->
 -spec load_all_deps_of_spec(cuter_types:stored_spec_value(), module(), cuter_cerl:kmodule(), state()) -> [cuter:mod()].
 load_all_deps_of_spec(CerlSpec, Module, Kmodule, State) ->
   LocalTypesCache = cuter_cerl:kmodule_types(Kmodule),
-  % Get the remote dependencies of the spec.
+  %% Get the remote dependencies of the spec.
   ToBeVisited = cuter_types:find_remote_deps_of_spec(CerlSpec, LocalTypesCache),
   InitDepMods = ordsets:add_element(Module, ordsets:new()),
-  % Find iteratively the dependencies of the found dependencies.
+  %% Find iteratively the dependencies of the found dependencies.
   case load_all_deps(ToBeVisited, State, ordsets:new(), InitDepMods) of
     error -> [];
     {ok, DepMods} -> DepMods
@@ -285,7 +320,7 @@ load_all_deps([Remote={M, TypeName, Arity}|Rest], State, VisitedRemotes, DepMods
               Deps = cuter_types:find_remote_deps_of_type(Type, LocalTypesCache),
               %% Queue the ones that we haven't encountered yet.
               NewRemotes = [R || R <- Deps,
-                not ordsets:is_element(R, VisitedRemotes1)],
+				 not ordsets:is_element(R, VisitedRemotes1)],
               load_all_deps(NewRemotes ++ Rest, State, VisitedRemotes1, DepMods1)
           end;
         _Msg ->