Support FFI on Windows

This patch: * Adds the appropriate conditional logic to use the `Win32` library to dynamically load shared libraries on Windows. * Tweaks some FFI-related test cases to make them work portably on Windows. I have left comments describing each of the non-obvious tweaks that I had to make. * Updates the reference manual accordingly. Fixes #1394.
GaloisInc · Sep 24, 2022 · 27ac8d9 · 27ac8d9
1 parent 146934b
commit 27ac8d9
Show file tree

Hide file tree

Showing 53 changed files with 4,438 additions and 14,047 deletions.
diff --git a/cryptol.cabal b/cryptol.cabal
@@ -92,8 +92,11 @@ library
 
   if flag(ffi)
     build-depends:     hgmp,
-                       libffi            >= 0.2,
-                       unix
+                       libffi            >= 0.2
+    if os(windows)
+      build-depends:   Win32
+    else
+      build-depends:   unix
     cpp-options:       -DFFI_ENABLED
 
   Build-tool-depends:  alex:alex, happy:happy

diff --git a/docs/RefMan/FFI.rst b/docs/RefMan/FFI.rst
@@ -7,8 +7,9 @@ C (or other languages that use the C calling convention).
 Platform support
 ----------------
 
-The FFI is currently **not supported on Windows**, and only works on Unix-like
-systems (macOS and Linux).
+The FFI is built on top of the C ``libffi`` library, and as such, it should be
+portable across many operating systems. We have tested it to work on Linux,
+macOS, and Windows.
 
 Basic usage
 -----------
@@ -52,6 +53,7 @@ extension it uses is platform-specific:
 
 * On Linux, it looks for the extension ``.so``.
 * On macOS, it looks for the extension ``.dylib``.
+* On Windows, it looks for the extension ``.dll``.
 
 For example, if you are on Linux and your ``foreign`` declaration is in
 ``Foo.cry``, Cryptol will dynamically load ``Foo.so``. Then for each ``foreign``
@@ -90,6 +92,7 @@ simple usages, you can do this manually with the following commands:
 
 * Linux: ``cc -fPIC -shared Foo.c -o Foo.so``
 * macOS: ``cc -dynamiclib Foo.c -o Foo.dylib``
+* Windows: ``cc -fPIC -shared Foo.c -o Foo.dll``
 
 Converting between Cryptol and C types
 --------------------------------------

diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree
diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree
diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree
diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree
diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree
diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree
diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree
diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree
diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle
diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 41758cdb8fafe65367e2aa727ac7d826
+config: 69485412ee215e2257ea16f8a42506fe
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html
diff --git a/docs/RefMan/_build/html/BasicTypes.html b/docs/RefMan/_build/html/BasicTypes.html
diff --git a/docs/RefMan/_build/html/Expressions.html b/docs/RefMan/_build/html/Expressions.html
diff --git a/docs/RefMan/_build/html/FFI.html b/docs/RefMan/_build/html/FFI.html
diff --git a/docs/RefMan/_build/html/Modules.html b/docs/RefMan/_build/html/Modules.html
diff --git a/docs/RefMan/_build/html/OverloadedOperations.html b/docs/RefMan/_build/html/OverloadedOperations.html
diff --git a/docs/RefMan/_build/html/RefMan.html b/docs/RefMan/_build/html/RefMan.html
@@ -1,42 +1,84 @@
+
+
 <!DOCTYPE html>
-<html class="writer-html5" lang="en" >
+<!--[if IE 8]><html class="no-js lt-ie9" lang="en" > <![endif]-->
+<!--[if gt IE 8]><!--> <html class="no-js" lang="en" > <!--<![endif]-->
 <head>
-  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
-
-  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
+  <meta charset="utf-8">
+
+  <meta name="viewport" content="width=device-width, initial-scale=1.0">
+
   <title>Cryptol Reference Manual &mdash; Cryptol 2.11.0 documentation</title>
-      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
-      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
-  <!--[if lt IE 9]>
-    <script src="_static/js/html5shiv.min.js"></script>
-  <![endif]-->
 
-        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
+
+
+
+
+
+
+
+  <script type="text/javascript" src="_static/js/modernizr.min.js"></script>
+
+
+      <script type="text/javascript" id="documentation_options" data-url_root="./" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
         <script src="_static/underscore.js"></script>
         <script src="_static/doctools.js"></script>
-    <script src="_static/js/theme.js"></script>
+
+    <script type="text/javascript" src="_static/js/theme.js"></script>
+
+
+
+
+  <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
+  <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
     <link rel="index" title="Index" href="genindex.html" />
     <link rel="search" title="Search" href="search.html" />
     <link rel="next" title="Basic Syntax" href="BasicSyntax.html" /> 
 </head>
 
-<body class="wy-body-for-nav"> 
+<body class="wy-body-for-nav">
+
+
   <div class="wy-grid-for-nav">
+
     <nav data-toggle="wy-nav-shift" class="wy-nav-side">
       <div class="wy-side-scroll">
         <div class="wy-side-nav-search" >
+
+
+
             <a href="#" class="icon icon-home"> Cryptol
+
+
+
           </a>
+
+
+
+
+
+
+
 <div role="search">
   <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
     <input type="text" name="q" placeholder="Search docs" />
     <input type="hidden" name="check_keywords" value="yes" />
     <input type="hidden" name="area" value="default" />
   </form>
 </div>
-        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
-              <p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
+
+
+        </div>
+
+        <div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="main navigation">
+
+
+
+
+
+
+              <p class="caption"><span class="caption-text">Cryptol Reference Manual</span></p>
 <ul>
 <li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
 <li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
@@ -47,34 +89,72 @@
 <li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
 </ul>
 
+
+
         </div>
       </div>
     </nav>
 
-    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
+    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap">
+
+
+      <nav class="wy-nav-top" aria-label="top navigation">
+
           <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
           <a href="#">Cryptol</a>
+
       </nav>
 
+
       <div class="wy-nav-content">
+
         <div class="rst-content">
-          <div role="navigation" aria-label="Page navigation">
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+<div role="navigation" aria-label="breadcrumbs navigation">
+
   <ul class="wy-breadcrumbs">
-      <li><a href="#" class="icon icon-home"></a> &raquo;</li>
+
+      <li><a href="#">Docs</a> &raquo;</li>
+
       <li>Cryptol Reference Manual</li>
+
+
       <li class="wy-breadcrumbs-aside">
+
+
             <a href="_sources/RefMan.rst.txt" rel="nofollow"> View page source</a>
+
+
       </li>
+
   </ul>
+
+
   <hr/>
 </div>
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
-             
-  <section id="cryptol-reference-manual">
-<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this headline"></a></h1>
+
+  <div class="section" id="cryptol-reference-manual">
+<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this headline">¶</a></h1>
 <div class="toctree-wrapper compound">
-<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
+<p class="caption"><span class="caption-text">Cryptol Reference Manual</span></p>
 <ul>
 <li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a><ul>
 <li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#declarations">Declarations</a></li>
@@ -179,36 +259,53 @@ <h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manua
 </li>
 </ul>
 </div>
-</section>
+</div>
 
 
            </div>
+
           </div>
-          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
-        <a href="BasicSyntax.html" class="btn btn-neutral float-right" title="Basic Syntax" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
+          <footer>
+
+    <div class="rst-footer-buttons" role="navigation" aria-label="footer navigation">
+
+        <a href="BasicSyntax.html" class="btn btn-neutral float-right" title="Basic Syntax" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right"></span></a>
+
+
     </div>
+
 
   <hr/>
 
   <div role="contentinfo">
-    <p>&#169; Copyright 2021, The Cryptol Team.</p>
-  </div>
+    <p>
+        &copy; Copyright 2021, The Cryptol Team
 
-  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
-    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
-    provided by <a href="https://readthedocs.org">Read the Docs</a>.
-
+    </p>
+  </div>
+  Built with <a href="http://sphinx-doc.org/">Sphinx</a> using a <a href="https://github.com/rtfd/sphinx_rtd_theme">theme</a> provided by <a href="https://readthedocs.org">Read the Docs</a>. 
 
 </footer>
+
         </div>
       </div>
+
     </section>
+
   </div>
-  <script>
+
+
+
+  <script type="text/javascript">
       jQuery(function () {
           SphinxRtdTheme.Navigation.enable(true);
       });
-  </script> 
+  </script>
+
+
+
+
+
 
 </body>
 </html>