fixes register assignments in p-code semantics (#1455)

In p-code the lower parts of registers are referenced as variables with the same name as the base register but with the size equal to the size of the referenced part, e.g., YMM0:64 refers to the lower 64 bits of the YMM0 register. The semantics of assignemnt assumes that the upper parts are preserved. This commit implements the proper semantics of the `set#` operator, i.e., it extends the right-hand side to the size of the base register, and properly ORs it with the left-hand side. Note, the fix also touches the `setw` macro from #1454. It was still correct, since all uses of setw was properly typed (unlike p-code), but the new version is more consistent and more general as it now allows the right-hand side to have a different type.
BinaryAnalysisPlatform · Mar 29, 2022 · 8108e36 · 8108e36
1 parent 1415134
commit 8108e36
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/plugins/arm/semantics/arm-bits.lisp b/plugins/arm/semantics/arm-bits.lisp
@@ -26,9 +26,6 @@
         (set-flags r x y))
       (set$ rd r))))
 
-(defun logandnot (rd rn)
-  (logand rd (lnot rn)))
-
 (defmacro shift-with-carry (shift rd rn rm cnd)
   (when (condition-holds cnd)
     (let ((r (cast-signed (word-width) rn)))
@@ -61,4 +58,5 @@
 
 (defmacro setw (reg val)
   "(set Wx V) sets a Wx register clearing the upper 32 bits."
-  (set$ (alias-base-register reg) val))
+  (set$ (alias-base-register reg)
+        (cast-unsigned (word-width) val)))
diff --git a/plugins/ghidra/semantics/pcode.lisp b/plugins/ghidra/semantics/pcode.lisp
@@ -10,7 +10,10 @@
 (defmacro set# (typ dst src)
   (if (is-symbol typ)
     (store-word (cast-word dst) src)
-    (set$ dst src)))
+    (let ((typ (coerce (word-width dst) typ)))
+      (set$ dst (logor
+                 (logandnot dst (- (lshift 1 typ) 1))
+                 (cast-unsigned (word-width dst) src))))))
 
 (defmacro get# (typ src)
   (if (is-symbol typ) (load-word (cast-word src))

diff --git a/plugins/primus_lisp/semantics/bits.lisp b/plugins/primus_lisp/semantics/bits.lisp
@@ -1,5 +1,9 @@
 (in-package core)
 
+(defun logandnot (rd rn)
+  "(logandnot X Y) is X & ~Y, i.e., X and complement of Y"
+  (logand rd (lnot rn)))
+
 (defun msb (x)
   "(msb X) is the most significant bit of X."
   (select (- (word-width x) 1) x))