SRI-CSL / OCCAM

OCCAM: Object Culling and Concretization for Assurance Maximization
BSD 3-Clause "New" or "Revised" License
26 stars 10 forks source link

Configuration Priming removing function when it shouldn't #39

Closed mudbri closed 3 years ago

mudbri commented 3 years ago

In the given code below, configuration priming removes the function sampleFunc even though it could be called if the second command line argument is 'd' or 'c'.

// this is hello.c
#include <stdio.h>

int sampleFunc (char character) {
    if (character == 'a') {
        return 'a';
    }
    return 'b';
}

int main(int argc, char *argv[]) {
  char character = 'b';

  char arg_character = argv[2][0];

  if (argv[2][0] == 'c') {
      arg_character = 'd';
  }

  if(argv[1][0] == 'a' || arg_character == 'd') {
      character = sampleFunc(argv[1][0]);
  }

  return 0;
}

The manifest file (named hello.manifest) is:

{ "main" : "hello.bc"
, "binary"  : "hello"
, "modules"    : []
, "native_libs" : []
, "name"    : "hello"
, "static_args" : ["b"]
, "dynamic_args" : "1"
}

The bitcode is generated using: gclang hello.c -o hello get-bc hello

and OCCAM is run with the following options: slash --work-dir=slash --no-strip --intra-spec-policy=none --inter-spec-policy=none --disable-inlining --enable-config-prime hello.manifest

caballa commented 3 years ago

This has nothing to do with config-prime. LLVM decides that your main function is pretty much empty. The variable character is not used so the call to sampleFunc is dead code because it does not have any side-effect. By transitivity the whole main body is dead code.

If you add some side-effect to sampleFunc (e.g., add some printf) then the call cannot be removed.

mudbri commented 3 years ago

The function is being removed even if I print something in sampleFunc.

int sampleFunc (char character) {
    printf("In sample function\n");
    if (character == 'a') {
        return 'a';
    }
    return 'b';
}

The behavior changes if I make slight changes in the main function though. For example, this code does not remove sampleFunc:

int main(int argc, char *argv[]) {
  char character = 'b';

  char arg_character = argv[2][0];

  if (argv[2][0] == 'c') {
      arg_character = 'e';
  }

  if(argv[1][0] == 'a' || arg_character == 'e') {
      character = sampleFunc(argv[1][0]);
  }

  return 0;
}

I have only replaced 'd' with 'e' but for some reason this prevents the sampleFunc from being removed.

Moreover, sampleFunc is not removed if I do not provide the --enable-config-prime flag to slash.

caballa commented 3 years ago

issue39.zip

I cannot reproduce your problem. I attach a zip file with all the files generated by OCCAM. Go to slash directory and open the file test-final.ll. You should see the function sampleFunc there. Moreover, you should see that that sampleFunc has been actually specialized since OCCAM infers that it is always called with the character b. But the specialized function is still there. You can try by yourself by doing:

make clean
./build.sh
mudbri commented 3 years ago

Thank you! I tried it on a fresh VM and it worked fine. It seems like an issue with my environment.