Skip to content

Make better use of conditional unreachable's in LLVM #1182

@llvmbot

Description

@llvmbot
Bugzilla Link 810
Resolution FIXED
Resolved on Sep 03, 2020 07:29
Version trunk
OS All
Blocks llvm/llvm-bugzilla-archive#3100
Reporter LLVM Bugzilla Contributor
CC @atrick,@mkurdej,@dwblaikie,@fhahn,@yuanfang-chen,@irishrover

Extended Description

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugzillaIssues migrated from bugzilla

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions