postcondition.c File Reference

#include <stdio.h>
#include <string.h>
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "prettyprint.h"
#include "effects-util.h"
#include "misc.h"
#include "semantics.h"
#include "transformer.h"

Include dependency graph for postcondition.c:

Go to the source code of this file.

Macros
#define	StorePost(stat, val)
#define	StorePre(stat, val)
#define	LoadPost(stat)
#define	LoadPre(stat)

Functions
static bool	postcondition_filter (statement stat)
	filter used by gen_recurse: Top-down computation of the postcondition mapping More...
statement_mapping	compute_postcondition (statement stat, statement_mapping post_map, statement_mapping pre_map)
	statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping post_map, pre_map; More...

Variables
static statement_mapping	current_precondition_map = hash_table_undefined
	filtering of postconditions More...
static statement_mapping	current_postcondition_map = hash_table_undefined

Macro Definition Documentation

LoadPost

#define LoadPost

(

stat

)

Value:

    (debug(9, "LoadPost", "loading 0x%x\n", stat), \
     (transformer) (hash_get(current_postcondition_map, (char*) stat)))

Definition at line 77 of file postcondition.c.

LoadPre

#define LoadPre

(

stat

)

Value:

    (debug(9, "LoadPre", "loading 0x%x\n", stat), \
     (transformer) (hash_get(current_precondition_map, (char*) stat)))

Definition at line 81 of file postcondition.c.

StorePost

#define StorePost	(		stat,
			val
	)

Value:

   (debug(9, "StorePost", "storing 0x%x, 0x%x\n", stat, val), \
    hash_put(current_postcondition_map, (char*) (stat), (char*) (val)))

Definition at line 69 of file postcondition.c.

StorePre

#define StorePre	(		stat,
			val
	)

Value:

   (debug(9, "StorePre", "storing 0x%x, 0x%x\n", stat, val), \
    hash_put(current_precondition_map, (char*) (stat), (char*) (val)))

Definition at line 73 of file postcondition.c.

Function Documentation

compute_postcondition()

statement_mapping compute_postcondition	(	statement	stat,
		statement_mapping	post_map,
		statement_mapping	pre_map
	)

statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping post_map, pre_map;

computes the postcondition mapping post_map from the precondition mapping pre_map and the related statement tree starting from stat. The rule applied is that the postcondition of one statement is the precondition of the following one. The last postcondition is arbitrary set to transformer_identity, what is not enough. (??? should I take the stat transformer?)

the initial postcondition is empty ???

Top-down definition

Parameters

stat	tat
post_map	ost_map
pre_map	re_map

Definition at line 186 of file postcondition.c.

{
    debug_on("SEMANTICS_POSTCONDITION_DEBUG_LEVEL");
    pips_debug(1, "computing!\n");
 
    current_postcondition_map = post_map;
    current_precondition_map = pre_map;
 
    /* the initial postcondition is empty ??? */
    StorePost(stat, transformer_identity());
 
    /* Top-down definition */
    gen_recurse(stat, statement_domain, postcondition_filter, gen_null);
 
    current_precondition_map = hash_table_undefined;
    current_postcondition_map = hash_table_undefined;
 
    debug_off();
    return post_map;
}

References current_postcondition_map, current_precondition_map, debug_off, debug_on, gen_null(), gen_recurse, hash_table_undefined, pips_debug, postcondition_filter(), statement_domain, StorePost, and transformer_identity().

Referenced by set_resources_for_module().

Here is the call graph for this function:

Here is the caller graph for this function:

postcondition_filter()

static bool postcondition_filter ( statement  stat )

static

filter used by gen_recurse: Top-down computation of the postcondition mapping

??? may happen in obscure unstructured...

??? may be false...

??? is just false...

generates the full list

???

must go downward

Definition at line 88 of file postcondition.c.

{
    instruction inst = statement_instruction(stat);
    transformer post = LoadPost(stat);
 
    pips_debug(5, "statement %p (post %p)\n", stat, post);
 
    ifdebug(9) {
        pips_debug(9, "statement is\n");
        print_statement(stat);
    }
 
    /* ??? may happen in obscure unstructured... */
    if (transformer_undefined_p(post)) return true; 
 
    switch(instruction_tag(inst))
    {
    case is_instruction_block:
    {
        list ls = gen_nreverse(gen_copy_seq(instruction_block(inst)));
 
        pips_debug(6, "in block\n");
 
        MAP(STATEMENT, s,
         {
             StorePost(s, post);
             post = LoadPre(s);
         },
             ls);
 
        gen_free_list(ls);
        break;
    }
    case is_instruction_test:
    {
        test t = instruction_test(inst);
        pips_debug(6, "in test\n");
 
        StorePost(test_true(t), post);
        StorePost(test_false(t), post);
 
        break;
    }
    case is_instruction_loop:
        pips_debug(6, "in loop\n");
        StorePost(loop_body(instruction_loop(inst)), post);
        break;
    case is_instruction_goto:
        /* ??? may be false... */
        pips_internal_error("unexpected goto encountered");
        break;
    case is_instruction_call:
        break;
    case is_instruction_unstructured:
        /* ??? is just false... */
    {
        control c = unstructured_control(instruction_unstructured(inst));
        list blocks = NIL;
 
        pips_debug(6, "in unstructured\n");
 
        /* generates the full list */
        CONTROL_MAP(__attribute__ ((unused)) ct, {}, c, blocks);
 
        blocks = gen_nreverse(blocks);
 
        MAP(CONTROL, c,
         {
             statement s = control_statement(c);
             StorePost(s, post);
             post = LoadPre(s); /* ??? */
         },
             blocks);
 
        gen_free_list(blocks);
 
        break;
    }
    default:
        pips_internal_error("unexpected instruction tag");
        break;
    }
 
    return true; /* must go downward */
}

References blocks, CONTROL, CONTROL_MAP, control_statement, gen_copy_seq(), gen_free_list(), gen_nreverse(), ifdebug, instruction_block, instruction_loop, instruction_tag, instruction_test, instruction_unstructured, is_instruction_block, is_instruction_call, is_instruction_goto, is_instruction_loop, is_instruction_test, is_instruction_unstructured, LoadPost, LoadPre, loop_body, MAP, NIL, pips_debug, pips_internal_error, print_statement(), STATEMENT, statement_instruction, StorePost, test_false, test_true, transformer_undefined_p, and unstructured_control.

Referenced by compute_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

current_postcondition_map

statement_mapping current_postcondition_map = hash_table_undefined

static

Definition at line 67 of file postcondition.c.

Referenced by compute_postcondition().

current_precondition_map

statement_mapping current_precondition_map = hash_table_undefined

static

filtering of postconditions

Standard includes Psystems stuff Newgen stuff PIPS stuff

Definition at line 66 of file postcondition.c.

Referenced by compute_postcondition().