[Question][Hw4] Cannot find lhs of i32

[leporia]

Name: Andrea Lepori

When having a print call that takes as argument an immediate LLVM throws the error Cannot find lhs of i32 5. I tried to search everywhere and tried to find the instruction that throw this error but I was unsuccessful. It is before the code that we are supposed to implement.

I imagine this is a problem in the template? As it is thrown before the execution of any of my code.

[Re-st]

Sorry to see some possible bug.
Can you give the code? Do you mean you tried print(int x) and it didn't work?
I immediately tried below;

#include "homework.h"

int main() {
  int x = input();
  int z;
  if (x >= 0) {
    z = 10 / x; // error
    if (x < 0) {
      z = 10 / x; // unreachable
    }
  } else {
    z = 10 / x; // safe
  }
  z = 10 / x; // error
  print(z);
  return 0;
}

As you know, this is example1.c, and it worked fine.

[jaehyun1ee]

I've struggled with the same problem, and it seems like the given check_instr function assumes that the argument to a print call is an llvm value corresponding to some instruction.

let check_instr llctx instr memory =
    match Llvm.instr_opcode instr with
    | Llvm.Opcode.Call when Llvmutils.is_print instr ->
        let arg = Llvm.operand instr 0 in
        let v = Semantics.eval arg memory in
        F.printf "%s @@ %s : %a\n"
          (Llvmutils.string_of_lhs arg) (* here *)
          (Llvmutils.string_of_location llctx instr)
          Memory.Value.pp v

Thus, if we use print in the test file in either patterns:

print(1);

int a = 1;
print(a); // clang propagates the value 1 to a, so in llvm ir, it is a call to print with i32 1

it yields the Cannot find lhs of ... error.

A quick fix on your side may be avoiding such patterns, but it would be great if the template code is updated with pattern-matches on the lhs arg of call instructions :)

[Re-st]

I'm sorry to see we have lost opportunity to fix the bug.
@jaehyun1ee is right.
You can evade the bug by the code snippet, pointed out by @jaehyun1ee , as below.

let check_instr llctx instr memory =
    match Llvm.instr_opcode instr with
    | Llvm.Opcode.Call when Llvmutils.is_print instr ->
        let arg = Llvm.operand instr 0 in
        let v = Semantics.eval arg memory in
        F.printf "%s @@ %s : %a\n"
          (Llvmutils.string_of_exp arg)
          (Llvmutils.string_of_location llctx instr)
          Memory.Value.pp v

Llvmutils.string_of_exp is defined at https://prosyslab-classroom.github.io/llvmutils/llvmutils/Llvmutils/index.html#val-string_of_exp

[Re-st]

@leporia , please check if this fixes the bug.
If it's good enough, I'll find out if it is possible to update the template code structure.
Thanks.

[leporia]

The snipped provided is the same as the one in the original template. But here is the fix that I've implemented.
@jaehyun1ee Thanks for pointing out the location of the bug!

let check_instr llctx instr memory =
    match Llvm.instr_opcode instr with
    | Llvm.Opcode.Call when Llvmutils.is_print instr -> (
        let arg = Llvm.operand instr 0 in
        let v = Semantics.eval arg memory in
        match Llvm.classify_value arg with
        | Llvm.ValueKind.ConstantInt ->
            F.printf "%s @@ %a\n"
              (Llvmutils.string_of_location llctx instr)
              Memory.Value.pp v
        | Llvm.ValueKind.Instruction _ ->
            F.printf "%s @@ %s : %a\n"
              (Llvmutils.string_of_lhs arg)
              (Llvmutils.string_of_location llctx instr)
              Memory.Value.pp v
        | _ -> failwith "Unsupported value")

I think there is also a bug in the execution of the tests in dune. As they don't take into account the print statements and cut the output incorrectly. run cut -f1 -d, only removes after the , but a print statement doesn't have it. I assume this is needed for the interval domain to have a more relaxed check.

[Re-st]

@leporia, I was mentioning about #186 (comment). It is different from original code.

Your solution seems good too!

For your next argument, yes, interval domain has a more relaxed check by cutting after the comma.
If you want to add custom testcases that has print statements, you can delete the 'run cut -f1 -d,' if that incurs crash.

[Re-st]

Currently we don't grade your custom testcases. We just encourage you to, before submission, test your code by yourself.
If you test your code enough to exceed the coverage bound, it's good.
You change your dune file at /test for

1. test your code by yourself
2. let the coverage checker recognize your new testcases.

[leporia]

I'm sorry I totally missed the edit. Thanks a lot for the support!