Crucible/LLVM: Error when function returns pointer inside new allocation

[langston-barrett]

This same sort of thing works fine with a function/spec that returns a pointer to the base of an allocation.

/*
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; clang_7" --run "clang -g -O1 -emit-llvm -c *.c"
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; llvm_7" --run "llvm-dis *.bc"
*/

#include "stdlib.h"
#include "string.h"

char *zeroes(int len) {
  char* data = malloc(len*sizeof(char));
  memset(data, 0, len);
  return data+1;
}

m <- llvm_load_module "test.bc";
let spec = do {
  crucible_execute_func [crucible_term {{ 10 : [32] }}];
  ptr <- crucible_alloc (llvm_array 10 (llvm_int 8));
  crucible_points_to ptr (crucible_term {{ zero : [10][8] }});
  crucible_return (crucible_elem ptr 1);
};
crucible_llvm_verify m "zeroes" [] false spec z3;

[22:21:29.144] resolveSetupVal: Unresolved prestate variable:AllocIndex 0

[brianhuffman]

I think the reason for the failure is that function matchArg in module Crucible.LLVM.Override doesn't have a case where the expected value (the last argument) is a SetupElem. I believe it's hitting the catch-all error case, which calls mkStructuralMismatch, which in turn fails when it calls resolveSetupValue while it's trying to pretty-print a nice error message.

To fix this (and potential related problems), I think we just need to add more cases to matchArg: we need to handle expected values with SetupElem and SetupField; we should also implement SetupArray while we're at it (this last one should be very similar to SetupStruct which is implemented).

[langston-barrett]

Looks like I'll have to do the case for SetupElem to fix #524

[langston-barrett]

This was not fixed by #519 after all (the additional matchArg case). There is probably a missing call to assignVar somewhere...

[brianhuffman]

This was fixed by #989.