Tuple setup values unsupported in the LLVM API

[weaversa]

I'm seeing "Tuple setup values unsupported in the LLVM API" show up as an error message while using the Python interface and saw-remote-api. The same proof has been working for years before a recent change here (I don't know which one). Does anyone have any ideas on what this error message means or what is causing this? Thank you.

[RyanGlScott]

Hm, it's possible that this was unintended fallout from my #1934 patch, which repurposed the "tuple" value in the remote API for MIR tuples. (What was previously referred to as "tuple" is now called "struct", as structs and tuples are different in MIR.) Out of curiosity, are you using the SAW Python bindings from the master branch of SAW, or are you using the SAW Python bindings from PyPI?

[weaversa]

Thanks @RyanGlScott -- I'm doing:

pip3 install saw-client

[RyanGlScott]

That would explain it then—you're using a version of the Python bindings meant for version 1.0 of the SAW remote API, but the remote API has changed in the master branch. You'd need to install the Python bindings from master if you want them to interoperate with the latest SAW nightly. There are instructions for how to do this (with Poetry) here—let me know if I can help further.

[weaversa]

Hi @RyanGlScott, I installed the bindings from master and am seeing the same error. Do you have any more ideas?

[RyanGlScott]

Hm, it's tricky to diagnose further without knowing a bit more about your setup. Can you give more details on the sequence of commands you're running to invoke the Python bindings?

[weaversa]

Here is the structure (untested) of the python that is causing problems. Here we have some implementation that initializes a struct and we're using SAW to verify that struct creation happens w/out error.

# Returns a tuple (struct, pointer to the struct)
def setup_parameters(c : Contract, pointer=None, read_only=False) -> Tuple[SetupVal, SetupVal]:
    
    a = cry("`a : [64]")
    b = cry("`b : [64]")
    params  = struct(a, b)

    if pointer == None:
        fresh_pointer = c.alloc(parameters_t, points_to=params, read_only=read_only)
        return (params, fresh_pointer)

    else:
        c.points_to(pointer, params)
        return (params, pointer)

class InitContract(Contract):
    def specification(self):
        (_, params_p) = setup_parameters(self)

        a = cry("`a : [64]")
        b = cry("`b : [64]")

        self.execute_func(params_p, a, b)

        self.returns_f("{SUCCESS} : [32]")

[RyanGlScott]

OK. Can you run the following sequence of commands and indicate what goes wrong?

1. From your saw-script checkout, navigate to saw-remote-api/python.

2. Put the following two files in this directory:

   #include <stdint.h>
   
   #define SUCCESS 1
   
   typedef struct {
     uint64_t a;
     uint64_t b;
   } parameters_t;
   
   uint32_t init(parameters_t *p, uint64_t a, uint64_t b) {
     return SUCCESS;
   }

   from pathlib import Path
   from saw_client import *
   from saw_client.crucible import cry, cry_f, struct
   from saw_client.llvm import Contract, SetupVal, alias_ty
   from typing import Tuple
   
   parameters_t = alias_ty('struct.parameters_t')
   SUCCESS = 1
   a = 27
   b = 42
   
   # Returns a tuple (struct, pointer to the struct)
   def setup_parameters(c : Contract, pointer=None, read_only=False) -> Tuple[SetupVal, SetupVal]:
   
       a = cry_f("{a} : [64]")
       b = cry_f("{b} : [64]")
       params  = struct(a, b)
   
       if pointer == None:
           fresh_pointer = c.alloc(parameters_t, points_to=params, read_only=read_only)
           return (params, fresh_pointer)
   
       else:
           c.points_to(pointer, params)
           return (params, pointer)
   
   class InitContract(Contract):
       def specification(self):
           (_, params_p) = setup_parameters(self)
   
           a = cry_f("{a} : [64]")
           b = cry_f("{b} : [64]")
   
           self.execute_func(params_p, a, b)
   
           self.returns_f("{SUCCESS} : [32]")
   
   if __name__ == "__main__":
       connect(reset_server=True)
       view(LogResults(verbose_failure=True))
       bcname = str(Path('test.bc'))
       mod = llvm_load_module(bcname)
   
       result = llvm_verify(mod, 'init', InitContract())
       print(result.is_success())

   (This is my attempt at filling out your templates in a complete, executable specification.)

3. Compile the test.c file with:

   $ clang -g -emit-llvm -c test.c -o test.bc
   

4. Run the test.py specification with:

   $ docker run --name=saw-remote-api -d -v $PWD:/home/saw -p 8080:8080 galoisinc/saw-remote-api:nightly
   $ poetry install
   $ SAW_SERVER_URL="http://localhost:8080/" poetry run python test.py
   

   If everything is set up correctly, this should succeed with:

   ✅  Verified: lemma_InitContract (defined at /home/ryanscott/Documents/Hacking/Haskell/saw-script/saw-remote-api/python/test.py:44)
   True
   ✅  The goal was verified!