improve printed output for C files to look more like actual C

utwente-fmt · Oct 6, 2024 · 60db9ab · 60db9ab
1 parent 41c5c03
commit 60db9ab
Show file tree

Hide file tree

Showing 9 changed files with 121 additions and 30 deletions.
diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala
@@ -10,5 +10,11 @@ trait NewPointerArrayImpl[G] extends NewPointerArrayOps[G] {
 
   override def precedence: Int = Precedence.POSTFIX
   override def layout(implicit ctx: Ctx): Doc =
-    Text("new") <+> element <> "[" <> size <> "]"
+    ctx.syntax match {
+      case Ctx.C =>
+        val (spec, decl) = t.layoutSplitDeclarator
+        Text("(") <+> spec <+> decl <+> Text(") malloc(") <+> size <+>
+          Text(" * sizeof(") <+> element <+> Text("))")
+      case _ => Text("new") <+> element <> "[" <> size <> "]"
+    }
 }
diff --git a/src/col/vct/col/ast/expr/literal/constant/BooleanValueImpl.scala b/src/col/vct/col/ast/expr/literal/constant/BooleanValueImpl.scala
@@ -27,12 +27,24 @@ trait BooleanValueImpl[G] extends BooleanValueOps[G] {
       SharedLayoutElement('e'),
     )
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc =
-    Text(
-      orderedLayoutFixture.collect {
-        case e @ SharedLayoutElement(_) => e;
-        case e @ DedicatedLayoutElement(r, _) if r.toString == value.toString =>
-          e
-      }.map(_.textualData).mkString("")
-    )
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.C =>
+        Text(
+          if (value)
+            "1"
+          else
+            "0"
+        )
+      case _ =>
+        Text(
+          orderedLayoutFixture.collect {
+            case e @ SharedLayoutElement(_) => e;
+            case e @ DedicatedLayoutElement(r, _)
+                if r.toString == value.toString =>
+              e
+          }.map(_.textualData).mkString("")
+        )
+    }
+  }
 }
diff --git a/src/col/vct/col/ast/expr/literal/constant/NullImpl.scala b/src/col/vct/col/ast/expr/literal/constant/NullImpl.scala
@@ -9,5 +9,10 @@ trait NullImpl[G] extends NullOps[G] {
   override def t: Type[G] = TNull()
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc = Text("null")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.C => Text("NULL")
+      case _ => Text("null")
+    }
+  }
 }
diff --git a/src/col/vct/col/ast/unsorted/CNoParamImpl.scala b/src/col/vct/col/ast/unsorted/CNoParamImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.unsorted
+
+//import vct.col.ast.CNoParam
+//import vct.col.ast.ops.{CNoParamOps, CNoParamFamilyOps}
+//import vct.col.print._
+//
+//trait CNoParamImpl[G] extends CNoParamOps[G] with CNoParamFamilyOps[G] { this: CNoParam[G] =>
+//  // override def layout(implicit ctx: Ctx): Doc = ???
+//}
diff --git a/src/col/vct/col/ast/unsorted/SimplifiedLoopImpl.scala b/src/col/vct/col/ast/unsorted/SimplifiedLoopImpl.scala
@@ -0,0 +1,10 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.SimplifiedLoop
+import vct.col.ast.ops.SimplifiedLoopOps
+import vct.col.print._
+
+trait SimplifiedLoopImpl[G] extends SimplifiedLoopOps[G] {
+  this: SimplifiedLoop[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}
diff --git a/src/col/vct/col/ast/unsorted/SimplifiedProcedureInvocationImpl.scala b/src/col/vct/col/ast/unsorted/SimplifiedProcedureInvocationImpl.scala
@@ -0,0 +1,26 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.{SimplifiedProcedureInvocation, Type, Variable}
+import vct.col.ast.ops.SimplifiedProcedureInvocationOps
+import vct.col.print._
+
+trait SimplifiedProcedureInvocationImpl[G]
+    extends SimplifiedProcedureInvocationOps[G] {
+  this: SimplifiedProcedureInvocation[G] =>
+  override def precedence: Int = Precedence.POSTFIX
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(
+      Group(
+        Text(ctx.name(ref)) <>
+          (if (typeArgs.nonEmpty)
+             Text("<") <> Doc.args(typeArgs) <> ">"
+           else
+             Empty) <> "("
+      ) <> Doc.args(args ++ outArgs) <> ")" <>
+        DocUtil.givenYields(givenMap, yields)
+    )
+
+  override def typeEnv: Map[Variable[G], Type[G]] =
+    ref.decl.typeArgs.zip(typeArgs).toMap
+}
diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala
@@ -2,10 +2,17 @@ package vct.col.print
 
 import hre.util.ScopedStack
 import vct.col.ast._
+import vct.col.origin.{Origin, SourceName}
 
 import scala.collection.mutable
 
-case class Namer[G](syntax: Ctx.Syntax) {
+object Namer {
+  def getSrcName(o: Origin): Option[String] = {
+    o.find[SourceName].map(n => n.name)
+  }
+}
+
+case class Namer[G](syntax: Ctx.Syntax, useSourceNames: Boolean = false) {
   private val stack = ScopedStack[Node[G]]()
   private val names = mutable.Map[(scala.Any, String, Int), Declaration[G]]()
 
@@ -98,16 +105,21 @@ case class Namer[G](syntax: Ctx.Syntax) {
     }
 
     val name = decl.o.getPreferredNameOrElse()
-    var (baseName, index) = unpackName(decl match {
-      case declaration: GlobalDeclaration[_] =>
-        declaration match {
-          case _: Applicable[_] => name.camel
-          case _ => name.ucamel
-        }
-      case constant: EnumConstant[_] => name.usnake
-      case decl: LabelDecl[_] => name.usnake
-      case _ => name.camel
-    })
+    val srcName = Namer.getSrcName(decl.o)
+    var (baseName, index) =
+      if (useSourceNames && srcName.isDefined)
+        (srcName.get, 0)
+      else
+        unpackName(decl match {
+          case declaration: GlobalDeclaration[_] =>
+            declaration match {
+              case _: Applicable[_] => name.camel
+              case _ => name.ucamel
+            }
+          case constant: EnumConstant[_] => name.usnake
+          case decl: LabelDecl[_] => name.usnake
+          case _ => name.camel
+        })
 
     if (index == 0 && keywords.contains(baseName)) { index = 1 }
 

diff --git a/src/main/vct/main/stages/Output.scala b/src/main/vct/main/stages/Output.scala
@@ -20,7 +20,7 @@ import java.nio.file.{Files, Path}
 
 case object Output {
   def cSimplifierOfOptions(options: Options) = {
-    Output(options.cOutput, Ctx.C, false)
+    Output(options.cOutput, Ctx.C, false, useSourceNames = true)
   }
 
   def vesuvOfOptions[G <: Generation](
@@ -37,8 +37,12 @@ case object Output {
     Output(options.veymontOutput, Ctx.PVL, false)
 }
 
-case class Output(out: Option[Path], syntax: Ctx.Syntax, splitDecls: Boolean)
-    extends Stage[Verification[_ <: Generation], Seq[LiteralReadable]]
+case class Output(
+    out: Option[Path],
+    syntax: Ctx.Syntax,
+    splitDecls: Boolean,
+    useSourceNames: Boolean = false,
+) extends Stage[Verification[_ <: Generation], Seq[LiteralReadable]]
     with LazyLogging {
   override def friendlyName: String = "Saving Output"
 
@@ -56,7 +60,7 @@ case class Output(out: Option[Path], syntax: Ctx.Syntax, splitDecls: Boolean)
     }
 
   override def run(in: Verification[_ <: Generation]): Seq[LiteralReadable] = {
-    val namer = Namer[Generation](syntax)
+    val namer = Namer[Generation](syntax, useSourceNames)
     in.tasks
       .foreach(t => namer.name(t.program.asInstanceOf[Program[Generation]]))
     val names = namer.finish

diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
@@ -412,7 +412,13 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         // We can convert between rationals, integers and floats
         CastFloat[Post](rw.dispatch(c.expr), rw.dispatch(t))(c.o)
       case CCast(
-            inv @ CInvocation(CLocal("__vercors_malloc"), Seq(arg), Nil, Nil, _),
+            inv @ CInvocation(
+              CLocal("__vercors_malloc"),
+              Seq(arg),
+              Nil,
+              Nil,
+              _,
+            ),
             CTPointer(t2),
           ) =>
         val (t1, size) =
@@ -1067,12 +1073,13 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
                 contract = rw.dispatch(decl.decl.contract),
                 pure = pure,
                 inline = inline,
-              )(AbstractApplicable)(init.o)
+              )(AbstractApplicable)(init.o.sourceName(info.name))
             )
           )
         case None =>
           cGlobalNameSuccessor(RefCGlobalDeclaration(decl, idx)) = rw
-            .globalDeclarations.declare(new HeapVariable(t)(init.o))
+            .globalDeclarations
+            .declare(new HeapVariable(t)(init.o.sourceName(info.name)))
       }
     }
   }
@@ -1786,7 +1793,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           inv.blame,
         )
       case ref: RefCFunctionDefinition[Pre] =>
-        if(simplify) {
+        if (simplify) {
           SimplifiedProcedureInvocation[Post](
             cFunctionSuccessor.ref(ref.decl),
             newArgs,
@@ -1979,7 +1986,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         getCudaLocalSize(i, o) * getCudaGroupThread(i, o) +
           getCudaLocalThread(i, o)
       case _ =>
-        if(simplify) {
+        if (simplify) {
           SimplifiedProcedureInvocation[Post](
             cFunctionDeclSuccessor.ref((decls, initIdx)),
             rewrittenArgs,