Is there an interactive interpreter for Primus Lisp ?

[Heersin]

This document is a summary of gitter thread. I would like to express my great thanks to Ivan,

Using Primus Lisp interpreter

Just imagine that you found an interesting operation of BAP Core Theory, and would like to explore the semantic of such an operation. How ? Is there an interactive interpreter for Primus Lisp, which I can simply type (print_int (cast_int -1.0)) and evaluate it ?

Primus Lisp Interpreter

Currently, the interpreter is not really intreactive, but very close to it. There are two interpreters in BAP, a static one and a dynamic one.

Static (semantic) one interprets Primus Lisp into static denotations (e.g. BIL, Bir). The translation uses staged computation, so everything that could be reduced will be reduced as much as possible. In other words, it uses advanced contact folding. Normally operations are resolved statically and lifted into intrinsic subroutines that perform floating-point operations using bitvector arithmetic.

Dynamic one evaluates programs to values. It lacks some primitives (e.g. float operations), so BAP provides those primitives by mapping some operations to calls to OCaml functions instead of Core Theory operations (bitvector arithmetic). And developer do not use it other than debugging.

Usage

Related command can be found by :

$ bap list commands | grep lisp
  primus-lisp-documentation no description provided
  eval-lisp                runs the Primus lisp program
  show-lisp                shows the static semantics of Primus Lisp definitions

To read the documentation about a command, use bap <command> --help, or the abbreviate the name to unambiguous form bap show --help

created a demo.lisp with the following content:

(defun e0 ()
  (set RDI (+ 1 2 3)))

and let's print the BIL reification of this program

$ bap show e0 --primus-lisp-load=demo -tx86_64 -obap:bil
e0:
"{
   RDI := 6
 }"

show takes the definition name that you would like to see, in our case it is e0. It has another two params:

• -t specify the target (see bap list targets)

• -o specify the output denotation (see bap list classes), omit this would print all non-empty denotations.

  $ bap show e0 --primus-lisp-load=demo -tx86_64
  e0:
  ((bap:ir-graph "0000000a:
                  0000000b: RDI := 6")
   (bap:insn-dests (()))
   (bap:bir (%0000000a))
   (bap:bil "{
               RDI := 6
             }")
   (core:value ((bap:static-value (0x6)) (bap:exp 6))))

To get a whole set of Primus Lisp operations, you could use the following commands to generate Emacs org format doc, and then translate it to other format. (e.g. pdf)

$ bap primus-lisp-doc --semantics > lisp.org
$ pandoc lisp.org -o primus_lisp.pdf

Examples

It's time to go to the original question. I would like to explore the semantic of (cast_int -1.0) on x86_64 machine. We could locate related operations and constant in document,

"Constants"
+rne+
;; File "x86-64-sse-intrinsics.lisp", line 8, characters 0-21
(defconstant +rne+ 0)

(cast-int M S X) converts a floating-point number X to the nearest unsigned
integer with the size S using the rounding mode M

(cast-sfloat M S X) converts a signed integer X to the nearest representable
floating-point number with size S using the rounding mode M

create a fcast_demo.lisp with following contents:

(defun e1 ()
  (set RDI (cast-int :rne 64 (cast-sfloat :rne 64 -1))))

(defun e2 ()
  (set RDI (cast-int :rne 64 (cast-sfloat :rne 64 0xDEADBEEF))))

(defun e3 ()
  (set RDI (cast-sint :rne 64 (cast-sfloat :rne 64 -1))))

and show all of them

$ bap show e{1,2,3} --primus-lisp-load=fcast_demo -tx86_64 -obap:bil
e1:
"{
   RDI := 0xFFFFFFFFFFFFFFFF
 }"
e2:
"{
   RDI := 0xDEADBEEF
 }"
e3:
"{
   RDI := 0xFFFFFFFFFFFFFFFF
 }"

Q&A

1. When set the size of cast-float to 16/32/80/128, it reports an error.

   (defun e0 ()
     (set RAX (cast-int :rne 32 (cast-sfloat :rne 32 1))))

   Failed to reify the program: Failed to apply primitive core:cast-int: defined for bitvecs, bools, or syms
   Applied as:
   (core:cast-int ((bap:static-value (0x2)) (lisp-symbol (:rne)))
     ((bap:static-value (0x20)) (bap:exp 0x20)) ((bap:exp 0x3F800000)))
   

   it's a misleading error message, now BAP only support IEEE754 64-bit binary format.

Refs

1. BAP Primus Lisp