From f4c2c8be7c4e71336345922072c26eff921c034e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 16 Nov 2020 12:53:05 -0800
Subject: [PATCH] [sledge] Translate __llair_choice intrinsic to nondet

Summary:
Currently __llair_choice is left undefined, and so executed as skip.
This has the correct behavior, but makes it hard to distinguish from
calls to unintentionally-undefined procedures.

Reviewed By: ngorogiannis

Differential Revision: D24989068

fbshipit-source-id: f62981857
---
 sledge/cli/frontend.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index 49f9058bc..0ca07835a 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -1013,6 +1013,10 @@ let xlate_instr :
       | Some intrinsic -> inline_or_move (intrinsic x)
       | None -> (
         match String.split_on_char fname ~by:'.' with
+        | ["__llair_choice"] ->
+            let reg = xlate_name x instr in
+            let msg = "__llair_choice" in
+            emit_inst (Inst.nondet ~reg:(Some reg) ~msg ~loc)
         | ["__llair_throw"] ->
             let pre, exc = xlate_value x (Llvm.operand instr 0) in
             emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc)