Htd/structured to unstructured pipeline

README.md

@@ -72,7 +72,7 @@ A JDK (11+) providing `javac` must be on your `PATH`. For running the
 Java/Ion integration test, download the ion-java jar:
 
 ```bash
-wget -q -O StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar \
+wget -q -O StrataTestExtra/DDM/Integration/Java/testdata/ion-java-1.11.11.jar \
   https://github.com/amazon-ion/ion-java/releases/download/v1.11.11/ion-java-1.11.11.jar
 ```
 

Strata.lean

@@ -31,9 +31,12 @@ import Strata.Languages.Laurel.LaurelCompilationPipeline
 
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect
+import Strata.Transform.CanFailPreservation
 import Strata.Transform.CoreSpecification
 import Strata.Transform.DetToKleeneCorrect
+import Strata.Transform.PipelineBridge
 import Strata.Transform.ProcBodyVerifyCorrect
+import Strata.Transform.StructuredToUnstructuredCorrect
 
 /- Strata Languages — additional -/
 import Strata.Languages.B3
@@ -59,6 +62,7 @@ import Strata.DL.SMT.FactoryCorrect
 import Strata.DL.SMT.Translate
 
 /- Code Transforms — additional -/
+import Strata.Transform.GenSuffix
 import Strata.Transform.StructuredToUnstructured
 
 /- Other -/

Strata/DL/Imperative/BasicBlock.lean

@@ -30,25 +30,30 @@ where `n` is the total number of blocks in the graph.
 where execution should proceed next, if anywhere. -/
 inductive DetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to `lt` if `p` is true, or `lf` is `p` is false. -/
-  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P := .empty)
+  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P)
   /-- Stop execution of the current unstructured program. If in a procedure
   body, this can be interpreted as returning to the caller. -/
-  | finish (md : MetaData P := .empty)
+  | finish (md : MetaData P)
+  /-- Escape the current unstructured program by an uncaught structured exit
+  to `lbl`. Unlike `finish` (a normal return), this records that control
+  left the program via an exit that no enclosing block caught, preserving
+  the escaping label so the outcome kind is observable on the target side. -/
+  | exitTo (lbl : Label) (md : MetaData P)
 
 /-- For the moment, we don't have an unconditional jump in the language, and
 model it instead using `condGoto`. By defining this function, we can easily
 create unconditional jumps, and future proof against the possibility of adding
 it as a constructor in the future.  -/
-def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P :=
-  condGoto HasBool.tt l l
+@[expose] def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P) : DetTransferCmd Label P :=
+  condGoto HasBool.tt l l md
 
 /-- A `NondetTransfer` command terminates a non-deterministic basic block,
 indicating the list of possible blocks where execution could proceed next, if
 anywhere. -/
 inductive NondetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to any one of a list of labels, non-deterministically. `goto`
   with no labels is equivalent to `finish` in `DetTransferCmd` -/
-  | goto (ls : List Label) (md : MetaData P := .empty)
+  | goto (ls : List Label) (md : MetaData P)
   deriving Inhabited
 
 def NondetTransferCmd.targets : NondetTransferCmd Label P → List Label
@@ -79,13 +84,35 @@ structure CFG (Label Block : Type) where
 
 --------
 
+/-- Strip metadata from a deterministic transfer command. -/
+def DetTransferCmd.stripMetaData : DetTransferCmd Label P → DetTransferCmd Label P
+  | .condGoto p lt lf _ => .condGoto p lt lf .empty
+  | .finish _ => .finish .empty
+  | .exitTo lbl _ => .exitTo lbl .empty
+
+/-- Strip metadata from a non-deterministic transfer command. -/
+def NondetTransferCmd.stripMetaData : NondetTransferCmd Label P → NondetTransferCmd Label P
+  | .goto ls _ => .goto ls .empty
+
+/-- Strip transfer metadata from a deterministic basic block. -/
+def DetBlock.stripMetaData (blk : DetBlock Label Cmd P) : DetBlock Label Cmd P :=
+  { blk with transfer := blk.transfer.stripMetaData }
+
+/-- Strip transfer metadata from all blocks in a deterministic CFG. -/
+def CFG.stripDetMetaData (cfg : CFG Label (DetBlock Label Cmd P)) :
+    CFG Label (DetBlock Label Cmd P) :=
+  { cfg with blocks := cfg.blocks.map fun (lbl, blk) => (lbl, blk.stripMetaData) }
+
+--------
+
 open Std (ToFormat Format format)
 
 def formatDetTransferCmd (P : PureExpr) (c : DetTransferCmd Label P)
   [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=
   match c with
   | .condGoto c lt lf md => f!"{md}condGoto {c} {lt} {lf}"
   | .finish md => f!"{md}finish"
+  | .exitTo lbl md => f!"{md}exitTo {lbl}"
 
 def formatNondetTransferCmd (P : PureExpr) (c : NondetTransferCmd Label P)
   [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=