From c9185ae6078623354b657fa5d4b9e1b1f40d0c66 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:48:50 -0800 Subject: [PATCH] [sledge] Add __llair_unreachable intrinsic for use in model code Reviewed By: jvillard Differential Revision: D25146156 fbshipit-source-id: cf48508b9 --- sledge/cli/frontend.ml | 2 ++ sledge/model/llair_intrinsics.h | 6 +++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 7719f394a..2df115a29 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -1112,6 +1112,7 @@ let xlate_instr : | ["__llair_throw"] -> let pre, exc = xlate_value x (Llvm.operand instr 0) in emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc) + | ["__llair_unreachable"] -> emit_term Term.unreachable (* dropped / handled elsewhere *) | ["llvm"; "dbg"; ("declare" | "value")] |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _ @@ -1180,6 +1181,7 @@ let xlate_instr : xlate_jump x instr unwind_blk loc [] in emit_term ~prefix (Term.goto ~dst ~loc) ~blocks + | ["__llair_unreachable"] -> emit_term Term.unreachable (* unimplemented *) | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ -> todo "statepoints:@ %a" pp_llvalue instr () diff --git a/sledge/model/llair_intrinsics.h b/sledge/model/llair_intrinsics.h index daef770dc..81ca43882 100644 --- a/sledge/model/llair_intrinsics.h +++ b/sledge/model/llair_intrinsics.h @@ -13,9 +13,13 @@ extern "C" { __attribute__((noreturn)) void __llair_throw(void* thrown_exception); -/* This models allocation that cannot fail. */ +/* express assumption that an execution is not possible */ +__attribute__((noreturn)) void __llair_unreachable(); + +/* allocation that cannot fail. */ void* __llair_alloc(unsigned size); +/* non-deterministic choice */ int __llair_choice(); #ifdef __cplusplus