initial.c File Reference

#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"

Include dependency graph for initial.c:

Go to the source code of this file.

Macros
#define	pred_debug(level, msg, trans)    ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);}

Functions
bool	initial_precondition (string name)
	Compute an initial transformer. More...
static void	intersect (transformer t1, transformer t2)
	returns t1 inter= t2; More...
bool	program_precondition (const string name)
	Compute the union of all initial preconditions. More...
bool	program_postcondition (const string name)
	The program correctness postcondition cannot be infered. More...
bool	print_initial_precondition (const string name)
bool	print_program_precondition (const string name)

Macro Definition Documentation

pred_debug

#define pred_debug	(		level,
			msg,
			trans
	)		ifdebug(level) { pips_debug(level, msg); dump_transformer(trans);}

Definition at line 129 of file initial.c.

Function Documentation

initial_precondition()

bool initial_precondition

(

string

name

)

Compute an initial transformer.

initial.c

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

Parameters

name

ame

Definition at line 75 of file initial.c.

{
    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;
}

References all_data_to_precondition(), db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free_statement_global_stack(), free_value_mappings(), ifdebug, make_statement_global_stack(), module, module_name_to_entity(), module_to_value_mappings(), pips_assert, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), strdup(), and transformer_consistency_p().

Here is the call graph for this function:

intersect()

static void intersect ( transformer  t1, transformer  t2  )

static

returns t1 inter= t2;

Definition at line 120 of file initial.c.

{
    predicate_system(transformer_relation(t1)) =
        sc_append((Psysteme) predicate_system(transformer_relation(t1)),
                  (Psysteme) predicate_system(transformer_relation(t2)));
}

References predicate_system, sc_append(), and transformer_relation.

Referenced by program_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

print_initial_precondition()

bool print_initial_precondition

(

const string

name

)

Parameters

name

ame

Definition at line 261 of file initial.c.

{
    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;
}

References db_get_memory_resource(), debug_off, debug_on, free_value_mappings(), make_text_resource_and_free(), module, module_name_to_entity(), module_to_value_mappings(), ok, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().

Here is the call graph for this function:

print_program_precondition()

bool print_program_precondition

(

const string

name

)

A small function that would require pipsdbm and ri-util

Parameters

name

ame

Definition at line 293 of file initial.c.

{
    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;
}

References db_get_memory_resource(), debug_off, debug_on, free(), free_value_mappings(), get_main_entity_name(), make_text_resource_and_free(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), ok, pips_debug, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().

Here is the call graph for this function:

program_postcondition()

bool program_postcondition

(

const string

name

)

The program correctness postcondition cannot be infered.

It should be provided by the user.

A small function that would require pipsdbm and ri-util

Parameters

name

ame

Definition at line 233 of file initial.c.

{
  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;
}

References DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free(), get_main_entity_name(), ifdebug, module_local_name(), module_name_to_entity(), pips_assert, pips_debug, pred_debug, transformer_consistency_p(), and transformer_identity().

Here is the call graph for this function:

program_precondition()

bool program_precondition

(

const string

name

)

Compute the union of all initial preconditions.

A small function that would require pipsdbm and ri-util

e_inter = effects_to_list(get_cumulated_rw_effects(get_current_module_statement()));

Unavoidable pitfall: initializations in uncalled modules may be taken into account. It all depends on the "create" command.

no dup & false => core

modifies tm!

tm = transformer_normalize(tm, 2);

Parameters

name

ame

Definition at line 134 of file initial.c.

{
    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;
}

References db_get_memory_resource(), db_get_module_list(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, effects_to_list(), entity_undefined, free(), free_statement_global_stack(), free_transformer(), free_value_mappings(), gen_array_full_free(), gen_array_item(), gen_array_nitems(), get_main_entity_name(), ifdebug, intersect(), make_statement_global_stack(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), NIL, pips_assert, pips_debug, pips_internal_error, pred_debug, print_transformer, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_intra_to_inter(), and translate_global_values().

Here is the call graph for this function: