[C2C] Extend proof generation.

Add support for non-strict binary expressions with non-pure operands.

Also add tests to demonstrate this added support.

Author: acoglio

books/kestrel/c/transformation/proof-generation.lisp

@@ -1414,11 +1414,9 @@
      both argument expressions are pure,
      since the order of evaluation is unspecified in C.")
    (xdoc::p
-    "For pure non-strict binary operators,
-     for now we also require both argument expressions to be pure
-     in order to generate a theorem.
-     But this could be relaxed, since in this case
-     the order of evaluation is prescribed.")
+    "For non-strict binary operators (which are pure),
+     the argument expressions may be pure or not,
+     because the order of evaluation is always determined.")
    (xdoc::p
     "For the non-pure strict simple assignment operator,
      for theorem generation we require the left expression to be a variable.
@@ -1497,10 +1495,7 @@
                        :thm-name thm-name
                        :vartys gin.vartys))))
      ((member-eq (binop-kind op) '(:logand :logor))
-      (b* (((unless (and (expr-purep arg1)
-                         (expr-purep arg2)))
-            (mv expr-new gout-no-thm))
-           ((mv & old-arg1) (ldm-expr arg1)) ; ERP must be NIL
+      (b* (((mv & old-arg1) (ldm-expr arg1)) ; ERP must be NIL
            ((mv & old-arg2) (ldm-expr arg2)) ; ERP must be NIL
            ((mv & new-arg1) (ldm-expr arg1-new)) ; ERP must be NIL
            ((mv & new-arg2) (ldm-expr arg2-new)) ; ERP must be NIL

books/kestrel/c/transformation/tests/simpadd0/logand.lisp

@@ -36,6 +36,9 @@
  :content "int logand(short x, long y) {
   return x && y;
 }
+int logand_nonpure(int x, int y, int z) {
+  return (x = z) && (y = ~z);
+}
 ")
 
 (assert-highest-thm-has-exec-fun *new-code*)

books/kestrel/c/transformation/tests/simpadd0/logor.lisp

@@ -36,6 +36,9 @@
  :content "int logor(short x, long y) {
   return x || y;
 }
+int logor_nonpure(int x, int y, int z) {
+  return (x = !z) || (y = z);
+}
 ")
 
 (assert-highest-thm-has-exec-fun *new-code*)

books/kestrel/c/transformation/tests/simpadd0/old/logand.c

@@ -1,3 +1,7 @@
 int logand(short x, long y) {
   return x && y;
 }
+
+int logand_nonpure(int x, int y, int z) {
+  return (x = z) && (y = ~z);
+}

books/kestrel/c/transformation/tests/simpadd0/old/logor.c

@@ -1,3 +1,7 @@
 int logor(short x, long y) {
   return x || y;
 }
+
+int logor_nonpure(int x, int y, int z) {
+  return (x = !z + 0) || (y = z);
+}