Chore: Rust refactorings

Makefile

@@ -1,3 +1,6 @@
+# Run these tasks even if eponymous files or folders exist
+.PHONY: test-dafny exe
+
 DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
 
 default: exe
@@ -30,6 +33,24 @@ tests:
 test:
 	(cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}")
 
+# Run Dafny on an integration test case directly in the folder itself.
+# make test-run name=<part of the path> action="run ..."
+test-dafny:
+	name="$(name)"; \
+	files=$$(cd "${DIR}"/Source/IntegrationTests/TestFiles/LitTests/LitTest; find . -type f -wholename "*$$name*" | grep -E '\.dfy$$'); \
+	count=$$(echo "$$files" | wc -l); \
+  echo "$${files}"; \
+	if [ "$$count" -eq 0 ]; then \
+		echo "No files found matching pattern: $$name"; \
+		exit 1; \
+	else \
+		echo "$$count test files found."; \
+		for file in $$files; do \
+			filedir=$$(dirname "$$file"); \
+			(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; "${DIR}"/Binaries/Dafny $(action)  "$$(basename $$file)" ); \
+		done; \
+	fi
+
 tests-verbose:
 	(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
 

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -2200,7 +2200,11 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             match op {
               case Eq(referential) => {
                 if (referential) {
-                  r := R.BinaryOp("==", left, right, DAST.Format.BinaryOpFormat.NoFormat());
+                  if pointerType.Raw? {
+                    r := Error("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)");
+                  } else {
+                    r := R.BinaryOp("==", left, right, DAST.Format.BinaryOpFormat.NoFormat());
+                  }
                 } else {
                   if rExpr.SeqValue? && |rExpr.elements| == 0 {
                     r := R.BinaryOp("==", left.Sel("to_array").Apply0().Sel("len").Apply0(), R.LiteralInt("0"), DAST.Format.BinaryOpFormat.NoFormat());

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -3213,7 +3213,13 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._
                 bool _14_referential = _source1.dtor_referential;
                 {
                   if (_14_referential) {
-                    r = RAST.Expr.create_BinaryOp(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("=="), _8_left, _11_right, DAST.Format.BinaryOpFormat.create_NoFormat());
+                    if (((this).pointerType).is_Raw) {
+                      RAST._IExpr _out6;
+                      _out6 = (this).Error(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)"), (this).InitEmptyExpr());
+                      r = _out6;
+                    } else {
+                      r = RAST.Expr.create_BinaryOp(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("=="), _8_left, _11_right, DAST.Format.BinaryOpFormat.create_NoFormat());
+                    }
                   } else {
                     if (((_2_rExpr).is_SeqValue) && ((new BigInteger(((_2_rExpr).dtor_elements).Count)).Sign == 0)) {
                       r = RAST.Expr.create_BinaryOp(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("=="), ((((_8_left).Sel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("to_array"))).Apply0()).Sel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("len"))).Apply0(), RAST.Expr.create_LiteralInt(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("0")), DAST.Format.BinaryOpFormat.create_NoFormat());
@@ -3254,11 +3260,11 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._
         }
       }
     after_match0: ;
-      RAST._IExpr _out6;
-      Defs._IOwnership _out7;
-      (this).FromOwned(r, expectedOwnership, out _out6, out _out7);
-      r = _out6;
-      resultingOwnership = _out7;
+      RAST._IExpr _out7;
+      Defs._IOwnership _out8;
+      (this).FromOwned(r, expectedOwnership, out _out7, out _out8);
+      r = _out7;
+      resultingOwnership = _out8;
       readIdents = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Union(_10_recIdentsL, _13_recIdentsR);
       return ;
     }