initial.c

Go to the documentation of this file.

/*
 
  $Id: initial.c 23412 2017-08-09 15:07:09Z irigoin $
 
  Copyright 1989-2016 MINES ParisTech
 
  This file is part of PIPS.
 
  PIPS is free software: you can redistribute it and/or modify it
  under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  any later version.
 
  PIPS is distributed in the hope that it will be useful, but WITHOUT ANY
  WARRANTY; without even the implied warranty of MERCHANTABILITY or
  FITNESS FOR A PARTICULAR PURPOSE.
 
  See the GNU General Public License for more details.
 
  You should have received a copy of the GNU General Public License
  along with PIPS.  If not, see <http://www.gnu.org/licenses/>.
 
*/
#ifdef HAVE_CONFIG_H
    #include "pips_config.h"
#endif
/*
 * Computation of initial transformers that allow to collect
 * global initializations of BLOCK DATA and so.
 *
 * This computation is not safe because pipsmake does not provide a real
 * link-edit. The set of modules called $ALL may contain modules which
 * are never called by the main.
 *
 * The initial precondition of each module must be filtered with respect
 * to the effects of the MAIN in order to eliminate information about
 * unused variables.
 *
 * The filtering cannot be performed at the module level because some
 * modules such as BLOCKDATA do not have any proper effects and because
 * a module can initialize a variable in a common without using it.
 *
 */
 
#include <stdio.h>
#include <string.h>
 
#include "genC.h"
 
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "effects-util.h"
 
#include "database.h"
#include "pipsdbm.h"
#include "resources.h"
 
#include "misc.h"
 
#include "effects-generic.h"
#include "effects-simple.h"
 
#include "prettyprint.h"
#include "transformer.h"
 
#include "semantics.h"
 
 
/******************************************************** PIPSMAKE INTERFACE */
 
/* Compute an initial transformer.
 */
bool initial_precondition(string name)
{
    entity module = module_name_to_entity(name);
    transformer prec;
 
    debug_on("SEMANTICS_DEBUG_LEVEL");
 
    set_current_module_entity(module);
    set_current_module_statement( (statement)
        db_get_memory_resource(DBR_CODE, name, true));
    make_statement_global_stack();
    set_cumulated_rw_effects((statement_effects)
                   db_get_memory_resource(DBR_CUMULATED_EFFECTS, name, true));
    set_proper_rw_effects((statement_effects)
                   db_get_memory_resource(DBR_PROPER_EFFECTS, name, true));
    module_to_value_mappings(module);
 
    prec = all_data_to_precondition(module);
 
    ifdebug(1)
        pips_assert("consistent initial precondition before filtering", 
                    transformer_consistency_p(prec));
 
    /* Filter out local and unused variables from the local precondition?
     * No, because it is not possible to guess what is used or unused at
     * the program level. Filtering is postponed to program_precondition().
     */
 
    DB_PUT_MEMORY_RESOURCE(DBR_INITIAL_PRECONDITION, strdup(name), (char*) prec);
 
    reset_current_module_entity();
    reset_current_module_statement();
    free_statement_global_stack();
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
 
    free_value_mappings();
 
    debug_off();
    return true;
}
 
/* returns t1 inter= t2;
 */
static void
intersect(
    transformer t1,
    transformer t2)
{
    predicate_system(transformer_relation(t1)) =
        sc_append((Psysteme) predicate_system(transformer_relation(t1)),
                  (Psysteme) predicate_system(transformer_relation(t2)));
}
 
#define pred_debug(level, msg, trans) \
  ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);}
 
/* Compute the union of all initial preconditions.
 */
bool program_precondition(const string name)
{
    transformer t = transformer_identity();
 
    /* A small function that would require pipsdbm and ri-util*/
    const string mn = get_main_entity_name();
    entity the_main = module_name_to_entity(mn);
 
    pips_assert("main was found", the_main!=entity_undefined);
 
    free(mn);
 
    int i, nmodules;
    gen_array_t modules;
    list e_inter = NIL;
 
    debug_on("SEMANTICS_DEBUG_LEVEL");
    pips_debug(1, "considering program \"%s\" with main \"%s\"\n", name,
               module_local_name(the_main));
 
    set_current_module_entity(the_main);
    set_current_module_statement( (statement)
                                  db_get_memory_resource(DBR_CODE,
                                                         module_local_name(the_main),
                                                         true));
    make_statement_global_stack();
    set_cumulated_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_CUMULATED_EFFECTS,
                                                    module_local_name(the_main),
                                                    true));
    set_proper_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_PROPER_EFFECTS,
                                                    module_local_name(the_main),
                                                    true));
 
    /* e_inter = effects_to_list(get_cumulated_rw_effects(get_current_module_statement())); */
 
    e_inter = effects_to_list( (effects)
                               db_get_memory_resource(DBR_SUMMARY_EFFECTS,
                                                      module_local_name(the_main),
                                                      true));
 
    module_to_value_mappings(the_main);
 
    /* Unavoidable pitfall: initializations in uncalled modules may be
     * taken into account. It all depends on the "create" command.
     */
    modules = db_get_module_list();
    nmodules = gen_array_nitems(modules);
    pips_assert("some modules in the program", nmodules>0);
 
    for(i=0; i<nmodules; i++) {
        transformer tm;
        string mname = gen_array_item(modules, i);
        pips_debug(1, "considering module %s\n", mname);
 
        tm = transformer_dup((transformer) /* no dup & false => core */
                             db_get_memory_resource(DBR_INITIAL_PRECONDITION,
                                                    mname, true));
 
        pred_debug(3, "current: t =\n", t);
        pred_debug(2, "to be added: tm =\n", tm);
        translate_global_values(the_main, tm); /* modifies tm! */
        pred_debug(3, "to be added after translation:\n", tm);
        tm = transformer_intra_to_inter(tm, e_inter);
        /* tm = transformer_normalize(tm, 2); */
        if(!transformer_consistency_p(tm)) {
            (void) print_transformer(tm);
            pips_internal_error("Non-consistent filtered initial precondition");
        }
        pred_debug(3, "to be added after filtering:\n", tm);
 
        intersect(t, tm);
        free_transformer(tm);
    }
 
    pred_debug(1, "resulting program precondition:\n", t);
 
    ifdebug(1)
        pips_assert("consistent program precondition",
                    transformer_consistency_p(t));
 
    DB_PUT_MEMORY_RESOURCE(DBR_PROGRAM_PRECONDITION, "", t);
 
    reset_current_module_entity();
    reset_current_module_statement();
    free_statement_global_stack();
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
 
    free_value_mappings();
    gen_array_full_free(modules);
 
    debug_off();
    return true;
}
 
/* The program correctness postcondition cannot be infered. It should be
   provided by the user. */
bool program_postcondition(const string name)
{
  transformer post = transformer_identity();
 
  /* A small function that would require pipsdbm and ri-util*/
  const string mn = get_main_entity_name();
  entity the_main = module_name_to_entity(mn);
  free(mn);
 
  debug_on("SEMANTICS_DEBUG_LEVEL");
  pips_debug(1, "considering program \"%s\" with main \"%s\"\n", name,
             module_local_name(the_main));
 
  pred_debug(1, "assumed program postcondition:\n", post);
 
  ifdebug(1) 
    pips_assert("consistent program postcondition", 
                transformer_consistency_p(post));
 
  DB_PUT_MEMORY_RESOURCE(DBR_PROGRAM_POSTCONDITION, "", post);
 
  debug_off();
  return true;
}
 
 
/*********************************************************** PRETTY PRINTERS */
 
bool print_initial_precondition(const string name)
{
    bool ok;
    entity module = module_name_to_entity(name);
    transformer t = (transformer) 
        db_get_memory_resource(DBR_INITIAL_PRECONDITION, name, true);
    
    debug_on("SEMANTICS_DEBUG_LEVEL");
 
    set_current_module_entity(module);
    set_current_module_statement( (statement) 
        db_get_memory_resource(DBR_CODE, name, true));
    set_cumulated_rw_effects((statement_effects) 
                   db_get_memory_resource(DBR_CUMULATED_EFFECTS,
                                          name,
                                          true));
    module_to_value_mappings(module);
 
    ok = make_text_resource_and_free(name, DBR_PRINTED_FILE, ".ipred",
                                     text_transformer(t));
 
    reset_current_module_entity();
    reset_current_module_statement();
    reset_cumulated_rw_effects();
 
    free_value_mappings();
 
    debug_off();
 
    return ok;
}
 
bool print_program_precondition(const string name)
{
    bool ok;
    transformer t = (transformer) 
        db_get_memory_resource(DBR_PROGRAM_PRECONDITION, "", true);
 
    /* A small function that would require pipsdbm and ri-util*/
    const string mn = get_main_entity_name();
    entity m = module_name_to_entity(mn);
    free(mn);
    
    debug_on("SEMANTICS_DEBUG_LEVEL");
    pips_debug(1, "for \"%s\"\n", name);
 
    set_current_module_entity(m);
    set_current_module_statement( (statement) 
        db_get_memory_resource(DBR_CODE,
                               module_local_name(m),
                               true));
    set_cumulated_rw_effects((statement_effects) 
                   db_get_memory_resource(DBR_CUMULATED_EFFECTS,
                                          module_local_name(m),
                                          true));
    module_to_value_mappings(m);
 
    ok = make_text_resource_and_free(name, DBR_PRINTED_FILE, ".pipred",
                                     text_transformer(t));
 
    reset_current_module_entity();
    reset_current_module_statement();
    reset_cumulated_rw_effects();
 
    free_value_mappings();
 
    debug_off();
 
    return ok;
}