other
(in-package "BRIDGE")
other
(include-book "xdoc/top" :dir :system)
other
(include-book "tools/include-raw" :dir :system)
other
(include-book "std/strings/top" :dir :system)
other
(include-book "to-json")
other
(include-book "quicklisp/hunchentoot" :dir :system)
other
(include-book "quicklisp/bt-semaphore" :dir :system)
other
(defxdoc bridge :parents (interfacing-tools) :short "Connects ACL2 and the outside world." :long "<p>The ACL2 Bridge is a general mechanism for allowing other programming languages, which may be much better than Lisp for certain tasks like developing graphical user interfaces, to interact with ACL2. It extends ACL2 with a server that can accept connections from client programs and run commands on their behalf.</p> <p>The bridge is supported on both CCL (Clozure Common Lisp) and SBCL (Steel Bank Common Lisp). On SBCL, it uses the bordeaux-threads, usocket, and trivial-gray-streams libraries via Quicklisp.</p> <p>The basic picture is:</p> @({ _____________ _______________________ | | | | | ACL2 [bridge]--------------| client program | | | socket | java, c, perl, ... | |_____________| |_______________________| }) <p>On the ACL2 side, the bridge is a simple listen/accept style server that waits for new clients. When a client connects, it creates a new worker thread to handle the client's requests. The worker thread presents the client with a kind of read-eval-print loop.</p> <p>The client then sends @(see command)s. Basically each command says what s-expression to evaluate, and also indicates how the reply should be encoded. For instance, you can tell the bridge to return raw s-expressions, or you can tell it to use @(see json-encoding) to make the output easy to parse in some other programming languages. Other options may be added in the future.</p> <p>The worker thread executes the command. As it runs, it may send @(see message)s to the client. These messages contain output that has been printed to standard output, the return value or error conditions, and a ready indicator that says when the worker is ready for more input. The messages are tagged with types so that the client can tell what kind of output it's receiving.</p> <p>Some things are missing. There's currently no support for Lisp functions that want to read from standard input after they've been invoked. For instance, there's not really any way to interact with break loops, @('ld'), etc. There's also currently no direct way to send an interrupt. However, workers announce their name to the client when they say hello, so a client could presumably open another connection and interrupt that way. We haven't developed this much, yet.</p>")
other
(defxdoc security :parents (bridge) :short "Important warnings about network security and the ACL2 bridge." :long "<p>The ACL2 bridge allows clients to run arbitrary Lisp commands, including for instance syscall. Because of this,</p> <box><p>If a malicious person can connect to your bridge, then he can read or delete your files, run arbitrary programs as you, and so on.</p></box> <p>To reduce the chances of this happening, you should probably only run the bridge on a <a href='http://en.wikipedia.org/wiki/Unix_domain_socket'>unix domain socket</a>. These sockets appear to have good security properties. (Per my understanding: remote users on the internet cannot connect to them, and they even offer some protection from other users on your system through the normal Unix filesystem permissions.)</p> <p>The bridge <i>can</i> also be run on an ordinary TCP/IP socket, <b><color rgb='#ff0000'>but this is very scary</color></b> because remote clients can connect. If you decide to run it this very scary way, then you should be very scared:</p> <ul> <li>The bridge has <b>no authentication</b> mechanism, and will allow anyone who can connect to it to run any command.</li> <li>The bridge sends all messages in <b>plain text</b>, so an eavesdropper can probably see everything you send to the server and everything it sends back.</li> </ul> <p>So, before you even <i>think</i> about putting the bridge on a TCP/IP port, you should make sure that, e.g., you have firewalls in place or are using SSH tunnels or something.</p> <p><b>Disclaimer</b>. I am no security expert. The advice above is probably not enough to protect you. Please do not use the ACL2 Bridge without consulting your local security expert and network administrator.</p>")
other
(defxdoc message :parents (bridge) :short "Messages that the bridge sends to the client program." :long "<p>We send all output to the client in discrete <b>messages</b>. The message format is very simple. It is easy for a client to reliably parse, and doesn't require us to think about character encoding. Informally, the format is:</p> @({ type len[newline] contents[newline] }) <p>To make this extremely clear: we first print the @('type'), then a space, then the @('len'), then a newline character, then the @('contents'), then another newline character.</p> <p>The @('type') here is a label that describes what kind of message this is. It matches @('[A-Z][A-Z0-9_]*'). That is, it starts with an uppercase alphabetic character, and then contains only uppercase alphabetic, numeric, and underscore characters.</p> <p>The @('len') says how many characters are in @('contents'). It matches @('[0-9]+'), i.e., it is a base-10 natural number.</p>")
other
(defxdoc command :parents (bridge) :short "Commands that the client sends to the bridge." :long "<p>Each client is expected to send discrete <b>commands</b> that will be processed individually.</p> <p>The command format is identical to the @(see message) format, and is meant to be very easy for the client to generate. Clients should typically @('flush') the stream after printing their command to ensure that the server gets the input.</p> <p>The @('type') of the command governs how the server should send the result back to the client. The currently supported command types are:</p> <ul> <li>@('LISP') -- send only the first return value, and just use @('prin1') to encode it.</li> <li>@('LISP_MV') -- send all of the return values, essentially by doing @('prin1') on the @('multiple-value-list') of the result.</li> <li>@('JSON') -- send the @(see json-encoding) of the first return value. Note that this encoder only handles good ACL2 objects.</li> <li>@('JSON_MV') -- send the @(see json-encoding) of the @('multiple-value-list') of the result. Note that this encoder only handles good ACL2 objects.</li> </ul> <p>Adding other types would be trivial. For instance, it might be useful to add pretty-printing.</p>")
other
(defxdoc bindings :parents (bridge) :short "ACL2 Bridge interfaces for other programming languages." :long "<p>The ACL2 Bridge can probably be used from just about any programming language that has sockets.</p> <p>There is a nice <a href='https://www.ruby-lang.org/'>Ruby</a> interface in @('books/centaur/bridge/ruby').</p> <p>A <a href='https://www.python.org/'>Python</a> interface with synchronous and asynchronous bindings is available in @('books/centaur/bridge/python').</p> <p>For other programming languages, implementing a client should be a very easy exercise: just read about @(see command)s and @(see message)s to understand the communication. You might look at the Ruby interface as an example.</p>")
other
(defsection start :parents (bridge) :short "Start an ACL2 Bridge server." :long "<p><b>Warning:</b> don't even <i>think</i> about starting an ACL2 Bridge until you have read about @(see security).</p> <p>Unix Domain Socket Examples (recommended):</p> @({ (bridge::start "./my-socket") (bridge::start "/tmp/my-socket") }) <p>TCP/IP Socket Examples (<b>very scary</b> -- see @(see security)!!!):</p> @({ (bridge::start nil) ;; Listen on TCP/IP port 55432 (bridge::start 12345) ;; Listen on TCP/IP port 12345 }) <p>Additional keyword options (CCL only):</p> <ul> <li>@(':stack-size') -- stack size for worker threads (in bytes)</li> <li>@(':tstack-size') -- temporary stack size for worker threads (in bytes)</li> <li>@(':vstack-size') -- value stack size for worker threads (in bytes)</li> </ul> <p><b>Note:</b> The stack size parameters are CCL-specific. On SBCL, these parameters are accepted for API compatibility but are ignored; a warning is printed if non-default values are supplied. SBCL thread stack sizes are controlled at the SBCL startup level via command-line options like @('--control-stack-size') and @('--dynamic-space-size').</p>" (defun start-fn (socket-name-or-port-number stack-size tstack-size vstack-size) (declare (xargs :guard t) (ignorable socket-name-or-port-number stack-size tstack-size vstack-size)) (cw "Under-the-hood definition of bridge::start-fn not installed?~%")) (defmacro start (socket-name-or-port-number &key (stack-size '(* 16 (expt 2 20))) (tstack-size '(* 16 (expt 2 20))) (vstack-size '(* 16 (expt 2 20)))) `(start-fn ,BRIDGE::SOCKET-NAME-OR-PORT-NUMBER ,BRIDGE::STACK-SIZE ,BRIDGE::TSTACK-SIZE ,BRIDGE::VSTACK-SIZE)))
other
(defsection stop :parents (bridge) :short "Stop any running ACL2 Bridge servers." :long "<p>This is a low-level cleanup mechanism that ungracefully kills any bridge-listener and bridge-worker threads. This isn't something you probably want to ordinarily rely on in your code, but it's useful when you want to restart a server.</p>" (defun stop nil (declare (xargs :guard t)) (cw "Under-the-hood definition of bridge::stop not installed?")))
fibfunction
(defun fib (n) (declare (xargs :guard (natp n))) (cond ((zp n) 1) ((= n 1) 1) (t (+ (fib (- n 1)) (fib (- n 2))))))
other
(memoize 'fib)
sleep$function
(defun sleep$ (n) "Sleep for (rfix n) seconds. Has an under-the-hood implementation." (declare (xargs :guard t) (ignore n)) nil)
sleepyprintfunction
(defun sleepyprint (n) (declare (xargs :guard (natp n))) (if (zp n) nil (progn$ (cw "Sleepy print: ~x0~%" n) (sleep$ 1) (sleepyprint (- n 1)))))
other
(defttag :bridge)
other
(include-raw "bridge-sbcl-raw.lsp")
other
(defsection in-main-thread :parents (bridge) :short "Special mechanism for making sure forms execute in the main thread." :long "<p>This is a special form that is only meant to be used by ACL2 Bridge clients when they issue commands. A syntax example is:</p> @({ (bridge::in-main-thread (memoize 'fib) (fib 37)) }) <p>This is really just a hack that lets you use commands that, for one reason or another, must only ever be executed in the "main" thread (in CCL parlance, the "initial listener" thread; on SBCL, the initial thread). Practical applications include:</p> <ul> <li>Running memoized functions (the memoization code isn't thread-safe, and attempts to use a memoized function in multiple thread can result in hard errors), and</li> <li>Doing computations that involve a lot of @(see hons)ing (otherwise, each thread has its own hons space, and you may not get the sharing you are expecting).</li> </ul> <p>If the main thread is busy with work from other clients, this form will wait until it becomes available again. See also @(see try-in-main-thread), which instead just causes an error if the main thread is busy.</p>" (defmacro-last run-in-main-thread) (defmacro in-main-thread (&rest forms) `(run-in-main-thread :irrelevant-val-for-return-last (progn$ . ,BRIDGE::FORMS))))
other
(defsection try-in-main-thread :parents (bridge) :short "Alternative to @(see in-main-thread) that exits immediately if the main thread is already busy with something else." (defmacro-last try-to-run-in-main-thread) (defmacro try-in-main-thread (&rest forms) `(try-to-run-in-main-thread :irrelevant-val-for-return-last (progn$ . ,BRIDGE::FORMS))))