From 60db9ab1a93e2dd5b18a2f02af2b4bb75b04eaab Mon Sep 17 00:00:00 2001 From: ArmborstL Date: Sun, 6 Oct 2024 15:36:04 +0200 Subject: [PATCH] improve printed output for C files to look more like actual C --- .../expr/heap/alloc/NewPointerArrayImpl.scala | 8 ++++- .../literal/constant/BooleanValueImpl.scala | 28 ++++++++++----- .../ast/expr/literal/constant/NullImpl.scala | 7 +++- .../vct/col/ast/unsorted/CNoParamImpl.scala | 9 +++++ .../col/ast/unsorted/SimplifiedLoopImpl.scala | 10 ++++++ .../SimplifiedProcedureInvocationImpl.scala | 26 ++++++++++++++ src/col/vct/col/print/Namer.scala | 34 +++++++++++++------ src/main/vct/main/stages/Output.scala | 12 ++++--- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 17 +++++++--- 9 files changed, 121 insertions(+), 30 deletions(-) create mode 100644 src/col/vct/col/ast/unsorted/CNoParamImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/SimplifiedLoopImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/SimplifiedProcedureInvocationImpl.scala diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala index 18bd2bfbf8..c4cc3b8a77 100644 --- 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 index 2202095016..11123c99ca 100644 --- 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 index c331dea598..7656dc9f86 100644 --- 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 new file mode 100644 index 0000000000..ac3bbb1944 --- /dev/null +++ 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 new file mode 100644 index 0000000000..bf47ed58c7 --- /dev/null +++ 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 new file mode 100644 index 0000000000..2ad821238a --- /dev/null +++ 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 index 5f6da6a18f..5579114c0c 100644 --- 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 index e8dd1cc29e..48f2d58f5c 100644 --- 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 index 37e2e63b53..3c5084057d 100644 --- 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,