Add Concrete Syntax for Unstructured Programs in Strata Core

.github/pull_request_template.md

@@ -0,0 +1,7 @@
+**Warning:** This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete.
+
+The code that will be moved includes:
+- Strata/DDM/*
+- Strata/Languages/Boole/*
+- Strata/Languages/Python/* along with Tools/Python/*
+- Tools/BoogieToStrata

Examples/CFGNondet.core.st

@@ -0,0 +1,23 @@
+program Core;
+
+// Nondeterministic CFG: y is set to either 1 or 2.
+procedure NondetChoice(out y : int)
+spec {
+  ensures (y == 1 || y == 2);
+}
+cfg entry {
+  entry: {
+    goto left, right;
+  }
+  left: {
+    y := 1;
+    goto done;
+  }
+  right: {
+    y := 2;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};

Examples/CFGSimple.core.st

@@ -0,0 +1,48 @@
+program Core;
+
+// A simple deterministic CFG: compute max of two integers.
+procedure Max(x : int, y : int, out m : int)
+spec {
+  ensures (m >= x);
+  ensures (m >= y);
+  ensures (m == x || m == y);
+}
+cfg entry {
+  entry: {
+    branch (x >= y) goto then_branch else else_branch;
+  }
+  then_branch: {
+    m := x;
+    goto done;
+  }
+  else_branch: {
+    m := y;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+
+// A CFG with a simple loop: increment y until it reaches n.
+procedure CountUp(n : int, out y : int)
+spec {
+  requires (n >= 0);
+  ensures (y == n);
+}
+cfg entry {
+  entry: {
+    y := 0;
+    goto loop;
+  }
+  loop: {
+    branch (y < n) goto body else done;
+  }
+  body: {
+    y := y + 1;
+    goto loop;
+  }
+  done: {
+    return;
+  }
+};

Examples/expected/IrrelevantAxioms.removeIrrelevantAxioms.core.st

@@ -1,11 +1,11 @@
 program Core;
 
 function f (x : int) : int;
-axiom [f_positive]: forall __q0 : int :: f(__q0) > 0;
-axiom [f_monotone]: forall __q0 : int :: forall __q1 : int :: __q0 < __q1 ==> f(__q0) < f(__q1);
+axiom [f_positive]: forall x : int :: f(x) > 0;
+axiom [f_monotone]: forall x : int :: forall y : int :: x < y ==> f(x) < f(y);
 function g (x : int) : int;
 function h (x : int) : int;
-axiom [h_def]: forall __q0 : int :: h(__q0) == f(__q0) + 1;
+axiom [h_def]: forall x : int :: h(x) == f(x) + 1;
 procedure TestF (x : int, out result : int)
 spec {
   ensures [result_positive]: result > 0;

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -346,7 +346,8 @@ def createImplementationSymbolFromAST (func : Core.Procedure) : Except String CB
 
   -- For now, keep the hardcoded implementation but use function name from AST
   let loc : SourceLoc := { functionName := (func.header.name.toPretty), lineNum := "1" }
-  let stmtJsons ← (func.body.mapM (stmtToJson (I:=CoreLParams) · loc))
+  let bodyStmts ← func.body.getStructured
+  let stmtJsons ← (bodyStmts.mapM (stmtToJson (I:=CoreLParams) · loc))
 
   let implValue := Json.mkObj [
     ("id", "code"),

Strata/Backends/CBMC/GOTO.lean

@@ -5,6 +5,7 @@
 -/
 module
 
+import Strata.Backends.CBMC.GOTO.CoreCFGToGOTOPipeline
 import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
 import Strata.Backends.CBMC.GOTO.DefaultSymbols