Replace Identifier with String x Metadata (#163)

*Issue #, if available:*

*Description of changes:*

Redefines an `Identifier` as `String x IDMeta` and parameterizes
`LExpr`, `LExprT`, etc with `IDMeta` rather than `Identifier`. This
allows several important operations on identifiers and expressions
including:
- Generating arbitrary distinct identifiers (assuming `IDMeta` is
`Inhabited`)
- Pattern matching on the name of a `.op` expression

Note: since the `ToFormat` instance of `BoogieIdent` (the only
non-`String` identifier in use) simply gave the name, this
implementation ignores `IDMeta` when converting `Identifiers` to
`String` or `Format`.


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

Co-authored-by: Josh Cohen <[email protected]>

Author: joscoh

Strata/Backends/CBMC/BoogieToCBMC.lean

@@ -54,10 +54,10 @@ instance : IdentToStr String where
 class HasLExpr (P : Imperative.PureExpr) (I : Type) where
   expr_eq : P.Expr = Lambda.LExpr Lambda.LMonoTy I
 
-instance : HasLExpr Boogie.Expression BoogieIdent where
+instance : HasLExpr Boogie.Expression Visibility where
   expr_eq := rfl
 
-def exprToJson (I : Type) [IdentToStr I] (e : Lambda.LExpr Lambda.LMonoTy I) (loc: SourceLoc) : Json :=
+def exprToJson (I : Type) [IdentToStr (Lambda.Identifier I)] (e : Lambda.LExpr Lambda.LMonoTy I) (loc: SourceLoc) : Json :=
   match e with
   | .app (.app (.op op _) left) right =>
     let leftJson := match left with
@@ -102,7 +102,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
       mkCodeBlock "expression" "6" loc.functionName #[
         mkSideEffect "assign" "6" loc.functionName mkIntType #[
           mkLvalueSymbol s!"{loc.functionName}::1::{name.toPretty}" "6" loc.functionName,
-          exprToJson (I:=BoogieIdent) expr exprLoc
+          exprToJson (I:=Visibility) expr exprLoc
         ]
       ]
     | .assert label expr _ =>
@@ -127,7 +127,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
           Json.mkObj [
             ("id", "arguments"),
             ("sub", Json.arr #[
-              exprToJson (I:=BoogieIdent) expr exprLoc,
+              exprToJson (I:=Visibility) expr exprLoc,
               mkStringConstant label "7" loc.functionName
             ])
           ]
@@ -155,15 +155,15 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json :=
           Json.mkObj [
             ("id", "arguments"),
             ("sub", Json.arr #[
-              exprToJson (I:=BoogieIdent) expr exprLoc
+              exprToJson (I:=Visibility) expr exprLoc
             ])
           ]
         ]
       ]
     | .havoc _ _ => panic! "Unimplemented"
 
 mutual
-partial def blockToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr I] [HasLExpr P I]
+partial def blockToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr (Lambda.Identifier I)] [HasLExpr P I]
   (b: Imperative.Block P Command) (loc: SourceLoc) : Json :=
   Json.mkObj [
     ("id", "code"),
@@ -176,7 +176,7 @@ partial def blockToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr I] [Has
     ("sub", Json.arr (b.ss.map (stmtToJson (I:=I) · loc)).toArray)
   ]
 
-partial def stmtToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr I] [HasLExpr P I]
+partial def stmtToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr (Lambda.Identifier I)] [HasLExpr P I]
   (e : Imperative.Stmt P Command) (loc: SourceLoc) : Json :=
   match e with
   | .cmd cmd => cmdToJson cmd loc
@@ -245,7 +245,7 @@ def createContractSymbolFromAST (func : Boogie.Procedure) : CBMCSymbol :=
     ]),
     ("sub", Json.arr #[
       parameterTuple,
-      exprToJson (I:=BoogieIdent) (listToExpr func.spec.preconditions) {functionName := func.header.name.toPretty, lineNum := "2"}
+      exprToJson (I:=Visibility) (listToExpr func.spec.preconditions) {functionName := func.header.name.toPretty, lineNum := "2"}
     ])
   ]
 
@@ -257,7 +257,7 @@ def createContractSymbolFromAST (func : Boogie.Procedure) : CBMCSymbol :=
     ]),
     ("sub", Json.arr #[
       parameterTuple,
-      exprToJson (I:=BoogieIdent) (listToExpr func.spec.postconditions) {functionName := func.header.name.toPretty, lineNum := "2"}
+      exprToJson (I:=Visibility) (listToExpr func.spec.postconditions) {functionName := func.header.name.toPretty, lineNum := "2"}
     ])
   ]
 
@@ -304,7 +304,7 @@ def createContractSymbolFromAST (func : Boogie.Procedure) : CBMCSymbol :=
 def getParamJson(func: Boogie.Procedure) : Json :=
   Json.mkObj [
     ("id", ""),
-    ("sub", Json.arr (func.header.inputs.map (λ i => mkParameter i.fst.snd (func.header.name.toPretty) "1")).toArray)
+    ("sub", Json.arr (func.header.inputs.map (λ i => mkParameter i.fst.name (func.header.name.toPretty) "1")).toArray)
   ]
 
 
@@ -331,7 +331,7 @@ def createImplementationSymbolFromAST (func : Boogie.Procedure) : CBMCSymbol :=
 
   -- 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.map (stmtToJson (I:=BoogieIdent) · loc))
+  let stmtJsons := (func.body.map (stmtToJson (I:=Visibility) · loc))
 
   let implValue := Json.mkObj [
     ("id", "code"),
@@ -352,7 +352,7 @@ def createImplementationSymbolFromAST (func : Boogie.Procedure) : CBMCSymbol :=
     module := "ex_prog",
     name := (func.header.name.toPretty),
     prettyName := (func.header.name.toPretty),
-    prettyType := s!"signed int (signed int {String.intercalate ", signed int " (func.header.inputs.keys.map (λ p => p.snd))})",
+    prettyType := s!"signed int (signed int {String.intercalate ", signed int " (func.header.inputs.keys.map (λ p => p.name))})",
     prettyValue := "{\n  signed int z;\n  z = x;\n  z = z + 1;\n  return z;\n}",
     type := implType,
     value := implValue
@@ -364,23 +364,23 @@ def testSymbols (proc: Boogie.Procedure) : String := Id.run do
   let implSymbol := createImplementationSymbolFromAST proc
 
   -- Get parameter names from AST
-  let paramNames : List String := proc.header.inputs.keys.map (λ p => p.snd)
+  let paramNames : List String := proc.header.inputs.keys.map (λ p => p.name)
 
   -- Hardcode local variable for now
   let zSymbol := createLocalSymbol "z" proc.header.name.toPretty
 
   -- Build symbol map
   let mut m : Map String CBMCSymbol := Map.empty
-  m := m.insert s!"contract::{proc.header.name.snd}" contractSymbol
-  m := m.insert proc.header.name.snd implSymbol
+  m := m.insert s!"contract::{proc.header.name.name}" contractSymbol
+  m := m.insert proc.header.name.name implSymbol
 
   -- Add parameter symbols
   for paramName in paramNames do
     let paramSymbol := createParameterSymbol paramName proc.header.name.toPretty
-    m := m.insert s!"{proc.header.name.snd}::{paramName}" paramSymbol
+    m := m.insert s!"{proc.header.name.name}::{paramName}" paramSymbol
 
   -- Add local variable
-  m := m.insert s!"{proc.header.name.snd}::1::z" zSymbol
+  m := m.insert s!"{proc.header.name.name}::1::z" zSymbol
   toString (toJson m)
 
 end Boogie

Strata/Backends/CBMC/StrataToCBMC.lean

@@ -51,11 +51,11 @@ def lexprToCBMC (expr : Strata.C_Simp.Expression.Expr) (functionName : String) :
   let cfg := CBMCConfig.empty
   match expr with
   | .app (.app (.op op _) (.fvar varName _)) (.const value _) =>
-    mkBinaryOp (opToStr op) "2" functionName (config := cfg)
+    mkBinaryOp (opToStr op.name) "2" functionName (config := cfg)
       (Json.mkObj [
         ("id", "symbol"),
         ("namedSub", Json.mkObj [
-          ("#base_name", Json.mkObj [("id", varName)]),
+          ("#base_name", Json.mkObj [("id", varName.name)]),
           ("#id_class", Json.mkObj [("id", "1")]),
           ("#lvalue", Json.mkObj [("id", "1")]),
           ("#source_location", mkSourceLocation "from_andrew.c" functionName "2" cfg),
@@ -96,8 +96,8 @@ def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=
     ])
   }
 
-  let sourceLocation := mkSourceLocation "from_andrew.c" func.name "2"
-  let ensuresSourceLocation := mkSourceLocation "from_andrew.c" func.name "3"
+  let sourceLocation := mkSourceLocation "from_andrew.c" func.name.name "2"
+  let ensuresSourceLocation := mkSourceLocation "from_andrew.c" func.name.name "3"
 
   let mathFunctionType := Json.mkObj [
     ("id", "mathematical_function"),
@@ -128,7 +128,7 @@ def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=
     ]),
     ("sub", Json.arr #[
       parameterTuple,
-      lexprToCBMC func.pre func.name
+      lexprToCBMC func.pre func.name.name
     ])
   ]
 
@@ -140,15 +140,15 @@ def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=
     ]),
     ("sub", Json.arr #[
       parameterTuple,
-      lexprToCBMC func.post func.name
+      lexprToCBMC func.post func.name.name
     ])
   ]
 
   let parameters := Json.mkObj [
     ("id", ""),
     ("sub", Json.arr #[
-      mkParameter "x" func.name "1" cfg,
-      mkParameter "y" func.name "1" cfg
+      mkParameter "x" func.name.name "1" cfg,
+      mkParameter "y" func.name.name "1" cfg
     ])
   ]
 
@@ -172,13 +172,13 @@ def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=
   ]
 
   {
-    baseName := func.name,
+    baseName := func.name.name,
     isProperty := true,
     location := location,
     mode := "C",
     module := "from_andrew",
     name := s!"contract::{func.name}",
-    prettyName := func.name,
+    prettyName := func.name.name,
     prettyType := "signed int (signed int x, signed int y)",
     type := contractType,
     value := Json.mkObj [("id", "nil")]
@@ -188,7 +188,7 @@ def getParamJson(func: Strata.C_Simp.Function) : Json :=
   let cfg := CBMCConfig.empty
   Json.mkObj [
     ("id", ""),
-    ("sub", Json.arr (func.inputs.map (λ i => mkParameter i.fst func.name "1" cfg)).toArray)
+    ("sub", Json.arr (func.inputs.map (λ i => mkParameter i.fst.name func.name.name "1" cfg)).toArray)
   ]
 
 def exprToJson (e : Strata.C_Simp.Expression.Expr) (loc: SourceLoc) : Json :=
@@ -203,7 +203,7 @@ def exprToJson (e : Strata.C_Simp.Expression.Expr) (loc: SourceLoc) : Json :=
       | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{varName}" loc.lineNum loc.functionName cfg
       | .const value _ => mkConstant value "10" (mkSourceLocation "from_andrew.c" loc.functionName loc.lineNum cfg) cfg
       | _ => exprToJson right loc
-    mkBinaryOp (opToStr op) loc.lineNum loc.functionName leftJson rightJson cfg
+    mkBinaryOp (opToStr op.name) loc.lineNum loc.functionName leftJson rightJson cfg
   | .const n _ =>
     mkConstant n "10" (mkSourceLocation "from_andrew.c" loc.functionName "14" cfg) cfg
   | _ => panic! "Unimplemented"
@@ -344,29 +344,29 @@ def createImplementationSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymb
   ]
 
   -- For now, keep the hardcoded implementation but use function name from AST
-  let loc : SourceLoc := { functionName := func.name, lineNum := "1" }
+  let loc : SourceLoc := { functionName := func.name.name, lineNum := "1" }
   let stmtJsons := (func.body.map (stmtToJson · loc)) --++ [returnStmt]
 
   let implValue := Json.mkObj [
     ("id", "code"),
     ("namedSub", Json.mkObj [
-      ("#end_location", mkSourceLocation "from_andrew.c" func.name "15"),
-      ("#source_location", mkSourceLocation "from_andrew.c" func.name "4"),
+      ("#end_location", mkSourceLocation "from_andrew.c" func.name.name "15"),
+      ("#source_location", mkSourceLocation "from_andrew.c" func.name.name "4"),
       ("statement", Json.mkObj [("id", "block")]),
       ("type", emptyType)
     ]),
     ("sub", Json.arr stmtJsons.toArray)
   ]
 
   {
-    baseName := func.name,
+    baseName := func.name.name,
     isLvalue := true,
     location := location,
     mode := "C",
     module := "from_andrew",
-    name := func.name,
-    prettyName := func.name,
-    prettyType := s!"signed int (signed int {String.intercalate ", signed int " func.inputs.keys})",
+    name := func.name.name,
+    prettyName := func.name.name,
+    prettyType := s!"signed int (signed int {String.intercalate ", signed int " (func.inputs.keys.map Lambda.Identifier.name)})",
     prettyValue := "{\n  signed int z;\n  z = x + y;\n  __CPROVER_assert(z > x, \"test_assert\");\n  if(z > 10)\n  {\n    z = z - 1;\n  }\n\n  else\n  {\n    z = z + 1;\n  }\n  __CPROVER_assume(z > 0);\n  return 0;\n}",
     type := implType,
     value := implValue
@@ -381,16 +381,16 @@ def testSymbols (myFunc: Strata.C_Simp.Function) : String := Id.run do
   let paramNames := myFunc.inputs.keys
 
   -- Hardcode local variable for now
-  let zSymbol := createLocalSymbol "z" myFunc.name
+  let zSymbol := createLocalSymbol "z" myFunc.name.name
 
   -- Build symbol map
   let mut m : Map String CBMCSymbol := Map.empty
   m := m.insert s!"contract::{myFunc.name}" contractSymbol
-  m := m.insert myFunc.name implSymbol
+  m := m.insert myFunc.name.name implSymbol
 
   -- Add parameter symbols
   for paramName in paramNames do
-    let paramSymbol := createParameterSymbol paramName myFunc.name
+    let paramSymbol := createParameterSymbol paramName.name myFunc.name.name
     m := m.insert s!"{myFunc.name}::{paramName}" paramSymbol
 
   -- Add local variable