Final tweak to the work on unused variables

[msprotz]

This is the final tweak on that series of PRs I just merged. Best explained via an excerpt of the diff this generates in HACL*:

@@ -208,15 +208,15 @@ encrypt_aes128_gcm(
   uint8_t *tag
 )
 {
-  KRML_HOST_IGNORE(s);
-  KRML_HOST_IGNORE(iv);
-  KRML_HOST_IGNORE(iv_len);
-  KRML_HOST_IGNORE(ad);
-  KRML_HOST_IGNORE(ad_len);
-  KRML_HOST_IGNORE(plain);
-  KRML_HOST_IGNORE(plain_len);
-  KRML_HOST_IGNORE(cipher);
-  KRML_HOST_IGNORE(tag);
+  KRML_MAYBE_UNUSED_VAR(s);
+  KRML_MAYBE_UNUSED_VAR(iv);
+  KRML_MAYBE_UNUSED_VAR(iv_len);
+  KRML_MAYBE_UNUSED_VAR(ad);
+  KRML_MAYBE_UNUSED_VAR(ad_len);
+  KRML_MAYBE_UNUSED_VAR(plain);
+  KRML_MAYBE_UNUSED_VAR(plain_len);
+  KRML_MAYBE_UNUSED_VAR(cipher);
+  KRML_MAYBE_UNUSED_VAR(tag);
   #if HACL_CAN_COMPILE_VALE
   if (s == NULL)
   {
@@ -236,12 +236,7 @@ encrypt_aes128_gcm(
   uint32_t bytes_len = len * (uint32_t)16U;
   uint8_t *iv_b = iv;
   memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t));
-  KRML_HOST_IGNORE(compute_iv_stdcall(iv_b,
-      (uint64_t)iv_len,
-      (uint64_t)len,
-      tmp_iv,
-      tmp_iv,
-      hkeys_b));
+  compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b);

• KRML_HOST_IGNORE becomes KRML_MAYBE_UNUSED (@polubelova's suggestion, thanks!)
• if the IGNORE would placed in statement position, it is automatically skipped, since C automatically discards the return value by default without warning

@tahina-pro I believe this impacts Everparse (slightly), since you may have to rename the macro... so I'll you comment and/or approve, then merge whenever is right... thanks!

[msprotz]

For the record, I could decorate variable declarations with __attribute__((unused)) which means "variable may be unused". The code above would become

... encrypt_aes128_gcm(..., __attribute__((unused)) uint8_t *tag)

but that's a gcc-ism and I couldn't convince myself that there's something equivalent for MSVC

[tahina-pro]

In EverParse, when doing:

OTHERFLAGS='--admit_smt_queries true make -j lowparse &&
OTHERFLAGS='--admit_smt_queries true make -j -C tests/lowparse Example12

the test fails when compiling the generated code from LowParseExample12, with the following gcc error:

✘ [CC,Example12/LowParseExample12.c] (use -verbose to see the output)
Example12/LowParseExample12.c: In function ‘validate_t’:
Example12/LowParseExample12.c:925:9: error: statement with no effect [-Werror=unused-value]
  925 |       x - (uint8_t)128U;
      |       ~~^~~~~~~~~~~~~~~
Example12/LowParseExample12.c: In function ‘jump_t’:
Example12/LowParseExample12.c:1014:8: error: statement with no effect [-Werror=unused-value]
 1014 |     x1 - (uint8_t)128U;
      |     ~~~^~~~~~~~~~~~~~~
Example12/LowParseExample12.c:1025:7: error: statement with no effect [-Werror=unused-value]
 1025 |     x - (uint8_t)128U;
      |     ~~^~~~~~~~~~~~~~~
Example12/LowParseExample12.c: At top level:
cc1: error: unrecognized command line option ‘-Wno-unknown-warning-option’ [-Werror]
cc1: all warnings being treated as errors

Warning 3: run_or_warn: the following command failed:
gcc-9 -I /home/tahina/everest/master/karamel/krmllib/dist/minimal -I /home/tahina/everest/master/karamel/krmllib -I /home/tahina/everest/master/karamel/include -I Example12 -Wall -Werror -Wno-unknown-warning-option -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c Example12/LowParseExample12.c -o Example12/LowParseExample12.o
Warning 3 is fatal, exiting.

By contrast, with Karamel master, Example12 succeeds, with the following contents in Example12/LowParseExample12.c:

 925 |       KRML_HOST_IGNORE(x - (uint8_t)128U);
1014 |     KRML_HOST_IGNORE(x1 - (uint8_t)128U);
1025 |     KRML_HOST_IGNORE(x - (uint8_t)128U);

[tahina-pro]

Also, this PR still produces some outstanding KRML_HOST_IGNORE, such as (in the same test):

 923 |       KRML_HOST_IGNORE((uint8_t)0U);
1012 |     KRML_HOST_IGNORE((uint8_t)0U);
1023 |     KRML_HOST_IGNORE((uint8_t)0U);

Is this intended?

[msprotz]

Thanks Tahina for testing, this is super helpful! I've refined the criterion that ignores the return value of a function call to only apply to function calls, not the application of a builtin operator. In other words,

ignore(f(...)); ... becomes f(...); ...

whereas ignore(a + b); ... becomes KRML_IGNORE(a+b); ...

now the question remains as to why these IGNORE nodes remain in the AST and why they haven't been eliminated earlier when the argument to IGNORE was very clearly a value that can be eliminated -- how much do you care? I could take a look, or merge now (provided your example compiles) and investigate later for your use-case. let me know

[tahina-pro]

Thanks Jonathan for your fix! Example12 now seems to work better.

now the question remains as to why these IGNORE nodes remain in the AST and why they haven't been eliminated earlier when the argument to IGNORE was very clearly a value that can be eliminated -- how much do you care? I could take a look, or merge now (provided your example compiles) and investigate later for your use-case. let me know

Sorry, I meant that there are some leftover mentions of KRML_HOST_IGNORE in the generated code for Example12, and I wonder whether they should be renamed into KRML_MAYBE_UNUSED_VAR. If so, then there is no need to remove them once renamed properly.

[msprotz]

No I would leave that as KRML_HOST_IGNORE -- my intent is that KRML_MAYBE_UNUSED_VAR only applies to variables (as the name implies), and that KRML_HOST_IGNORE applies to the rest -- the stuff that we do want to ignore. Even though both macros are identical, I think this signals the intent better.

[msprotz]

FYI I just pushed a commit that gets rid of the extra KRML_IGNORE on your specific example. (It was triggered by a situation of the form let unused_variable = match e with | ... -> | ... which krml would turn into let unused_variable = match e with | ... -> ignore (...) | ... -> ignore (...) only to later on compile the pattern-match and result in calls to IGNORE for values.

Now the syntactic analysis determines that the entire match is a pure subexpression and can be eliminated altogether, rather than pushing ignore at the leaves.

I suspect this might improve things for you a bunch -- for HACL*, the impact of that most recent commit was completely minor. Let me know what you think.

[tahina-pro]

Thanks for your attempt. Now I have the following error, this time on merkle-tree:

MerkleTree.c: In function 'MerkleTree_Low_mt_get_path_':
MerkleTree.c:1119:5: error: statement with no effect [-Werror=unused-value]
1119 |     *p;
     |     ^~
MerkleTree.c: At top level:
make[1]: *** [<builtin>: MerkleTree.o] Error 1
make[1]: Leaving directory '/home/test/merkle-tree/dist'
make: *** [Makefile:109: dist/libmerkletree.a] Error 2
make: Leaving directory '/home/test/merkle-tree'

[msprotz]

Thanks, I pushed a fix for that particular issue. I tried a full everest build but everparse returns errors about a diff that has changed. Do you have instructions for me to test locally?

[tahina-pro]

Thanks, I pushed a fix for that particular issue. I tried a full everest build but everparse returns errors about a diff that has changed. Do you have instructions for me to test locally?

Did you use EverParse branch _taramana_krml_385 (cf. project-everest/everparse#104)? This branch should already have those diffs fixed; you can do make -j 3d-doc-test there to check by yourself. If not, you can do make -j -C doc 3d-snapshot on that branch to fix those diffs.

I have Everest branch taramana_krml_385 which is using this EverParse branch and your Karamel branch. A CI task is running right now on that Everest branch.

[msprotz]

Thanks, I have a locally successful build using your everest branch and hopefully CI will agree and come back green soon. Thanks!

[tahina-pro]

Everest green now. Thank you again!