[LLVMbugs] [Bug 810] NEW: Adding assert/assume intrinsics to LLVM

[bugzilla-daemon at cs.uiuc.edu]

http://llvm.org/bugs/show_bug.cgi?id=810

           Summary: Adding assert/assume intrinsics to LLVM
           Product: libraries
           Version: trunk
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: Global Analyses
        AssignedTo: unassignedbugs at nondot.org
        ReportedBy: domagoj at engineer.com


Hi,

I'd like to open a discussion on adding assert/assume intrinsics to
LLVM. Here I will describe the syntax, semantics, and applications 
of both.

Those statements should have the following syntax:

assert/assume ( Boolean_variable, String )

"Boolean_variable" represents a condition.

The only purpose of "String" is to classify assertions and assumptions
into classes, so that, for example, certain class of assertions can be
enabled or disabled during the code generation. For maximal generality,
I'd suggest leaving "String" unspecified for now. The users can come up
with identifiers like "Range_check" or similar.


The semantics of statements is:

ASSERT - if the condition evaluates to TRUE, the statement is a NOP,
otherwise the assertion terminates the program. Code generators should
be able to enable/disable assertions, but are also allowed to completely
ignore them.

ASSUME - is always a NOP, but the code generators might generate code
that issues a warning if the condition evaluates to FALSE. Assumptions
present the conditions that "should", but are not guaranteed to hold.


Applications:

ASSERT - debugging, code reliability, can represent both user provided
assertions (invariants, pre/post-conditions) and automatically inserted
checks, like range checking.

ASSUME - primarily as a tool for communication between passes. Some
possible applications include: 

* language independent attribute mechanism
[ like assume(restricted(ptr_x), "Restricted Pointer") ] 

* passing information through different stages of the compilation 
framework, for example, a loop analysis pass might store an inferred
loop invariant as assume(x + y < 200, "Loop Invariant").

* static checking. For details I'd suggest papers from Dijkstra, Greg
Nelson, Rustan Leino.


It should be noted that ASSUMEs have application specific meaning, and
should not be touched by passes that do not use them (something like dbg
intrinsics).

Looking forward to your comments,

Domagoj Babic



------- You are receiving this mail because: -------
You are on the CC list for the bug, or are watching someone who is.