Skip to content

resolve RIP in some x86 fp semantics #1637

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Angs12 wants to merge 2 commits into
base: master
Choose a base branch
from
Open

resolve RIP in some x86 fp semantics #1637

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
02e3912
resolve rip
Angs12 May 25, 2026
f974fbf
Add get-instruction-length and fix pc resolving to account for instru…
Angs12 May 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions plugins/primus_lisp/primus_lisp_semantic_primitives.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,6 +256,10 @@ let export = Primus.Lisp.Type.Spec.[
"get-current-program-counter", unit @-> int,
"(get-current-program-counter) is an alias to (get-program-counter)";

"get-instruction-length", unit @-> int,
"(get-instruction-length) returns the length of the current instruction \
in bytes.";

"set-symbol-value", tuple [any; a] @-> a,
"(set-symbol-value S X) sets the value of the symbol S to X.
Returns X";
Expand Down Expand Up @@ -839,6 +843,12 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
| None -> !!(empty s)
| Some addr -> forget@@const_int s addr

let get_instruction_length s lbl =
let open Bap.Std in
KB.collect Memory.slot lbl >>= function
| None -> !!(empty s)
| Some mem -> forget@@int s (Memory.length mem)

let require_symbol v k =
match symbol v with
| Some name -> k name
Expand Down Expand Up @@ -1479,6 +1489,7 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
| "store-word",_-> data@@store_word t args
| "get-program-counter",[]
| "get-current-program-counter",[] -> pure@@get_pc s lbl
| "get-instruction-length",[] -> pure@@get_instruction_length s lbl
| "set-symbol-value",[sym;x] -> data@@set_symbol t sym x
| "symbol-concat",syms -> pure@@symbol_concat s syms
| "symbol",[x] -> pure@@mksymbol s x
Expand Down
2 changes: 1 addition & 1 deletion plugins/primus_lisp/site-lisp/llvm-x86-64-floats.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@

(defun reg-val (reg)
(case (reg-name reg)
'RIP (+ (get-current-program-counter) 8)
'RIP (+ (get-current-program-counter) (get-instruction-length))
'RSP RSP
'RBP RBP
(error "unknown register")))
Expand Down
4 changes: 2 additions & 2 deletions plugins/x86/semantics/x86-64.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@

(defun reg# (reg)
(if (is-rip reg)
(+ (get-program-counter) 8)
(+ (get-program-counter) (get-instruction-length))
reg))

(defun load-mem (reg off)
Expand Down Expand Up @@ -478,4 +478,4 @@
(set rd (opo (opi rn rm))))

(defmacro bitwise-rrm (set opo opi rd rn ptr off)
(set rd (opo (opi rn (load-bits (word-width (unquote rn)) (+ ptr off))))))
(set rd (opo (opi rn (load-bits (word-width (unquote rn)) (+ (reg# ptr) off))))))
Loading