How will one mark up a C program for the TASS model extractor? This page is organized by issues that arise.

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.

Input/Output

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.

Assumptions

In MiniMP one writes:

input int N {N>0};

How to do this in C?

Non-deterministic select statement

Does not exist in C. Do we need it?

Assertion Language

Some 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?

Loop invariants/co-invariants

Library calls

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.

Abstract Functions

Example

Here is a program that adds the elements in a file. The commandline argument is the filename. Inputs are the filename, the contents of the file, and the parameter B which is an upper bound on the number of elements that will be read. Output is to stdout.

How do we annotate this file in such a way that it does not interfere with compilation, but provides all the information we need to build a TASS model?

#include<stdio.h>
#include<assert.h>
/*@ _TASS_input {B>0} */
#define B 3

double sum = 0.0;

/* arguments to main are inputs */
int main(int argc, char* argv[]) {
  char *filename;
  double result = 0.0;
  FILE *fp;
  double tmp;
  int i = 0;

  if (argc != 2) {
    printf("Usage: realadder filename\
");
    fflush(stdout);
    return 1;
  }
  filename = argv[1];
  fp = fopen(filename, "r");
  assert(fp);
  while (1) {
    /* if fp is a real file, read it as normal. otherwise it is a symbolic file,
      * and a symbolic expression is stored in tmp.   The expression
      * is the application of an abstract function to the filename and
      * an integer-valued expression representing current point in file. */
    int more = fscanf(fp, "%lf", &tmp);

    /*@ _TASS_assume(tmp>=0.0) */
    if (more == EOF) break;
    i++;
    if (i>B) {
      printf("Too many numbers!  Limit is %d.\
", B);
      fflush(stdout);
      return 2;
    }
    sum += tmp;
  }
  printf("The sum is %lf\
", sum);
  fclose(fp);
  return 0;
}

Idea: the result of fscanf can be represented as a symbolic function. In other words, add functions:

_TASS_read_int(string filename, int position)
_TASS_read_real(string filename, int position)

Or something like that.

Questions:

• do we need to add char (and string?) datatypes to TASS?

Pragmas

Pragmas might be the best way to get the information through the front-end.

l1:
#pragma factor(2:1) inv(i == spec.j && k == spec.s + 1)
while(...)
{
...
}

#pragma input assume(a>=0 && a<=5) is(b)
int a;