cSimplifier: some refactoring; make simplification optional

utwente-fmt · Oct 7, 2024 · 79e3e6d · 79e3e6d
1 parent 60db9ab
commit 79e3e6d
Show file tree

Hide file tree

Showing 3 changed files with 286 additions and 92 deletions.
diff --git a/src/col/vct/col/ast/unsorted/CNoParamImpl.scala b/src/col/vct/col/ast/unsorted/CNoParamImpl.scala
diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
@@ -169,7 +169,9 @@ object Transformation extends LazyLogging {
 
   def cSimplifierOfOptions(options: Options): Transformation =
     CSimplifier(onPassEvent =
-      writeOutFunctions(before, options.outputBeforePass) ++
+      options.outputIntermediatePrograms
+        .map(p => reportIntermediateProgram(p, "intermediate")).toSeq ++
+        writeOutFunctions(before, options.outputBeforePass) ++
         writeOutFunctions(after, options.outputAfterPass)
     )
 
@@ -463,4 +465,12 @@ case class VeyMontImplementationGeneration(
     )
 
 case class CSimplifier(override val onPassEvent: Seq[PassEventHandler] = Nil)
-    extends Transformation(onPassEvent, Seq(MakeRuntimeChecks))
+    extends Transformation(
+      onPassEvent,
+      Seq(
+        CIntBoolCoercion,
+        QuantifySubscriptAny, // no arr[*]
+        PropagateContextEverywhere, // inline context_everywhere into loop invariants
+        MakeRuntimeChecks,
+      ),
+    )