Changes between Version 11 and Version 12 of C Interface


Ignore:
Timestamp:
06/04/10 11:58:56 (16 years ago)
Author:
Stephen Siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • C Interface

    v11 v12  
    11How will one mark up a C program for the TASS model extractor?  This page is organized by issues that arise.
    2 
    3 Some of these problems might be solved by having the user assume there is an identifier {{{_TASS}}}. Then the user can use {{{#ifdef}}} blocks to wrap statements used by TASS but not a standard C compiler.
    42
    53== Input/Output ==
    64
    7 A real scientific program written in C does not have "input" and "output" variables  Inputs may come from a variety of sources, mainly from files.   But preprocessor directives may also be considered input, there may be input from the terminal, or from other sources.  Output is also typically written to files or the screen.  How do we model the input/output in this case?   What should we expect the user to do?    Perhaps the user should write a "TASS harness" which wraps the code in some way that specifies the input and output clearly?  Ideas, please.
     5A real scientific program written in C does not have "input" and "output" variables.  Inputs may come from a variety of sources, mainly from files.   But preprocessor directives may also be considered input, there may be input from the terminal, or from other sources.  Output is also typically written to files or the screen.  How do we model the input/output in this case?   What should we expect the user to do?    Perhaps the user should write a "TASS harness" which wraps the code in some way that specifies the input and output clearly?  Ideas, please.
     6
     7I/O to/from files (including stdout) will be handled by creating an abstract model of the stdio library.   This will introduce some shared variables (for the files) and define functions corresponding to the usual ones in stdio.h.   There will be no need for user annotations, except for exceptional situations (e.g., to ignore a certain input or output command).   Further details are coming.
     8
     9The argv and argc parameters passed to main will become the input variables for the model.   There are some ways pre-processor object-type macros can also be treated as inputs, but some thought will have to be put into this.
     10
    811
    912== Assumptions ==
    … …  
    1518How to do this in C?
    1619
     20Answer: with a new pragma inserted at some appropriate place:
     21
     22{{{
     23#pragma TASS assume N>0
     24}}}
     25
    1726== Non-deterministic select statement ==
    1827
    … …  
    2332Some MiniMP expressions do not occur in C, such as {{{forall}}}, {{{exists}}}.  For accuracy, there is also the derivative notation.   How to express them?  Where can they occur?  Can we use C's {{{assert}}}?
    2433
     34Answer: probably we cannot use C's assert for expressions which are not C expressions.  Instead use pragmas:
    2535
    26 == Loop invariants/co-invariants ==
     36{{{
     37#pragma TASS assert forall {int i | i>=0 && i<N} a[i]>=0
     38}}}
    2739
     40
     41== Loop (joint) invariants ==
     42
     43These are also expressed as pragmas:
     44{{{
     45#pragma TASS jointinvariant skew(2:1) i == spec.j && k == spec.s + 1
     46}}}
     47or something like that.
    2848
    2949== Library calls ==
    3050
    31 Think of the functions in {{{stdlib}}}, {{{stdio}}}, etc.  We need some sort of abstract model of at least the most commonly-used functions.  Most of them do not have state and should be representable in a simple way, perhaps abstracted away altogether.
     51Library calls will be modeled by creating abstract versions of the libraries.    Syntactically, in the model these will also be function calls just like other function calls.
     52There are three types of functions that can be called:
    3253
    33 We think the best approach is to create separate MiniMP library files corresponding to the standard C ones.  For example, mathlib.mmp:
     541. regular function that have an explicit body (locations and statements).  These may be user-defined, or be defined in a library.  They are treated the same in either case.
     55
     562. abstract function: these are modeled just using an uninterpreted symbolic constant function.  They have no body and no semantics associated to them.    They must be side-effect free.  Examples are "sin" and "atanh".   These will be declared in our abstract representations of the libraries, e.g.:
    3457
    3558{{{
    … …  
    3861}}}
    3962
    40 == Abstract Functions ==
     633. system level functions.  Examples are malloc, free, send.  These do not have bodies.  Instead, the semantics of each will be defined by a special class in the semantics package that describes how the state is transformed by executing such a function.    The function is executed in one atomic step.  It is like defining a new atomic statement.
    4164
    4265== Example ==
    … …  
    4972#include<stdio.h>
    5073#include<assert.h>
    51 /*@ _TASS_input {B>0} */
     74
     75#pragma TASS input int B
    5276#define B 3
    5377
    … …  
    7296  assert(fp);
    7397  while (1) {
    74     /* if fp is a real file, read it as normal. otherwise it is a symbolic file,
    75       * and a symbolic expression is stored in tmp.   The expression
    76       * is the application of an abstract function to the filename and
    77       * an integer-valued expression representing current point in file. */
    7898    int more = fscanf(fp, "%lf", &tmp);
    7999
    80     /*@ _TASS_assume(tmp>=0.0) */
     100    #pragma TASS assume tmp>=0.0
    81101    if (more == EOF) break;
    82102    i++;
    83103    if (i>B) {
     104      #pragma TASS ignore
    84105      printf("Too many numbers!  Limit is %d.\
    85106", B);
    … …  
    96117}}}
    97118
    98 Idea: the result of fscanf can be represented as a symbolic function.  In other words, add functions:
    99 {{{
    100 _TASS_read_int(string filename, int position)
    101 _TASS_read_real(string filename, int position)
    102 }}}
    103 Or something like that.
     119== Pragmas ==
     120
     121Here is a list of pragma types we need:
     122
     123* {{{#pragma TASS assert <TASS expression>}}}
     124* {{{#pragma TASS assume <TASS expression>}}}
     125* {{{#pragma TASS invariant <TASS expression>}}}
     126* {{{#pragma TASS jointinvariant <TASS expression>}}}
     127* {{{#pragma TASS ignore}}}
     128* {{{#pragma TASS input <type> <variable>}}}
     129
     130Grammar of TASS expressions:
     131
     132The grammar can basically be extracted from the MiniMP grammar.   It should allow most all C expressions, plus our new expressions:
     133* {{{spec.<identifier>}}}
     134* {{{forall {<type> <ident> | expr} expr}}}
     135* ditto with {{{exists}}} in place of {{{forall}}}
    104136
    105137
    106 
    107 Questions:
    108 * do we need to add char (and string?) datatypes to TASS?
    109 
    110 == Pragmas ==
    111 
    112 Pragmas might be the best way to get the information through the front-end.
    113 
    114 {{{
    115 l1:
    116 #pragma TASS factor(2:1) inv(i == spec.j && k == spec.s + 1)
    117 while(...)
    118 {
    119 ...
    120 }
    121 }}}
    122 
    123 {{{
    124 #pragma TASS input assume(a>=0 && a<=5) is(b)
    125 int a;
    126 }}}
    127 
    128 How to deal with preprocessor macros?  We want to preserve preprocessor info.
    129 We must find out if ROSE and LLVM can do that.
     138Examples:
    130139
    131140== LLVM to TASS-AST ==