crucible and dot product example

[Johanvdberg]

I am trying to to convert the dot product example so that it uses crucible command. I get errors that does not make sense for me. The saw script:

import "dotprod.cry";
let dotprod_setup = do {
  crucible_fresh_pointer "x" (crucible_array  12 (llvm_int 8));
  x <- crucible_fresh_var "*x" (crucible_array  12 (llvm_int 8));
  crucible_fresh_pointer "y" (crucible_array  12 (llvm_int 8));
  y <- crucible_fresh_var "*y" (crucible_array  12 (llvm_int 8));
  size <- crucible_fresh_var "size" (llvm_int 32);
  crucible_execute_func [crucible_term x, crucible_term y];
};

let main : TopLevel () = do {
    m <- llvm_load_module "dotprod.bc";
    crucible_llvm_verify m "dotprod" [] false dotprod_setup abc;
    print "Done.";
};

The errors I get are:

Loading module Main
saw: user error (Error
  type mismatch: Int -> t.22 and [SetupValue] -> SetupValue
 at "dotprod_setup" (/home/johan/Documents/cryptol/dotprod.saw:3:5)
mismatched type constructors: Int and ([])

  type mismatch: String -> t.18 and LLVMType -> CrucibleSetup SetupValue
 at "dotprod_setup" (/home/johan/Documents/cryptol/dotprod.saw:3:5)
type mismatch: String and LLVMType at "dotprod_setup" (/home/johan/Documents/cryptol/dotprod.saw:3:5)

...... and some more.

The version of saw-script: 0.2 (b37faa8)

[atomb]

The structure of the Crucible interface is fairly different from the old LLVM interface. I just added a dotprod_struct-crucible.saw in the examples/llvm directory to contrast with dotprod_struct.saw for an illustration of the differences.

[Johanvdberg]

A step wise approach to structures I use a C function and structure

typedef struct {
    uint32_t a;
    uint32_t b;
} add_structure;

uint32_t add_struct(add_structure data) {
    return data.a +  data.b;
}

and in a saw-script the part

let add_struct n = do {
    a <- crucible_term {{ a:[32]}};
    b <- crucible_term {{ b:[32]}};
   //define the structure 
    let data = crucible_struct [ a, b ];
   //define input of the function
    crucible_execute_func [data];
    crucible_return (crucible_term {{ a  + b }});
};

define the specification for the auditing the two components of the structure, but the the error

Type errors:
  /..../add/add.saw:20:20-26:2: type mismatch: t.1 t.4 and SetupValue
 at "add_struct" (/Users/johan/simon/add/add.saw:20:5-20:15)
type mismatch: t.1 t.4 and SetupValue at "add_struct" (/..../add/add.saw:20:5-20:15)

  /...../add/add.saw:20:20-26:2: type mismatch: t.1 t.2 and SetupValue
 at "add_struct" (/Users/johan/simon/add/add.saw:20:5-20:15)
type mismatch: t.1 t.2 and SetupValue at "add_struct" (/..../add/add.saw:20:5-20:15) 

Version of saw script: 0.2 (bbbb4ad-dirty)

[Johanvdberg]

Updating the example to

let add_struct  = do {
    a <- crucible_fresh_var "a" (llvm_int 32);
    b <- crucible_fresh_var "b" (llvm_int 32);
    let data = crucible_struct [ a, b ];
    let data2 =  crucible_fresh_var
        "data2"
        (llvm_struct "struct.add_structure");
    crucible_execute_func [data];
    crucible_return (crucible_term {{ a + b }});
};

the error is given by

add.saw:29:16-29:40: type mismatch: [Term] -> t.9 and [SetupValue] -> SetupValue
 at "data" (add.saw:29:9-29:13)
type mismatch: Term and SetupValue at "data" (add.saw:29:9-29:13)

and using

crucible_execute_func [data2];
crucible_return (crucible_term {{ data2.2 + data2.1 }});

does not help.

[weaversa]

The problem with data above is that crucible_fresh_var returns a Term and crucible_struct takes a list of SetupValue.

This should fix data:

let data = crucible_struct [ crucible_term a, crucible_term b];

The problem with data2 is similar in that crucible_execute_func needs a SetupValue and data2 is a Term.

This should fix data2.

crucible_execute_func [crucible_term data2];

I can't test these because Clang 7 keeps changing the input type of add_struct to i64 (essentially concatenating the struct elements together).

Types:
  %struct.add_structure = type { i32, i32 }

Globals:

External references:
  declare void @llvm.dbg.declare(metadata, metadata, metadata)

Definitions:
  i32 @add_struct(i64 %0)

So, maybe this issue is now moot?

[atomb]

I think you're right, @weaversa. Closing.