search

loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

Agree support uninterpreted functions #69

Closed cong-liu-2000 closed 3 years ago

cong-liu-2000 commented 3 years ago

What?

This implements the AGREE support of uninterpreted functions (UF). It is based on Isaac's previous work (branch "uninterpreted-functions"), which implements the UF grammar.

Why?

UF is used in TA6 use case to model complex math functions.

How?

  1. Add UF ("Function") to AST. Previously regular functions defined in AGREE annex are translated as Lustre "Node".
  2. Visit AST to add Jkind Lustre "Function" to AgreeProgram
  3. Visit AST (renaming) to store UF names (function name, I/O argument name)
  4. Process Jkind counterexample. If a UF name is recognized, let it pass to AGREE results.
  5. Reuse Jkind CounterexampleFormatter to display UF in AGREE console .
  6. Nothing special needs to be done for display UF in AGREE Excel view.

Testing?

Preliminary unit testing was done. It includes the following usage:

  1. UF is defined in a separate library.
  2. UF input argument is a record type
  3. UF output argument is a record type
  4. UF is called in another regular function definition
  5. UF is called in a contract
  6. UF is called in a expression

Screenshots (optional)

The table columns may be not fully aligned due to display issue. FUNCTIONS ufx ufy | UF_Unit_Test_5.A.uf._outvar.a
----------+------------------------------- 3 1 | 0
3 2 | 0

ufx ufy | UF_Unit_Test_5.A.uf._outvar.b
----------+------------------------------- 3 2 | 4

Anything Else?

  1. Display UF in AGREE Eclipse view is not supported. The current implementation (column-driven TreeViewer) of display counterexample in AGREE Eclipse is not compatible with UF natural format (row-driven, symbol row followed by value rows).
  2. UF without input argument is not supported.