From 4bae1ec07e306563a6ed926e59530cef45fa116f Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:47:42 -0800 Subject: [PATCH] [sledge] Rename exec_intrinsic to exec_intrinsic_func Summary: Rename the existing exec_intrinsic that works for calls to intrinsic functions to exec_intrinsic_func to make room for an exec_intrinsic that works on intrinsic instructions. Reviewed By: jvillard Differential Revision: D25146166 fbshipit-source-id: 80ae3aac9 --- sledge/src/domain_sh.ml | 4 ++-- sledge/src/exec.ml | 2 +- sledge/src/exec.mli | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 864a56737..340795f80 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -75,12 +75,12 @@ let exec_inst inst pre = let areturn = Option.map ~f:X.reg reg in let intrinsic = Llair.Intrinsic.to_string name in let actuals = IArray.map ~f:X.term args in - Exec.intrinsic ~skip_throw:true pre areturn intrinsic actuals + Exec.intrinsic_func ~skip_throw:true pre areturn intrinsic actuals |> Option.get_lazy (fail "exec_inst: %a" Llair.Inst.pp inst) ) |> Option.map ~f:simplify let exec_intrinsic ~skip_throw r i es q = - Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) + Exec.intrinsic_func ~skip_throw q (Option.map ~f:X.reg r) (Llair.Function.name i) (IArray.map ~f:X.term es) |> Option.map ~f:(Option.map ~f:simplify) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index f85f260e6..28e486af0 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -737,7 +737,7 @@ let free pre ~ptr = exec_spec pre (free_spec ptr) let nondet pre = function Some reg -> kill pre reg | None -> pre let abort _ = None -let intrinsic ~skip_throw : +let intrinsic_func ~skip_throw : Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option = fun pre areturn intrinsic actuals -> let name = diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli index 7dc2258fa..ec3e15dd9 100644 --- a/sledge/src/exec.mli +++ b/sledge/src/exec.mli @@ -22,7 +22,7 @@ val free : Sh.t -> ptr:Term.t -> Sh.t option val nondet : Sh.t -> Var.t option -> Sh.t val abort : Sh.t -> Sh.t option -val intrinsic : +val intrinsic_func : skip_throw:bool -> Sh.t -> Var.t option