Merge pull request #1538 from GaloisInc/T1493

saw-remote-api: Reach parity with SAWScript for global option settings

Author: mergify[bot]

saw-remote-api/CHANGELOG.md

@@ -3,7 +3,9 @@
 
 ## 0.9.1 -- YYYY-MM-DD
 
-* NEW CHANGELOG ENTRIES SINCE 0.9.0 GO HERE
+* `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`,
+  which controls whether to enable or disable What4 translation for SAWCore
+  expressions during Crucible symbolic execution.
 
 
 ## 0.9.0 -- 2021-11-19

saw-remote-api/docs/SAW.rst

@@ -515,7 +515,7 @@ Parameter fields
 
 
 ``option``
-  The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``debug intrinsics``, ``SMT array memory model``, or ``What4 hash consing``
+  The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``debug intrinsics``, ``SMT array memory model``, ``What4 hash consing``, or ``What4 eval``
 
 
 

saw-remote-api/python/CHANGELOG.md

@@ -2,7 +2,11 @@
 
 ## 0.9.1 -- YYYY-MM-DD
 
-* NEW CHANGELOG ENTRIES SINCE 0.9.0 GO HERE
+* Add a `set_option` command to `saw_client` that allows enabling and disabling
+  global SAW options. For example, SAWScript's `enable_lax_pointer_ordering` is
+  equivalent to `set_option(LaxPointerOrdering(), True)` in `saw-client.
+  `LaxPointerOrdering`, as well as all other possible options, can be imported
+  from the `saw_client.option` module.
 
 
 ## 0.9.0 -- 2021-11-19

saw-remote-api/python/saw_client/__init__.py

@@ -14,6 +14,7 @@
 from argo_client.connection import ServerConnection
 from . import llvm
 from . import exceptions
+from . import option
 from . import proofscript
 
 __designated_connection = None  # type: Optional[connection.SAWConnection]
@@ -357,7 +358,7 @@ def on_finish(self) -> None:
     def on_abort(self) -> None:
         print("🛑  Aborting proof script.", file=self.file)
 
-        
+
 def view(v: View) -> None:
     """Add a view to the global list of views. Future verification results will
        be handed to this view, and its on_finish() handler will be called at
@@ -648,6 +649,12 @@ def prove(goal: cryptoltypes.CryptolJSON,
         pr.counterexample = None
     return pr
 
+def set_option(option : option.SAWOption, value : bool) -> None:
+    """Set a boolean-valued SAW option."""
+    global __designated_connection
+    if __designated_connection is not None:
+        __designated_connection.set_option(option=option,value=value)
+
 @atexit.register
 def script_exit() -> None:
     global __designated_views

saw-remote-api/python/saw_client/commands.py

@@ -4,6 +4,7 @@
 from cryptol import cryptoltypes
 from . import exceptions
 from .proofscript import *
+from .option import *
 
 from typing import Any, List
 
@@ -199,3 +200,15 @@ def __init__(self, connection : argo.HasProtocolState) -> None:
             {},
             connection
         )
+
+
+class SAWSetOption(SAWCommand):
+    def __init__(self, connection : argo.HasProtocolState,
+                 option : SAWOption, value : bool,
+                 timeout : Optional[float]) -> None:
+        params = {'option': str(option),
+                  'value': value}
+        super(SAWSetOption, self).__init__('SAW/set option', params, connection, timeout=timeout)
+
+    def process_result(self, _res : Any) -> Any:
+        return None

saw-remote-api/python/saw_client/connection.py

@@ -6,6 +6,7 @@
 from argo_client.connection import ServerConnection, DynamicSocketProcess, HttpProcess, ManagedProcess
 from argo_client.interaction import Interaction, Command
 from .commands import *
+from .option import *
 from typing import Optional, Union, Any, List, TextIO
 
 # FIXME cryptol_path isn't always used...?
@@ -237,3 +238,11 @@ def prove(self,
         """
         self.most_recent_result = Prove(self, goal, proof_script, timeout)
         return self.most_recent_result
+
+    def set_option(self,
+                   option : SAWOption,
+                   value : bool,
+                   timeout : Optional[float] = None) -> Command:
+        """Set a boolean-valued SAW option."""
+        self.most_recent_result = SAWSetOption(self, option, value, timeout)
+        return self.most_recent_result

saw-remote-api/python/saw_client/option.py

@@ -0,0 +1,43 @@
+from abc import ABCMeta, abstractmethod
+from dataclasses import dataclass
+from typing import Any
+
+class SAWOption(metaclass=ABCMeta):
+    @abstractmethod
+    def __str__(self) -> str: pass
+
+
+@dataclass
+class LaxArithmetic(SAWOption):
+    def __str__(self) -> str:
+        return "lax arithmetic"
+
+
+@dataclass
+class LaxPointerOrdering(SAWOption):
+    def __str__(self) -> str:
+        return "lax pointer ordering"
+
+
+@dataclass
+class DebugIntrinsics(SAWOption):
+    def __str__(self) -> str:
+        return "debug intrinsics"
+
+
+@dataclass
+class SMTArrayMemoryModel(SAWOption):
+    def __str__(self) -> str:
+        return "SMT array memory model"
+
+
+@dataclass
+class What4HashConsing(SAWOption):
+    def __str__(self) -> str:
+        return "What4 hash consing"
+
+
+@dataclass
+class What4Eval(SAWOption):
+    def __str__(self) -> str:
+        return "What4 eval"

saw-remote-api/python/tests/saw/test-files/Makefile

@@ -5,3 +5,7 @@ all: $(BC_FILES)
 
 %.bc: %.c
 	clang -g -c -emit-llvm -o $@ $<
+
+# This test case crucially relies on the use of -O2.
+llvm_lax_pointer_ordering.bc: llvm_lax_pointer_ordering.c
+	clang -O2 -g -c -emit-llvm -o $@ $<

saw-remote-api/python/tests/saw/test-files/llvm_lax_pointer_ordering.bc

@@ -0,0 +1,10 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+const size_t LEN = 42;
+
+void zip_with_add(uint64_t c[LEN], const uint64_t a[LEN], const uint64_t b[LEN]) {
+  for (size_t i = 0; i < LEN; i++) {
+    c[i] = a[i] + b[i];
+  }
+}

saw-remote-api/python/tests/saw/test-files/llvm_lax_pointer_ordering.c

@@ -0,0 +1,51 @@
+from pathlib import Path
+import unittest
+from saw_client import *
+from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, cryptol, i64, void
+from saw_client.option import LaxPointerOrdering
+
+
+LEN = 42
+
+
+def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None,
+                read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
+    """Add to ``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value.
+    If ``read_only == True`` then the allocated memory is immutable.
+
+    :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh
+             variable will be assigned ``name`` if provided/available.)"""
+    var = c.fresh_var(ty, name)
+    ptr = c.alloc(ty, points_to = var, read_only = read_only)
+    return (var, ptr)
+
+
+class ZipWithAddContract(Contract):
+    def specification(self):
+        array_t = array_ty(LEN, i64)
+        c_ptr = self.alloc(array_t)
+        (a, a_ptr) = ptr_to_fresh(self, name='a', ty=array_t, read_only=True)
+        (b, b_ptr) = ptr_to_fresh(self, name='b', ty=array_t, read_only=True)
+
+        self.execute_func(c_ptr, a_ptr, b_ptr)
+
+        self.points_to(c_ptr, cryptol(f'zipWith`{{ {LEN} }} (+) {a.name()} {b.name()}'))
+        self.returns(void)
+
+
+class LLVMPointerTest(unittest.TestCase):
+
+    def test_llvm_pointer(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'llvm_lax_pointer_ordering.bc'))
+        mod = llvm_load_module(bcname)
+
+        set_option(LaxPointerOrdering(), True)
+
+        result = llvm_verify(mod, 'zip_with_add', ZipWithAddContract())
+        self.assertIs(result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py

@@ -39,6 +39,8 @@ setOption opt =
          updateRW rw { rwSMTArrayMemoryModel = enabled }
        EnableWhat4HashConsing enabled ->
          updateRW rw { rwWhat4HashConsing = enabled }
+       EnableWhat4Eval enabled ->
+         updateRW rw { rwWhat4Eval = enabled }
      ok
 
 data SetOptionParams
@@ -47,6 +49,7 @@ data SetOptionParams
   | EnableDebugIntrinsics Bool
   | EnableSMTArrayMemoryModel Bool
   | EnableWhat4HashConsing Bool
+  | EnableWhat4Eval Bool
 
 parseOption :: Object -> String -> Parser SetOptionParams
 parseOption o name =
@@ -56,6 +59,7 @@ parseOption o name =
     "debug intrinsics" -> EnableDebugIntrinsics <$> o .: "value"
     "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value"
     "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value"
+    "What4 eval" -> EnableWhat4Eval <$> o .: "value"
     _ -> empty
 
 instance FromJSON SetOptionParams where
@@ -70,8 +74,9 @@ instance Doc.DescribedMethod SetOptionParams OK where
                      , Doc.Literal "lax arithmetic", Doc.Text ", "
                      , Doc.Literal "lax pointer ordering", Doc.Text ", "
                      , Doc.Literal "debug intrinsics", Doc.Text ", "
-                     , Doc.Literal "SMT array memory model", Doc.Text ", or "
-                     , Doc.Literal "What4 hash consing"
+                     , Doc.Literal "SMT array memory model", Doc.Text ", "
+                     , Doc.Literal "What4 hash consing", Doc.Text ", or "
+                     , Doc.Literal "What4 eval"
                      ])
     ]
   resultFieldDescription = []