User:Realazthat/Projects wishlist/LLVM/Formal methods

From Rosetta Code


Follow the examples of wp:Java_Modeling_Language and wp:SPARK_programming_language.

Things that the pass might prove, for each function:

  • That all assert statements can not occur, or complain otherwise (if an assert statement cannot be proved to not fail)
    LLVM and assert/assume:
  • Determine if the function requires Turing-completeness
  • Compute function complexity (best, average, worst) of an algorithm (function)
    • Allow the function to assert complexity
  • Allow arbitrary restrictions on functions, which would propagate through the call graph
    • Complexity (time/memory)
    • Restricting stack allocation
    • Restricting heap allocation
  • Allow a programmer to make certain assumptions on input (probably through assertions)
  • Prove that no undefined behavior can occur
    • Math overflows/underflows
    • Out of bounds access
    • Memory leaks
    • Dangling pointers
      • etc.
    • Null dereferencing
    • What else
  • Determine valid input ranges (if the type of the input does not already assert this)
  • Show proofs for all of the above
  • Impossible stuff
    • Be able to calculate a function inverse if possible
    • Transformation of function to set of equivalent functions
  • Side effect free functions
  • Pure functions
  • Reentrant functions
  • No deadlocks etc.
  • If any of the above can't be proven, show test counter examples; that is exploitable input