[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
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 9a07d6a778
commit 4bae1ec07e

@ -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)

@ -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 =

@ -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

Loading…
Cancel
Save