From 1e602ade41ca76b8294cc6be77125425981896a8 Mon Sep 17 00:00:00 2001 From: pataei Date: Fri, 10 Mar 2023 08:55:17 -0500 Subject: [PATCH 01/25] starting on surface syntax --- lib/checker.ml | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/lib/checker.ml b/lib/checker.ml index 7b88bc136..13577e192 100644 --- a/lib/checker.ml +++ b/lib/checker.ml @@ -871,20 +871,12 @@ and compile_time_known_expr (env: Checker_env.t) (expr: P4light.coq_Expression) | _ -> false (* - judgment rule is as follows. it type check exp under environment e and context c. - it also infers type as well as doing a pass from types to prog. + judgment rule of expression typing is: - e, c |- exp ~~> prog_exp + env, ctx |- exp ~~> ss_exp, type, dir - Note: prog_exp is a record with three fields: expr, typ, dir. - For simplicity, I omitted the name of the fields but the order is kept. - Also, for simplicity, I omitted tags. - Data constructors start with a capital letter. - Where possible data constructors are omitted and instead the name of the - expression implies the data constructor, e.g., str indicates an expression - that is a string. - - e, c |- True {tags} ~~> {True {tags}; Bool; Directionless; tags} + It does type checking and type inference. generates an expression in surface syntax + written in Coq. *) From eeeff1ea9b2184cd0ad461473c2f3ea4a89ebf94 Mon Sep 17 00:00:00 2001 From: pataei Date: Thu, 23 Mar 2023 12:47:45 -0400 Subject: [PATCH 02/25] working on synthesized types syntax --- coq/lib/Surface/Syntax/Syntax.v | 100 ++++++++++++++++++++++++++++++++ 1 file changed, 100 insertions(+) create mode 100644 coq/lib/Surface/Syntax/Syntax.v diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v new file mode 100644 index 000000000..b59fde7f8 --- /dev/null +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -0,0 +1,100 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. + +From Coq Require Import Numbers.BinNums Classes.EquivDec. + +From Poulet4.P4light.Syntax Require P4String P4Int. + + +Section Syntax. + + Context {tags_t: Type}. + Notation P4String := (P4String.t tags_t). + Notation P4Int := (P4Int.t tags_t). + + Variant parameter := + | Parameter (direction: direction) + (typ: surfaceTyp) + (default_value: option expression) + (variable: P4String). + + Variant direction := + | In + | Out + | InOut + | Directionless. + + Variant functionKind := + | FunParser + | FunControl + | FunExtern + | FunTable + | FunAction + | FunFunction + | FunBuiltin. + + Inductive surfaceTyp := + | TypBool + | TypError + | TypMatchKind + | TypInteger + | TypString + | TypInt (width: N) + | TypBit (width: N) + | TypVarBit (width: N) + | TypIdentifier (name: P4String) + | TypSpecialization (base: surfaceTyp) + (args: list surfaceType) + | TypHeaderStack (typ: surfaceTyp) + (size: N) + | TypTuple (types: list surfaceTyp). + + Variant surfaceTypOrVoid := + | TypSurface (typ: surfaceTyp) + | TypVoid. + + Inductive declaredTyp := + | TypHeader (type_params: list P4String) + (fields: P4String.AList tags_t surfaceTyp) + | TypHeaderUnion (type_params: list P4String) + (fields: P4String.AList tags_t surfaceTyp) + | TypStruct (type_params: list P4String) + (fields: P4String.AList tags_t surfaceTyp) + | TypEnum (name: P4String) + (typ: option surfaceTyp) + (members: list P4String) + | TypParser (type_params: list P4String) + (parameters: list parameter) + | TypControl (type_params: list P4String) + (parameters: list parameter) + | TypPackage (type_params: list P4String) + (wildcard_params: listP4String) + (parameters: list parameter). + + Inductive synthesizedTyp := + | TypFunction (type_params: list P4String) + (parameters: list parameter) + (kind: functionKind) + (ret: surfaceTypOrVoid) + | TypSet + | TypExtern + | TypRecord + | TypNewTyp + | TypAction + | TypConstructor + | TypTable. + + Inductive typ := + | TypSurface (typ: surfaceTyp) + | TypDeclared (typ: declaredTyp) + | TypSynthesized (typ: synthesizedTyp) + | TypVoid. + + Inductive Expression := + | ExpBool (b: Bool) + | ExpString (s: P4String) + | ExpInt (i: P4Int) + | ExpSignedInt (). + +End Syntax. + From c4e3ac4ea0e7a443c53cf54500ec5e152bda96a3 Mon Sep 17 00:00:00 2001 From: pataei Date: Thu, 23 Mar 2023 14:02:01 -0400 Subject: [PATCH 03/25] types syntax --- coq/lib/Surface/Syntax/Syntax.v | 50 ++++++++++++++++++++------------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index b59fde7f8..7ef17c3cf 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -49,46 +49,56 @@ Section Syntax. (size: N) | TypTuple (types: list surfaceTyp). - Variant surfaceTypOrVoid := + Variant variableTyp := + | TypVariable (variable: P4String). + + Variant functionTyp := | TypSurface (typ: surfaceTyp) - | TypVoid. + | TypVoid + | TypVar (variable: variableTyp). Inductive declaredTyp := - | TypHeader (type_params: list P4String) + | TypHeader (type_params: list variableTyp) (fields: P4String.AList tags_t surfaceTyp) - | TypHeaderUnion (type_params: list P4String) + | TypHeaderUnion (type_params: list variableTyp) (fields: P4String.AList tags_t surfaceTyp) - | TypStruct (type_params: list P4String) + | TypStruct (type_params: list variableTyp) (fields: P4String.AList tags_t surfaceTyp) | TypEnum (name: P4String) (typ: option surfaceTyp) (members: list P4String) - | TypParser (type_params: list P4String) + | TypParser (type_params: list variableTyp) (parameters: list parameter) - | TypControl (type_params: list P4String) + | TypControl (type_params: list variableTyp) (parameters: list parameter) - | TypPackage (type_params: list P4String) - (wildcard_params: listP4String) + | TypPackage (type_params: list variableTyp) + (wildcard_params: list P4String) (parameters: list parameter). Inductive synthesizedTyp := - | TypFunction (type_params: list P4String) + | TypFunction (type_params: list variableTyp) (parameters: list parameter) (kind: functionKind) - (ret: surfaceTypOrVoid) - | TypSet - | TypExtern - | TypRecord - | TypNewTyp - | TypAction - | TypConstructor - | TypTable. + (ret: functionTyp) + | TypSet (typ: surfaceTyp) + | TypExtern (extern_name: P4String) + | TypRecord (type_params: list variableTyp) + (fields: P4String.AList tags_t surfaceTyp) + | TypNewTyp (name: P4String) + (typ: surfaceTyp) + | TypAction (data_params: list parameter) + (ctrl_params: list parameter) + | TypConstructor (type_params: list variableTyp) + (wildcard_params: list P4String) + (params: list parameter) + (ret: functionTyp) + | TypTable (result_typ_name: P4String). Inductive typ := | TypSurface (typ: surfaceTyp) | TypDeclared (typ: declaredTyp) - | TypSynthesized (typ: synthesizedTyp) - | TypVoid. + | TypSynthesized (typ: synthesizedTyp). + (* | TypVoid. *) Inductive Expression := | ExpBool (b: Bool) From cfa36aed03fbe6a0c512785dc31accfa1627e788 Mon Sep 17 00:00:00 2001 From: pataei Date: Thu, 23 Mar 2023 14:02:48 -0400 Subject: [PATCH 04/25] remove unfinished code --- coq/lib/Surface/Syntax/Syntax.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 7ef17c3cf..41585eaa8 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -100,11 +100,11 @@ Section Syntax. | TypSynthesized (typ: synthesizedTyp). (* | TypVoid. *) - Inductive Expression := - | ExpBool (b: Bool) - | ExpString (s: P4String) - | ExpInt (i: P4Int) - | ExpSignedInt (). + (* Inductive expression := *) + (* | ExpBool (b: Bool) *) + (* | ExpString (s: P4String) *) + (* | ExpInt (i: P4Int) *) + (* | ExpSignedInt (). *) End Syntax. From 5a45c6bcdef32961e2737087c1f63c6ea400ea14 Mon Sep 17 00:00:00 2001 From: pataei Date: Fri, 24 Mar 2023 11:54:11 -0400 Subject: [PATCH 05/25] fix some errors --- coq/lib/Surface/Syntax/Syntax.v | 38 ++++++++++++++++----------------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 41585eaa8..d04b6a081 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -12,18 +12,15 @@ Section Syntax. Notation P4String := (P4String.t tags_t). Notation P4Int := (P4Int.t tags_t). - Variant parameter := - | Parameter (direction: direction) - (typ: surfaceTyp) - (default_value: option expression) - (variable: P4String). - Variant direction := | In | Out | InOut | Directionless. + Variant variableTyp := + | TypVariable (variable: P4String). + Variant functionKind := | FunParser | FunControl @@ -44,14 +41,11 @@ Section Syntax. | TypVarBit (width: N) | TypIdentifier (name: P4String) | TypSpecialization (base: surfaceTyp) - (args: list surfaceType) + (args: list surfaceTyp) | TypHeaderStack (typ: surfaceTyp) (size: N) | TypTuple (types: list surfaceTyp). - Variant variableTyp := - | TypVariable (variable: P4String). - Variant functionTyp := | TypSurface (typ: surfaceTyp) | TypVoid @@ -73,7 +67,17 @@ Section Syntax. (parameters: list parameter) | TypPackage (type_params: list variableTyp) (wildcard_params: list P4String) - (parameters: list parameter). + (parameters: list parameter) + with parameter := + | Param (dir: direction) + (typ: surfaceTyp) + (default_value: option expression) + (variable: P4String) + with expression := + | ExpBool (b: bool) + | ExpString (s: P4String) + | ExpInt (i: P4Int). + (* | ExpSignedInt (). *) Inductive synthesizedTyp := | TypFunction (type_params: list variableTyp) @@ -95,16 +99,10 @@ Section Syntax. | TypTable (result_typ_name: P4String). Inductive typ := - | TypSurface (typ: surfaceTyp) - | TypDeclared (typ: declaredTyp) - | TypSynthesized (typ: synthesizedTyp). + | TypeSurface (typ: surfaceTyp) + | TypeDeclared (typ: declaredTyp) + | TypeSynthesized (typ: synthesizedTyp). (* | TypVoid. *) - (* Inductive expression := *) - (* | ExpBool (b: Bool) *) - (* | ExpString (s: P4String) *) - (* | ExpInt (i: P4Int) *) - (* | ExpSignedInt (). *) - End Syntax. From 45463ce3b61b8d87ffc92edf138c775441bb90ad Mon Sep 17 00:00:00 2001 From: pataei Date: Mon, 27 Mar 2023 22:42:58 -0400 Subject: [PATCH 06/25] syntax done --- coq/lib/Surface/Syntax/Syntax.v | 343 ++++++++++++++++++++++++++++---- 1 file changed, 299 insertions(+), 44 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index d04b6a081..a1935fdcd 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -30,79 +30,334 @@ Section Syntax. | FunFunction | FunBuiltin. + Variant uniOp : Type := + | Not + | BitNot + | UMinus. + + Variant binOp : Type := + | Plus + | PlusSat + | Minus + | MinusSat + | Mul + | Div + | Mod + | Shl + | Shr + | Le + | Ge + | Lt + | Gt + | Eq + | NotEq + | BitAnd + | BitXor + | BitOr + | PlusPlus + | And + | Or. + Inductive surfaceTyp := | TypBool | TypError | TypMatchKind | TypInteger | TypString - | TypInt (width: N) - | TypBit (width: N) - | TypVarBit (width: N) - | TypIdentifier (name: P4String) + | TypInt (width: N) + | TypBit (width: N) + | TypVarBit (width: N) + | TypIdentifier (name: P4String) | TypSpecialization (base: surfaceTyp) - (args: list surfaceTyp) - | TypHeaderStack (typ: surfaceTyp) - (size: N) - | TypTuple (types: list surfaceTyp). + (args: list surfaceTyp) + | TypHeaderStack (typ: surfaceTyp) + (size: N) + | TypTuple (types: list surfaceTyp). Variant functionTyp := | TypSurface (typ: surfaceTyp) | TypVoid - | TypVar (variable: variableTyp). + | TypVar (variable: variableTyp). Inductive declaredTyp := - | TypHeader (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) + | TypHeader (type_params: list variableTyp) + (fields: P4String.AList tags_t surfaceTyp) | TypHeaderUnion (type_params: list variableTyp) (fields: P4String.AList tags_t surfaceTyp) - | TypStruct (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) - | TypEnum (name: P4String) - (typ: option surfaceTyp) - (members: list P4String) - | TypParser (type_params: list variableTyp) - (parameters: list parameter) - | TypControl (type_params: list variableTyp) - (parameters: list parameter) - | TypPackage (type_params: list variableTyp) - (wildcard_params: list P4String) - (parameters: list parameter) + | TypStruct (type_params: list variableTyp) + (fields: P4String.AList tags_t surfaceTyp) + | TypEnum (name: P4String) + (typ: option surfaceTyp) + (members: list P4String) + | TypParser (type_params: list variableTyp) + (parameters: list parameter) + | TypControl (type_params: list variableTyp) + (parameters: list parameter) + | TypPackage (type_params: list variableTyp) + (wildcard_params: list P4String) + (parameters: list parameter) with parameter := | Param (dir: direction) (typ: surfaceTyp) (default_value: option expression) (variable: P4String) + with expressionPreT := + | ExpBool (b: bool) + | ExpString (s: P4String) + | ExpInt (i: P4Int) + (* | ExpSignedInt (*how come neither p4light nor surface has this*) *) + (* | ExpBitString (*how come neither p4light nor surface has this*) *) + | ExpName (name: P4String) (*why would it be typed.name?*) + | ExpArrayAccess (array: expression) + (index: expression) + | ExpBitStringAccess (bits: expression) + (lo: expression) + (high: expression) + | ExpList (value: list expression) + | ExpRecord (entries: P4String.AList tags_t expression) + | ExpUnaryOp (op: uniOp) + (arg: expression) + | ExpBinaryOp (op: binOp) + (arg1: expression) + (arg2: expression) + | ExpCast (typ: typ) (*this is different from p4 spec.*) + (expr: expression) + | ExpTypeMember (typ: P4String) + (mem: P4String) + | ExpErrorMember (mem: P4String) + | ExpExpressionMember (expr: expression) + (mem: P4String) + | ExpTernary (cond: expression) + (tru: expression) + (fls: expression) + | ExpFunctionCall (func: expression) + (type_args: list surfaceTyp) (*can the IR have any type variables?*) + (args: list argument) + | ExpAnonymousInstantiation (typ: surfaceTyp) + (args: list argument) + | ExpBitmask (expr: expression) + (mask: expression) + | ExpRange (low: expression) + (high: expression) with expression := - | ExpBool (b: bool) - | ExpString (s: P4String) - | ExpInt (i: P4Int). - (* | ExpSignedInt (). *) - - Inductive synthesizedTyp := - | TypFunction (type_params: list variableTyp) - (parameters: list parameter) - (kind: functionKind) - (ret: functionTyp) - | TypSet (typ: surfaceTyp) - | TypExtern (extern_name: P4String) - | TypRecord (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) - | TypNewTyp (name: P4String) - (typ: surfaceTyp) - | TypAction (data_params: list parameter) - (ctrl_params: list parameter) + | MkExpression (tags: tags_t) + (expr: expressionPreT) + (* (typ: typ) *) + (* (dir: direction) *) + with argument := + | ExpArg (value: expression) + | KeyValueArg (key: P4String) + (value: expression) + | MissingArg (*can the IR have any missing?*) + with synthesizedTyp := + | TypFunction (type_params: list variableTyp) + (parameters: list parameter) + (kind: functionKind) + (ret: functionTyp) + | TypSet (typ: surfaceTyp) + | TypExtern (extern_name: P4String) + | TypRecord (type_params: list variableTyp) + (fields: P4String.AList tags_t surfaceTyp) + | TypNewTyp (name: P4String) + (typ: surfaceTyp) + | TypAction (data_params: list parameter) + (ctrl_params: list parameter) | TypConstructor (type_params: list variableTyp) (wildcard_params: list P4String) (params: list parameter) (ret: functionTyp) - | TypTable (result_typ_name: P4String). - - Inductive typ := + | TypTable (result_typ_name: P4String) + with typ := | TypeSurface (typ: surfaceTyp) | TypeDeclared (typ: declaredTyp) | TypeSynthesized (typ: synthesizedTyp). (* | TypVoid. *) + Variant stmtSwitchLabel := + | StmtSwitchLabelDefault (tags: tags_t) + | StmtSwitchLabelName (tags: tags_t) + (label: P4String). + + Inductive stmtSwitchCases := + | StmtSwitchCaseAction (tags: tags_t) + (lable: stmtSwitchLabel) + (code: block) + | StmtSwitchCaseFallThrough (tags: tags_t) + (lable: stmtSwitchLabel) + with statementPreT := (*not sure why surface.ml has declaration in statements and p4light has variable and instantiation in it.*) + | StmtMethodCall (func: expression) + (type_args: list surfaceTyp) + (args: list argument) + | StmtAssignment (lhs: expression) + (rhs: expression) + | StmtdirectApplication (typ: surfaceTyp) + (args: list argument) + | StmtConditional (cond: expression) + (tru: statement) + (fls: option statement) + | StmtBlock (block: block) + | StmtExit + | StmtEmpty + | StmtReturn (expr: option expression) + | StmtSwitch (expr: expression) + (cases: list stmtSwitchCases) + with statement := + | MkStatement (tags: tags_t) + (stmt: statementPreT) + (* (typ: typ). *) + with block := + | BlockEmpty (tags: tags_t) + | BlockCons (statement: statement) + (rest: block). + + Variant tableOrParserMatch := + | MatchDefault (tags: tags_t) + | MatchDontCare (tags: tags_t) + | MatchExpression (tags: tags_t) + (expr: expression). + + Variant parserCase := + | ParserCase (tags: tags_t) + (matches: list tableOrParserMatch) + (next: P4String). + + Variant parserTransition := + | ParserDirect (tags: tags_t) + (next: P4String) + | ParserSelect (tags: tags_t) + (exprs: list expression) + (cases: list parserCase). + + Variant parserState := + | ParserState (tags: tags_t) + (name: P4String) + (statements: list statement) + (transistion: parserTransition). + + Variant fieldType := + | FieldType (typ: surfaceTyp) + (field: P4String). + + Variant methodPrototype := + | ProtoConstructor (tags: tags_t) + (name: P4String) + (params: list parameter) + | ProtoAbstractMethod (tags: tags_t) + (ret_type: surfaceTyp) + (name: P4String) + (type_params: list P4String) + (params: list parameter) + | ProtoMethod (tags: tags_t) + (ret_type: surfaceTyp) + (name: P4String) + (type_params: list P4String) + (params: list parameter). + + Variant tableKey := + | TabKey (tags: tags_t) + (key: expression) + (match_kind: P4String). + + Variant actionRef := + | TabActionRef (tags: tags_t) + (name: P4String) (*it's name in surface.ml.*) + (args: list argument). + + Variant tableEntry := + | TabEntry (tags: tags_t) + (matches: list tableOrParserMatch) + (action: actionRef). + + Variant tableProperty := + | TableKey (tags: tags_t) + (keys: list tableKey) + | TableActions (tags: tags_t) + (actions: list actionRef) + | TableEntries (tags: tags_t) + (entries: list tableEntry) + | TableDefaultAction (tags: tags_t) + (action: actionRef) + (const: bool) + | TableCustom (tags: tags_t) + (name: P4String) + (value: expression) + (const: bool). + + Inductive declarationPreT := + | DeclConstant (typ: surfaceTyp) + (name: P4String) + (value: expression) + | DeclInstantiation (typ: surfaceTyp) + (args: list argument) + (name: P4String) + (init: list declaration) + | DeclParser (name: P4String) + (type_params: list P4String) + (params: list parameter) + (constructor_params: list parameter) + (locals: declaration) + (states: list parserState) + | DeclControl (name: P4String) + (type_params: list P4String) + (params: list parameter) + (constructor_params: list parameter) + (locals: list declaration) + (apply: block) + | DeclFunction (ret_typ: functionTyp) + (name: P4String) + (type_params: list P4String) + (params: list parameter) + (body: block) + | DeclExternFunction (ret_type: surfaceTyp) + (name: P4String) + (type_params: list P4String) + (params: list parameter) + | DeclVariable (typ: surfaceTyp) + (name: P4String) + (init: option expression) + | DeclValueSet (typ: surfaceTyp) + (name: P4String) + (size: expression) + | DeclAction (name: P4String) + (data_params: list parameter) + (ctrl_params: list parameter) + (body: block) + | DeclTable (name: P4String) + (props: list tableProperty) + | DeclHeaderTyp (name: P4String) + (fields: list fieldType) + | DeclHeaderUnionTyp (name: P4String) + (fields: list fieldType) + | DeclStructTyp (name: P4String) + (fields: list fieldType) + | DeclError (members: list P4String) + | DeclMatchKind (members: list P4String) + | DeclEnumTyp (name: P4String) + (members: list P4String) + | DeclSerializableEnum (typ: surfaceTyp) + (name: P4String) + (members: P4String.AList tags_t expression) + | DeclControlTyp (name: P4String) + (type_params: list P4String) + (params: list parameter) + | DeclParserTyp (name: P4String) + (type_params: list P4String) + (params: list parameter) + | DeclPackageTyp (name: P4String) + (type_params: list P4String) + (params: list parameter) + | DeclExternObject (name: P4String) + (type_params: list P4String) + (methods: list methodPrototype) + | DeclTypeDef (name: P4String) + (typ_or_dcl: (surfaceTyp + declaration)) + | DeclNewType (name: P4String) + (typ_or_dcl: (surfaceTyp + declaration)) + with declaration := + | MkDeclaration (tags: tags_t) + (decl: declarationPreT). + (* (typ: typ). *) + + End Syntax. From a94117a57766aaafc8bc87ea827df429ed3b7172 Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 28 Mar 2023 09:33:20 -0400 Subject: [PATCH 07/25] comments --- coq/lib/Surface/Syntax/Syntax.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index a1935fdcd..7dd3cc238 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -57,7 +57,7 @@ Section Syntax. | PlusPlus | And | Or. - +(*add info, and option type. initially have none for type. *) Inductive surfaceTyp := | TypBool | TypError @@ -80,7 +80,7 @@ Section Syntax. | TypVar (variable: variableTyp). Inductive declaredTyp := - | TypHeader (type_params: list variableTyp) + | TypHeader (type_params: list variableTyp) (*needs to represent both before and after inference. *) (fields: P4String.AList tags_t surfaceTyp) | TypHeaderUnion (type_params: list variableTyp) (fields: P4String.AList tags_t surfaceTyp) From 90c41ff6f8a35dfdcb3778c73f6a43ddad2bc175 Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 28 Mar 2023 15:45:24 -0400 Subject: [PATCH 08/25] all types in one --- coq/lib/Surface/Syntax/Syntax.v | 139 +++++++++++++++----------------- 1 file changed, 64 insertions(+), 75 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 7dd3cc238..938f82683 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -18,9 +18,6 @@ Section Syntax. | InOut | Directionless. - Variant variableTyp := - | TypVariable (variable: P4String). - Variant functionKind := | FunParser | FunControl @@ -57,8 +54,9 @@ Section Syntax. | PlusPlus | And | Or. + (*add info, and option type. initially have none for type. *) - Inductive surfaceTyp := + Inductive typPreT := | TypBool | TypError | TypMatchKind @@ -68,45 +66,59 @@ Section Syntax. | TypBit (width: N) | TypVarBit (width: N) | TypIdentifier (name: P4String) - | TypSpecialization (base: surfaceTyp) - (args: list surfaceTyp) - | TypHeaderStack (typ: surfaceTyp) - (size: N) - | TypTuple (types: list surfaceTyp). - - Variant functionTyp := - | TypSurface (typ: surfaceTyp) - | TypVoid - | TypVar (variable: variableTyp). - - Inductive declaredTyp := - | TypHeader (type_params: list variableTyp) (*needs to represent both before and after inference. *) - (fields: P4String.AList tags_t surfaceTyp) - | TypHeaderUnion (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) - | TypStruct (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) + | TypSpecialization (base: typ) (*surface*) + (args: list typ) (*type arg*) + | TypHeaderStack (typ: typ) (*surface*) + (size: expression) + | TypTuple (types: list typ) (*surface*) + | TypHeader (type_params: list typ) (*type variable*) + (*needs to represent both before and after inference. *) + (fields: P4String.AList tags_t typ) (*surface*) + | TypHeaderUnion (type_params: list typ) (*variable type*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypStruct (type_params: list typ) (*variable type*) + (fields: P4String.AList tags_t typ) (*surface*) | TypEnum (name: P4String) - (typ: option surfaceTyp) + (typ: option typ) (*surface*) (members: list P4String) - | TypParser (type_params: list variableTyp) + | TypParser (type_params: list typ) (*type variable*) (parameters: list parameter) - | TypControl (type_params: list variableTyp) + | TypControl (type_params: list typ) (*type variable*) (parameters: list parameter) - | TypPackage (type_params: list variableTyp) + | TypPackage (type_params: list typ) (*type variable*) (wildcard_params: list P4String) (parameters: list parameter) + | TypFunction (type_params: list typ) (*type variable*) + (parameters: list parameter) + (kind: functionKind) + (ret: typ) (*surface+void+type variable*) + | TypSet (typ: typ) (*surface*) + | TypExtern (extern_name: P4String) + | TypRecord (type_params: list P4String) (*type variable*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypNewTyp (name: P4String) + (typ: typ) (*surface*) + | TypAction (data_params: list parameter) + (ctrl_params: list parameter) + | TypConstructor (type_params: list typ) (*type variable*) + (wildcard_params: list P4String) + (params: list parameter) + (ret: typ) (*surface+void+type variable*) + | TypTable (result_typ_name: P4String) + | TypVoid + | TypVar (variable: P4String) + with typ := + | MkType (tags: tags_t) + (typ: typPreT) with parameter := | Param (dir: direction) - (typ: surfaceTyp) + (typ: typ) (*surface*) (default_value: option expression) (variable: P4String) with expressionPreT := | ExpBool (b: bool) | ExpString (s: P4String) | ExpInt (i: P4Int) - (* | ExpSignedInt (*how come neither p4light nor surface has this*) *) - (* | ExpBitString (*how come neither p4light nor surface has this*) *) | ExpName (name: P4String) (*why would it be typed.name?*) | ExpArrayAccess (array: expression) (index: expression) @@ -120,7 +132,7 @@ Section Syntax. | ExpBinaryOp (op: binOp) (arg1: expression) (arg2: expression) - | ExpCast (typ: typ) (*this is different from p4 spec.*) + | ExpCast (typ: typ) (*surface*) (expr: expression) | ExpTypeMember (typ: P4String) (mem: P4String) @@ -131,9 +143,9 @@ Section Syntax. (tru: expression) (fls: expression) | ExpFunctionCall (func: expression) - (type_args: list surfaceTyp) (*can the IR have any type variables?*) + (type_args: list typ) (*surface*) (args: list argument) - | ExpAnonymousInstantiation (typ: surfaceTyp) + | ExpAnonymousInstantiation (typ: typ) (*surface*) (args: list argument) | ExpBitmask (expr: expression) (mask: expression) @@ -142,36 +154,13 @@ Section Syntax. with expression := | MkExpression (tags: tags_t) (expr: expressionPreT) - (* (typ: typ) *) + (typ: option typ) (* (dir: direction) *) with argument := | ExpArg (value: expression) | KeyValueArg (key: P4String) (value: expression) - | MissingArg (*can the IR have any missing?*) - with synthesizedTyp := - | TypFunction (type_params: list variableTyp) - (parameters: list parameter) - (kind: functionKind) - (ret: functionTyp) - | TypSet (typ: surfaceTyp) - | TypExtern (extern_name: P4String) - | TypRecord (type_params: list variableTyp) - (fields: P4String.AList tags_t surfaceTyp) - | TypNewTyp (name: P4String) - (typ: surfaceTyp) - | TypAction (data_params: list parameter) - (ctrl_params: list parameter) - | TypConstructor (type_params: list variableTyp) - (wildcard_params: list P4String) - (params: list parameter) - (ret: functionTyp) - | TypTable (result_typ_name: P4String) - with typ := - | TypeSurface (typ: surfaceTyp) - | TypeDeclared (typ: declaredTyp) - | TypeSynthesized (typ: synthesizedTyp). - (* | TypVoid. *) + | MissingArg. Variant stmtSwitchLabel := | StmtSwitchLabelDefault (tags: tags_t) @@ -186,11 +175,11 @@ Section Syntax. (lable: stmtSwitchLabel) with statementPreT := (*not sure why surface.ml has declaration in statements and p4light has variable and instantiation in it.*) | StmtMethodCall (func: expression) - (type_args: list surfaceTyp) + (type_args: list typ) (*surface*) (args: list argument) | StmtAssignment (lhs: expression) (rhs: expression) - | StmtdirectApplication (typ: surfaceTyp) + | StmtdirectApplication (typ: typ) (*surface*) (args: list argument) | StmtConditional (cond: expression) (tru: statement) @@ -204,7 +193,7 @@ Section Syntax. with statement := | MkStatement (tags: tags_t) (stmt: statementPreT) - (* (typ: typ). *) + (typ: option typ) with block := | BlockEmpty (tags: tags_t) | BlockCons (statement: statement) @@ -235,7 +224,7 @@ Section Syntax. (transistion: parserTransition). Variant fieldType := - | FieldType (typ: surfaceTyp) + | FieldType (typ: typ) (*surface*) (field: P4String). Variant methodPrototype := @@ -243,12 +232,12 @@ Section Syntax. (name: P4String) (params: list parameter) | ProtoAbstractMethod (tags: tags_t) - (ret_type: surfaceTyp) + (ret_type: typ) (*surface*) (name: P4String) (type_params: list P4String) (params: list parameter) | ProtoMethod (tags: tags_t) - (ret_type: surfaceTyp) + (ret_type: typ) (*surfce*) (name: P4String) (type_params: list P4String) (params: list parameter). @@ -260,7 +249,7 @@ Section Syntax. Variant actionRef := | TabActionRef (tags: tags_t) - (name: P4String) (*it's name in surface.ml.*) + (name: P4String) (*TODO: it's name in surface.ml.*) (args: list argument). Variant tableEntry := @@ -284,10 +273,10 @@ Section Syntax. (const: bool). Inductive declarationPreT := - | DeclConstant (typ: surfaceTyp) + | DeclConstant (typ: typ) (*surface*) (name: P4String) (value: expression) - | DeclInstantiation (typ: surfaceTyp) + | DeclInstantiation (typ: typ) (*surface*) (args: list argument) (name: P4String) (init: list declaration) @@ -303,19 +292,19 @@ Section Syntax. (constructor_params: list parameter) (locals: list declaration) (apply: block) - | DeclFunction (ret_typ: functionTyp) + | DeclFunction (ret_typ: typ) (*surface+void+type variable*) (name: P4String) (type_params: list P4String) (params: list parameter) (body: block) - | DeclExternFunction (ret_type: surfaceTyp) + | DeclExternFunction (ret_type: typ) (*surface*) (name: P4String) (type_params: list P4String) (params: list parameter) - | DeclVariable (typ: surfaceTyp) + | DeclVariable (typ: typ) (*surface*) (name: P4String) (init: option expression) - | DeclValueSet (typ: surfaceTyp) + | DeclValueSet (typ: typ) (*surface*) (name: P4String) (size: expression) | DeclAction (name: P4String) @@ -334,7 +323,7 @@ Section Syntax. | DeclMatchKind (members: list P4String) | DeclEnumTyp (name: P4String) (members: list P4String) - | DeclSerializableEnum (typ: surfaceTyp) + | DeclSerializableEnum (typ: typ) (*surface*) (name: P4String) (members: P4String.AList tags_t expression) | DeclControlTyp (name: P4String) @@ -350,13 +339,13 @@ Section Syntax. (type_params: list P4String) (methods: list methodPrototype) | DeclTypeDef (name: P4String) - (typ_or_dcl: (surfaceTyp + declaration)) + (typ_or_dcl: (typ + declaration)) (*surface*) | DeclNewType (name: P4String) - (typ_or_dcl: (surfaceTyp + declaration)) + (typ_or_dcl: (typ + declaration)) (*surface*) with declaration := | MkDeclaration (tags: tags_t) - (decl: declarationPreT). - (* (typ: typ). *) + (decl: declarationPreT) + (typ: option typ). End Syntax. From d1b72e65194207bf244509aed1ce3a3e5e9a6265 Mon Sep 17 00:00:00 2001 From: pataei Date: Wed, 29 Mar 2023 18:15:57 -0400 Subject: [PATCH 09/25] surface ir to represent before and after type inference --- coq/lib/Surface/Syntax/Syntax.v | 93 +++++++++++++++++---------------- 1 file changed, 48 insertions(+), 45 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 938f82683..8ea241f04 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -71,45 +71,48 @@ Section Syntax. | TypHeaderStack (typ: typ) (*surface*) (size: expression) | TypTuple (types: list typ) (*surface*) - | TypHeader (type_params: list typ) (*type variable*) - (*needs to represent both before and after inference. *) - (fields: P4String.AList tags_t typ) (*surface*) - | TypHeaderUnion (type_params: list typ) (*variable type*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypStruct (type_params: list typ) (*variable type*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypEnum (name: P4String) - (typ: option typ) (*surface*) - (members: list P4String) - | TypParser (type_params: list typ) (*type variable*) - (parameters: list parameter) - | TypControl (type_params: list typ) (*type variable*) - (parameters: list parameter) - | TypPackage (type_params: list typ) (*type variable*) - (wildcard_params: list P4String) - (parameters: list parameter) - | TypFunction (type_params: list typ) (*type variable*) - (parameters: list parameter) - (kind: functionKind) - (ret: typ) (*surface+void+type variable*) - | TypSet (typ: typ) (*surface*) - | TypExtern (extern_name: P4String) - | TypRecord (type_params: list P4String) (*type variable*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypNewTyp (name: P4String) - (typ: typ) (*surface*) - | TypAction (data_params: list parameter) - (ctrl_params: list parameter) - | TypConstructor (type_params: list typ) (*type variable*) - (wildcard_params: list P4String) - (params: list parameter) - (ret: typ) (*surface+void+type variable*) - | TypTable (result_typ_name: P4String) + | TypHeader (type_params: list typVarTyp) + (*type variable or their assignment*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypHeaderUnion (type_params: list typVarTyp) (*variable type*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypStruct (type_params: list typVarTyp) (*variable type*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypEnum (name: P4String) + (typ: option typ) (*surface*) + (members: list P4String) + | TypParser (type_params: list typVarTyp) (*type variable*) + (parameters: list parameter) + | TypControl (type_params: list typVarTyp) (*type variable*) + (parameters: list parameter) + | TypPackage (type_params: list typVarTyp) (*type variable*) + (wildcard_params: list P4String) + (parameters: list parameter) + | TypFunction (type_params: list typVarTyp) (*type variable*) + (parameters: list parameter) + (kind: functionKind) + (ret: typ) (*surface+void+type variable*) + | TypSet (typ: typ) (*surface*) + | TypExtern (extern_name: P4String) + | TypRecord (type_params: list typVarTyp) (*type variable*) + (fields: P4String.AList tags_t typ) (*surface*) + | TypNewTyp (name: P4String) + (typ: typ) (*surface*) + | TypAction (data_params: list parameter) + (ctrl_params: list parameter) + | TypConstructor (type_params: list typVarTyp) (*type variable*) + (wildcard_params: list typVarTyp) + (params: list parameter) + (ret: typ) (*surface+void+type variable*) + | TypTable (result_typ_name: P4String) | TypVoid - | TypVar (variable: P4String) + (* | TypVar (variable: P4String) *) with typ := | MkType (tags: tags_t) (typ: typPreT) + with typVarTyp := + | TypVarTyp (type_var: P4String) + (type: option typ) with parameter := | Param (dir: direction) (typ: typ) (*surface*) @@ -234,12 +237,12 @@ Section Syntax. | ProtoAbstractMethod (tags: tags_t) (ret_type: typ) (*surface*) (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) | ProtoMethod (tags: tags_t) (ret_type: typ) (*surfce*) (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter). Variant tableKey := @@ -281,25 +284,25 @@ Section Syntax. (name: P4String) (init: list declaration) | DeclParser (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) (constructor_params: list parameter) (locals: declaration) (states: list parserState) | DeclControl (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) (constructor_params: list parameter) (locals: list declaration) (apply: block) | DeclFunction (ret_typ: typ) (*surface+void+type variable*) (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) (body: block) | DeclExternFunction (ret_type: typ) (*surface*) (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) | DeclVariable (typ: typ) (*surface*) (name: P4String) @@ -327,16 +330,16 @@ Section Syntax. (name: P4String) (members: P4String.AList tags_t expression) | DeclControlTyp (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) | DeclParserTyp (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) | DeclPackageTyp (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (params: list parameter) | DeclExternObject (name: P4String) - (type_params: list P4String) + (type_params: list typVarTyp) (methods: list methodPrototype) | DeclTypeDef (name: P4String) (typ_or_dcl: (typ + declaration)) (*surface*) From b33b964c32f9961ccc7784ff0a9f89b259708edd Mon Sep 17 00:00:00 2001 From: pataei Date: Wed, 29 Mar 2023 20:47:38 -0400 Subject: [PATCH 10/25] added stmt decl --- coq/lib/Surface/Syntax/Syntax.v | 116 ++++++++++++++++---------------- 1 file changed, 58 insertions(+), 58 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 8ea241f04..538ac5367 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -12,6 +12,11 @@ Section Syntax. Notation P4String := (P4String.t tags_t). Notation P4Int := (P4Int.t tags_t). + Variant name := + | BareName (name: P4String) + | QualifiedName (namespaces: list P4String) + (name: P4String). + Variant direction := | In | Out @@ -55,7 +60,6 @@ Section Syntax. | And | Or. -(*add info, and option type. initially have none for type. *) Inductive typPreT := | TypBool | TypError @@ -72,7 +76,6 @@ Section Syntax. (size: expression) | TypTuple (types: list typ) (*surface*) | TypHeader (type_params: list typVarTyp) - (*type variable or their assignment*) (fields: P4String.AList tags_t typ) (*surface*) | TypHeaderUnion (type_params: list typVarTyp) (*variable type*) (fields: P4String.AList tags_t typ) (*surface*) @@ -105,12 +108,11 @@ Section Syntax. (params: list parameter) (ret: typ) (*surface+void+type variable*) | TypTable (result_typ_name: P4String) - | TypVoid - (* | TypVar (variable: P4String) *) + | TypVoid with typ := | MkType (tags: tags_t) (typ: typPreT) - with typVarTyp := + with typVarTyp := (*type variable or their assignment*) | TypVarTyp (type_var: P4String) (type: option typ) with parameter := @@ -122,7 +124,7 @@ Section Syntax. | ExpBool (b: bool) | ExpString (s: P4String) | ExpInt (i: P4Int) - | ExpName (name: P4String) (*why would it be typed.name?*) + | ExpName (name: name) | ExpArrayAccess (array: expression) (index: expression) | ExpBitStringAccess (bits: expression) @@ -165,43 +167,15 @@ Section Syntax. (value: expression) | MissingArg. + Variant fieldType := + | FieldType (typ: typ) (*surface*) + (field: P4String). + Variant stmtSwitchLabel := | StmtSwitchLabelDefault (tags: tags_t) | StmtSwitchLabelName (tags: tags_t) (label: P4String). - Inductive stmtSwitchCases := - | StmtSwitchCaseAction (tags: tags_t) - (lable: stmtSwitchLabel) - (code: block) - | StmtSwitchCaseFallThrough (tags: tags_t) - (lable: stmtSwitchLabel) - with statementPreT := (*not sure why surface.ml has declaration in statements and p4light has variable and instantiation in it.*) - | StmtMethodCall (func: expression) - (type_args: list typ) (*surface*) - (args: list argument) - | StmtAssignment (lhs: expression) - (rhs: expression) - | StmtdirectApplication (typ: typ) (*surface*) - (args: list argument) - | StmtConditional (cond: expression) - (tru: statement) - (fls: option statement) - | StmtBlock (block: block) - | StmtExit - | StmtEmpty - | StmtReturn (expr: option expression) - | StmtSwitch (expr: expression) - (cases: list stmtSwitchCases) - with statement := - | MkStatement (tags: tags_t) - (stmt: statementPreT) - (typ: option typ) - with block := - | BlockEmpty (tags: tags_t) - | BlockCons (statement: statement) - (rest: block). - Variant tableOrParserMatch := | MatchDefault (tags: tags_t) | MatchDontCare (tags: tags_t) @@ -213,24 +187,7 @@ Section Syntax. (matches: list tableOrParserMatch) (next: P4String). - Variant parserTransition := - | ParserDirect (tags: tags_t) - (next: P4String) - | ParserSelect (tags: tags_t) - (exprs: list expression) - (cases: list parserCase). - - Variant parserState := - | ParserState (tags: tags_t) - (name: P4String) - (statements: list statement) - (transistion: parserTransition). - - Variant fieldType := - | FieldType (typ: typ) (*surface*) - (field: P4String). - - Variant methodPrototype := + Variant methodPrototype := | ProtoConstructor (tags: tags_t) (name: P4String) (params: list parameter) @@ -252,7 +209,7 @@ Section Syntax. Variant actionRef := | TabActionRef (tags: tags_t) - (name: P4String) (*TODO: it's name in surface.ml.*) + (name: name) (args: list argument). Variant tableEntry := @@ -275,7 +232,50 @@ Section Syntax. (value: expression) (const: bool). - Inductive declarationPreT := + Inductive stmtSwitchCases := + | StmtSwitchCaseAction (tags: tags_t) + (lable: stmtSwitchLabel) + (code: block) + | StmtSwitchCaseFallThrough (tags: tags_t) + (lable: stmtSwitchLabel) + with statementPreT := (*why surface.ml has declaration in statements and p4light has variable and instantiation in it? *) + | StmtMethodCall (func: expression) + (type_args: list typ) (*surface*) + (args: list argument) + | StmtAssignment (lhs: expression) + (rhs: expression) + | StmtdirectApplication (typ: typ) (*surface*) + (args: list argument) + | StmtConditional (cond: expression) + (tru: statement) + (fls: option statement) + | StmtBlock (block: block) + | StmtExit + | StmtEmpty + | StmtReturn (expr: option expression) + | StmtSwitch (expr: expression) + (cases: list stmtSwitchCases) + | StmtDeclaration (dcl: declaration) (*can only be variable or constant decl.*) + with statement := + | MkStatement (tags: tags_t) + (stmt: statementPreT) + (typ: option typ) + with block := + | BlockEmpty (tags: tags_t) + | BlockCons (statement: statement) + (rest: block) + with parserTransition := + | ParserDirect (tags: tags_t) + (next: P4String) + | ParserSelect (tags: tags_t) + (exprs: list expression) + (cases: list parserCase) + with parserState := + | ParserState (tags: tags_t) + (name: P4String) + (statements: list statement) + (transistion: parserTransition) + with declarationPreT := | DeclConstant (typ: typ) (*surface*) (name: P4String) (value: expression) From 8c4a377f1fd0b46e877238588121f441ff2e9fef Mon Sep 17 00:00:00 2001 From: pataei Date: Sun, 2 Apr 2023 18:00:07 -0400 Subject: [PATCH 11/25] applied comments..inlined tags except for expr stmt and decl --- coq/lib/Surface/Syntax/Syntax.v | 270 +++++++++++++++++--------------- 1 file changed, 148 insertions(+), 122 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 538ac5367..7cb849973 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -3,115 +3,138 @@ Require Import Coq.Strings.String. From Coq Require Import Numbers.BinNums Classes.EquivDec. +From Poulet4.P4light.Syntax Require Import Info. + From Poulet4.P4light.Syntax Require P4String P4Int. Section Syntax. - Context {tags_t: Type}. - Notation P4String := (P4String.t tags_t). - Notation P4Int := (P4Int.t tags_t). + Notation P4String := (P4String.t Info). + Notation P4Int := (P4Int.t Info). Variant name := - | BareName (name: P4String) - | QualifiedName (namespaces: list P4String) + | BareName (tags: Info) + (name: P4String) + | QualifiedName (tags: Info) + (namespaces: list P4String) (name: P4String). Variant direction := - | In - | Out - | InOut - | Directionless. + | In (tags: Info) + | Out (tags: Info) + | InOut (tags: Info) + | Directionless (tags: Info). Variant functionKind := - | FunParser - | FunControl - | FunExtern - | FunTable - | FunAction - | FunFunction - | FunBuiltin. + | FunParser (tags: Info) + | FunControl (tags: Info) + | FunExtern (tags: Info) + | FunTable (tags: Info) + | FunAction (tags: Info) + | FunFunction (tags: Info) + | FunBuiltin (tags: Info). Variant uniOp : Type := - | Not - | BitNot - | UMinus. + | Not (tags: Info) + | BitNot (tags: Info) + | UMinus (tags: Info). Variant binOp : Type := - | Plus - | PlusSat - | Minus - | MinusSat - | Mul - | Div - | Mod - | Shl - | Shr - | Le - | Ge - | Lt - | Gt - | Eq - | NotEq - | BitAnd - | BitXor - | BitOr - | PlusPlus - | And - | Or. + | Plus (tags: Info) + | PlusSat (tags: Info) + | Minus (tags: Info) + | MinusSat (tags: Info) + | Mul (tags: Info) + | Div (tags: Info) + | Mod (tags: Info) + | Shl (tags: Info) + | Shr (tags: Info) + | Le (tags: Info) + | Ge (tags: Info) + | Lt (tags: Info) + | Gt (tags: Info) + | Eq (tags: Info) + | NotEq (tags: Info) + | BitAnd (tags: Info) + | BitXor (tags: Info) + | BitOr (tags: Info) + | PlusPlus (tags: Info) + | And (tags: Info) + | Or (tags: Info). - Inductive typPreT := - | TypBool - | TypError - | TypMatchKind - | TypInteger - | TypString - | TypInt (width: N) - | TypBit (width: N) - | TypVarBit (width: N) - | TypIdentifier (name: P4String) - | TypSpecialization (base: typ) (*surface*) + Inductive typ := + | TypBool (tags: Info) + | TypError (tags: Info) + | TypMatchKind (tags: Info) + | TypInteger (tags: Info) + | TypString (tags: Info) + | TypInt (tags: Info) + (width: N) + | TypBit (tags: Info) + (width: N) + | TypVarBit (tags: Info) + (width: N) + | TypIdentifier (tags: Info) + (name: P4String) + | TypSpecialization (tags: Info) + (base: typ) (*surface*) (args: list typ) (*type arg*) - | TypHeaderStack (typ: typ) (*surface*) + | TypHeaderStack (tags: Info) + (typ: typ) (*surface*) (size: expression) - | TypTuple (types: list typ) (*surface*) - | TypHeader (type_params: list typVarTyp) - (fields: P4String.AList tags_t typ) (*surface*) - | TypHeaderUnion (type_params: list typVarTyp) (*variable type*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypStruct (type_params: list typVarTyp) (*variable type*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypEnum (name: P4String) + | TypTuple (tags: Info) + (types: list typ) (*surface*) + | TypHeader (tags: Info) + (type_params: list typVarTyp) + (fields: P4String.AList Info typ) (*surface*) + | TypHeaderUnion (tags: Info) + (type_params: list typVarTyp) (*variable type*) + (fields: P4String.AList Info typ) (*surface*) + | TypStruct (tags: Info) + (type_params: list typVarTyp) (*variable type*) + (fields: P4String.AList Info typ) (*surface*) + | TypEnum (tags: Info) + (name: P4String) (typ: option typ) (*surface*) (members: list P4String) - | TypParser (type_params: list typVarTyp) (*type variable*) + | TypParser (tags: Info) + (type_params: list typVarTyp) (*type variable*) (parameters: list parameter) - | TypControl (type_params: list typVarTyp) (*type variable*) + | TypControl (tags: Info) + (type_params: list typVarTyp) (*type variable*) (parameters: list parameter) - | TypPackage (type_params: list typVarTyp) (*type variable*) + | TypPackage (tags: Info) + (type_params: list typVarTyp) (*type variable*) (wildcard_params: list P4String) (parameters: list parameter) - | TypFunction (type_params: list typVarTyp) (*type variable*) + | TypFunction (tags: Info) + (type_params: list typVarTyp) (*type variable*) (parameters: list parameter) (kind: functionKind) (ret: typ) (*surface+void+type variable*) - | TypSet (typ: typ) (*surface*) - | TypExtern (extern_name: P4String) - | TypRecord (type_params: list typVarTyp) (*type variable*) - (fields: P4String.AList tags_t typ) (*surface*) - | TypNewTyp (name: P4String) + | TypSet (tags: Info) (typ: typ) (*surface*) - | TypAction (data_params: list parameter) + | TypExtern (tags: Info) + (extern_name: P4String) + | TypRecord (tags: Info) + (type_params: list typVarTyp) (*type variable*) + (fields: P4String.AList Info typ) (*surface*) + | TypNewTyp (tags: Info) + (name: P4String) + (typ: typ) (*surface*) + | TypAction (tags: Info) + (data_params: list parameter) (ctrl_params: list parameter) - | TypConstructor (type_params: list typVarTyp) (*type variable*) + | TypConstructor (tags: Info) + (type_params: list typVarTyp) (*type variable*) (wildcard_params: list typVarTyp) (params: list parameter) (ret: typ) (*surface+void+type variable*) - | TypTable (result_typ_name: P4String) - | TypVoid - with typ := - | MkType (tags: tags_t) - (typ: typPreT) + | TypTable (tags: Info) + (result_typ_name: P4String) + | TypVoid (tags: Info) + | TypDontCare (tags: Info) with typVarTyp := (*type variable or their assignment*) | TypVarTyp (type_var: P4String) (type: option typ) @@ -128,10 +151,10 @@ Section Syntax. | ExpArrayAccess (array: expression) (index: expression) | ExpBitStringAccess (bits: expression) - (lo: expression) + (low: expression) (high: expression) | ExpList (value: list expression) - | ExpRecord (entries: P4String.AList tags_t expression) + | ExpRecord (entries: P4String.AList Info expression) | ExpUnaryOp (op: uniOp) (arg: expression) | ExpBinaryOp (op: binOp) @@ -152,14 +175,14 @@ Section Syntax. (args: list argument) | ExpAnonymousInstantiation (typ: typ) (*surface*) (args: list argument) - | ExpBitmask (expr: expression) + | ExpBitMask (expr: expression) (mask: expression) | ExpRange (low: expression) (high: expression) with expression := - | MkExpression (tags: tags_t) + | MkExpression (tags: Info) + (type: option typ) (expr: expressionPreT) - (typ: option typ) (* (dir: direction) *) with argument := | ExpArg (value: expression) @@ -167,84 +190,84 @@ Section Syntax. (value: expression) | MissingArg. - Variant fieldType := - | FieldType (typ: typ) (*surface*) - (field: P4String). + (* Variant fieldType := *) + (* | FieldType (typ: typ) (*surface*) *) + (* (field: P4String). *) Variant stmtSwitchLabel := - | StmtSwitchLabelDefault (tags: tags_t) - | StmtSwitchLabelName (tags: tags_t) + | StmtSwitchLabelDefault (tags: Info) + | StmtSwitchLabelName (tags: Info) (label: P4String). Variant tableOrParserMatch := - | MatchDefault (tags: tags_t) - | MatchDontCare (tags: tags_t) - | MatchExpression (tags: tags_t) + | MatchDefault (tags: Info) + | MatchDontCare (tags: Info) + | MatchExpression (tags: Info) (expr: expression). Variant parserCase := - | ParserCase (tags: tags_t) + | ParserCase (tags: Info) (matches: list tableOrParserMatch) (next: P4String). - Variant methodPrototype := - | ProtoConstructor (tags: tags_t) + Variant methodPrototype := + | ProtoConstructor (tags: Info) (name: P4String) (params: list parameter) - | ProtoAbstractMethod (tags: tags_t) + | ProtoAbstractMethod (tags: Info) (ret_type: typ) (*surface*) (name: P4String) (type_params: list typVarTyp) (params: list parameter) - | ProtoMethod (tags: tags_t) + | ProtoMethod (tags: Info) (ret_type: typ) (*surfce*) (name: P4String) (type_params: list typVarTyp) (params: list parameter). Variant tableKey := - | TabKey (tags: tags_t) + | TabKey (tags: Info) (key: expression) (match_kind: P4String). Variant actionRef := - | TabActionRef (tags: tags_t) + | TabActionRef (tags: Info) (name: name) (args: list argument). Variant tableEntry := - | TabEntry (tags: tags_t) + | TabEntry (tags: Info) (matches: list tableOrParserMatch) (action: actionRef). Variant tableProperty := - | TableKey (tags: tags_t) + | TableKey (tags: Info) (keys: list tableKey) - | TableActions (tags: tags_t) + | TableActions (tags: Info) (actions: list actionRef) - | TableEntries (tags: tags_t) + | TableEntries (tags: Info) (entries: list tableEntry) - | TableDefaultAction (tags: tags_t) + | TableDefaultAction (tags: Info) (action: actionRef) (const: bool) - | TableCustom (tags: tags_t) + | TableCustom (tags: Info) (name: P4String) (value: expression) (const: bool). Inductive stmtSwitchCases := - | StmtSwitchCaseAction (tags: tags_t) + | StmtSwitchCaseAction (tags: Info) (lable: stmtSwitchLabel) (code: block) - | StmtSwitchCaseFallThrough (tags: tags_t) + | StmtSwitchCaseFallThrough (tags: Info) (lable: stmtSwitchLabel) - with statementPreT := (*why surface.ml has declaration in statements and p4light has variable and instantiation in it? *) + with statementPreT := | StmtMethodCall (func: expression) (type_args: list typ) (*surface*) (args: list argument) | StmtAssignment (lhs: expression) (rhs: expression) - | StmtdirectApplication (typ: typ) (*surface*) + | StmtDirectApplication (typ: typ) (*surface*) (args: list argument) | StmtConditional (cond: expression) (tru: statement) @@ -255,23 +278,23 @@ Section Syntax. | StmtReturn (expr: option expression) | StmtSwitch (expr: expression) (cases: list stmtSwitchCases) - | StmtDeclaration (dcl: declaration) (*can only be variable or constant decl.*) + | StmtDeclaration (decl: declaration) (*can only be variable or constant decl.*) with statement := - | MkStatement (tags: tags_t) + | MkStatement (tags: Info) + (type: option typ) (stmt: statementPreT) - (typ: option typ) with block := - | BlockEmpty (tags: tags_t) - | BlockCons (statement: statement) - (rest: block) + | BlockEmpty (tags: Info) + | BlockCons (statement: statement) + (rest: block) with parserTransition := - | ParserDirect (tags: tags_t) + | ParserDirect (tags: Info) (next: P4String) - | ParserSelect (tags: tags_t) + | ParserSelect (tags: Info) (exprs: list expression) (cases: list parserCase) with parserState := - | ParserState (tags: tags_t) + | ParserState (tags: Info) (name: P4String) (statements: list statement) (transistion: parserTransition) @@ -317,18 +340,18 @@ Section Syntax. | DeclTable (name: P4String) (props: list tableProperty) | DeclHeaderTyp (name: P4String) - (fields: list fieldType) + (fields: P4String.AList Info typ) | DeclHeaderUnionTyp (name: P4String) - (fields: list fieldType) + (fields: P4String.AList Info typ) | DeclStructTyp (name: P4String) - (fields: list fieldType) + (fields: P4String.AList Info typ) | DeclError (members: list P4String) | DeclMatchKind (members: list P4String) | DeclEnumTyp (name: P4String) (members: list P4String) | DeclSerializableEnum (typ: typ) (*surface*) (name: P4String) - (members: P4String.AList tags_t expression) + (members: P4String.AList Info expression) | DeclControlTyp (name: P4String) (type_params: list typVarTyp) (params: list parameter) @@ -346,9 +369,12 @@ Section Syntax. | DeclNewType (name: P4String) (typ_or_dcl: (typ + declaration)) (*surface*) with declaration := - | MkDeclaration (tags: tags_t) - (decl: declarationPreT) - (typ: option typ). + | MkDeclaration (tags: Info) + (type: option typ) + (decl: declarationPreT). + + Variant program := + | Program (decls: list declaration). End Syntax. From b83d349b9a1cffa4b495ee37f92bc8283f4a6465 Mon Sep 17 00:00:00 2001 From: pataei Date: Thu, 6 Apr 2023 12:58:52 -0400 Subject: [PATCH 12/25] syntax fixed --- coq/lib/Surface/Syntax/Syntax.v | 69 +++++++++++++++++++++------------ 1 file changed, 44 insertions(+), 25 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 7cb849973..d9086079c 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -17,9 +17,19 @@ Section Syntax. | BareName (tags: Info) (name: P4String) | QualifiedName (tags: Info) - (namespaces: list P4String) + (namespaces: list P4String) (*namespace can only be empty. it's top level names.*) (name: P4String). + Definition get_name (name: name) : option P4String := + match name with + | BareName tags name + => Some name + | QualifiedName tags nil name + => Some name + | _ + => None + end. + Variant direction := | In (tags: Info) | Out (tags: Info) @@ -86,30 +96,30 @@ Section Syntax. | TypTuple (tags: Info) (types: list typ) (*surface*) | TypHeader (tags: Info) - (type_params: list typVarTyp) + (type_params: list P4String) (fields: P4String.AList Info typ) (*surface*) | TypHeaderUnion (tags: Info) - (type_params: list typVarTyp) (*variable type*) + (type_params: list P4String) (*variable type*) (fields: P4String.AList Info typ) (*surface*) | TypStruct (tags: Info) - (type_params: list typVarTyp) (*variable type*) + (type_params: list P4String) (*variable type*) (fields: P4String.AList Info typ) (*surface*) | TypEnum (tags: Info) (name: P4String) (typ: option typ) (*surface*) (members: list P4String) | TypParser (tags: Info) - (type_params: list typVarTyp) (*type variable*) + (type_params: list P4String) (*type variable*) (parameters: list parameter) | TypControl (tags: Info) - (type_params: list typVarTyp) (*type variable*) + (type_params: list P4String) (*type variable*) (parameters: list parameter) | TypPackage (tags: Info) - (type_params: list typVarTyp) (*type variable*) + (type_params: list P4String) (*type variable*) (wildcard_params: list P4String) (parameters: list parameter) | TypFunction (tags: Info) - (type_params: list typVarTyp) (*type variable*) + (type_params: list P4String) (*type variable*) (parameters: list parameter) (kind: functionKind) (ret: typ) (*surface+void+type variable*) @@ -118,7 +128,7 @@ Section Syntax. | TypExtern (tags: Info) (extern_name: P4String) | TypRecord (tags: Info) - (type_params: list typVarTyp) (*type variable*) + (type_params: list P4String) (*type variable*) (fields: P4String.AList Info typ) (*surface*) | TypNewTyp (tags: Info) (name: P4String) @@ -127,17 +137,17 @@ Section Syntax. (data_params: list parameter) (ctrl_params: list parameter) | TypConstructor (tags: Info) - (type_params: list typVarTyp) (*type variable*) - (wildcard_params: list typVarTyp) + (type_params: list P4String) (*type variable*) + (wildcard_params: list P4String) (params: list parameter) (ret: typ) (*surface+void+type variable*) | TypTable (tags: Info) (result_typ_name: P4String) | TypVoid (tags: Info) | TypDontCare (tags: Info) - with typVarTyp := (*type variable or their assignment*) - | TypVarTyp (type_var: P4String) - (type: option typ) + (* with typVarTyp := (*type variable or their assignment*) *) + (* | TypVarTyp (type_var: P4String) *) + (* (type: option typ) *) with parameter := | Param (dir: direction) (typ: typ) (*surface*) @@ -217,12 +227,12 @@ Section Syntax. | ProtoAbstractMethod (tags: Info) (ret_type: typ) (*surface*) (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) | ProtoMethod (tags: Info) (ret_type: typ) (*surfce*) (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter). Variant tableKey := @@ -278,7 +288,16 @@ Section Syntax. | StmtReturn (expr: option expression) | StmtSwitch (expr: expression) (cases: list stmtSwitchCases) - | StmtDeclaration (decl: declaration) (*can only be variable or constant decl.*) + | StmtDeclConstant (typ: typ) + (name: P4String) + (value: expression) + | StmtDeclVariable (typ: typ) + (name: P4String) + (init: option expression) + | StmtDeclInstantiation (typ: typ) (*surface*) + (args: list argument) + (name: P4String) + (init: list declaration) with statement := | MkStatement (tags: Info) (type: option typ) @@ -307,25 +326,25 @@ Section Syntax. (name: P4String) (init: list declaration) | DeclParser (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) (constructor_params: list parameter) (locals: declaration) (states: list parserState) | DeclControl (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) (constructor_params: list parameter) (locals: list declaration) (apply: block) | DeclFunction (ret_typ: typ) (*surface+void+type variable*) (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) (body: block) | DeclExternFunction (ret_type: typ) (*surface*) (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) | DeclVariable (typ: typ) (*surface*) (name: P4String) @@ -353,16 +372,16 @@ Section Syntax. (name: P4String) (members: P4String.AList Info expression) | DeclControlTyp (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) | DeclParserTyp (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) | DeclPackageTyp (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (params: list parameter) | DeclExternObject (name: P4String) - (type_params: list typVarTyp) + (type_params: list P4String) (methods: list methodPrototype) | DeclTypeDef (name: P4String) (typ_or_dcl: (typ + declaration)) (*surface*) From 7edd71082818b824ac625fc080554574b0ed47aa Mon Sep 17 00:00:00 2001 From: pataei Date: Sat, 8 Apr 2023 14:01:54 -0400 Subject: [PATCH 13/25] putting structure in for simple type checker --- coq/lib/Surface/Typing/Checker.v | 269 ++++++++++++++++++++++++++++ coq/lib/Surface/Typing/CheckerEnv.v | 29 +++ 2 files changed, 298 insertions(+) create mode 100644 coq/lib/Surface/Typing/Checker.v create mode 100644 coq/lib/Surface/Typing/CheckerEnv.v diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v new file mode 100644 index 000000000..47860078e --- /dev/null +++ b/coq/lib/Surface/Typing/Checker.v @@ -0,0 +1,269 @@ +From Coq Require Import Lists.List + NArith.NArith + Strings.String + ZArith.ZArith. + +(* From Coq Require Import Numbers.BinNums Classes.EquivDec. *) +From Poulet4 Require Import Utils.AList + Monads.Option + Utils.AListUtil + (* Monads.Result *) + Surface.Syntax.Syntax + Surface.Typing.CheckerEnv + P4light.Syntax.Info + P4light.Syntax.P4Int + P4light.Semantics.Semantics. + +From Poulet4.P4light.Syntax Require P4String. + +Import Result ResultNotations. +(*initially have none for types when you parse from p4 to surface ir. *) + +Section Checker. + + (* Context {tags_t: Type}. *) + Notation P4String := (P4String.t Info). + Notation P4Int := (P4Int.t Info). + Notation Val := (@ValueBase bool). + + Definition type_int (tags: Info) (i: P4Int) : typ := + match width_signed i with + | None => TypInteger tags + | Some (width, true) => TypInt tags width + | Some (width, false) => TypBit tags width + end. + + (*dummy function definition for now. TODO: fill in.*) + Definition compile_time_eval (env: checkerEnvs) (exp: expression) : option Val := + match exp with + | _ => Some ValBaseNull + end. + + Definition compile_time_known (env: checkerEnvs) (exp: expression) : bool := + match compile_time_eval env exp with + | Some _ => true + | _ => false + end. + + + Definition is_numeric (env: checkerEnvs) (exp: expression) (type: typ) : bool := + match type with + | TypInt _ _ => true + | TypBit _ _ => true + | TypInteger _ => compile_time_known env exp + | _ => false + end. + + Definition is_bool (type: typ) : bool := + match type with + | TypBool _ => true + | _ => false + end. + + Definition is_fixed_width_int (type: typ) : bool := + match type with + | TypInt _ _ => true + | TypBit _ _ => true + | _ => false + end. + + Definition is_integer (type: typ) : bool := + match type with + | TypInteger _ => true + | _ => false + end. + + (*dummy function definition. fill in later. TODO.*) + Definition to_nat (val: Val) : nat := 0. + + (*dummy function definition. fill in later. TODO.*) + Definition type_bit_string_access (env: checkerEnvs) (w: N) (low: expression) (type_low: typ) (high: expression) (type_high: typ) : result Exn.t typ := + error (Exn.Other "fill out later."). + + (*dummy function definition. fill in later. TODO.*) + Definition binary_op_typing (env: checkerEnvs) (op: binOp) (arg1: expression) (type_arg1: typ) (arg2: expression) (type_arg2: typ) : result Exn.t typ := + error (Exn.Other "fill out later."). + + Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := + match expr with + | MkExpression tags type expr => + match expr with + | ExpBool b + => ok (TypBool tags) + | ExpString s + => ok (TypString tags) + | ExpInt i + => ok (type_int tags i) + | ExpName name + => let* name' := from_opt (get_name name) + (Exn.Other "qualified name failure") in + let* (t, d) := from_opt (get (varEnv env) name') + (Exn.Other "name not found") in + ok t + | ExpArrayAccess array index + => let* type_array := type_expression env tags array in + let* type_index := type_expression env tags index in + match type_array with + | TypHeaderStack tags typ size + => if is_numeric env index type_index + then ok typ + else error (Exn.Other "array index not numeric") + (*the following block has a weird error. ask Ryan.*) + (* | TypTuple tags types *) + (* => if is_integer type_index *) + (* then let* i := from_opt (compile_time_eval env index) *) + (* (Exn.Other "failure in compile_time_eval")in *) + (* let* idx := from_opt (array_access_idx_to_z i) *) + (* (Exn.Other "failure in array_access_idx_to_z")in *) + (* if andb (Nat.leb 1 (N.to_nat idx)) *) + (* (Nat.leb (N.to_nat idx) (List.length types)) *) + (* then ok (Znth_default (TypVoid tags) (idx) types) *) + (* else error (Exn.Other "array access index out of bound") *) + (* else error (Exn.Other "array access index not integer") *) + | _ => error (Exn.Other "array access type incorrect") + end + | ExpBitStringAccess bits low high + => let* type_bits := type_expression env tags bits in + let* type_low := type_expression env tags low in + let* type_high := type_expression env tags high in + match type_bits with + | TypInt t w => type_bit_string_access env w low type_low high type_high + | TypBit t w => type_bit_string_access env w low type_low high type_high + | _ => error (Exn.Other "bit string access type incorrect") + end + (* | ExpList value *) + (* => let types := map (type_expression env tags) value in *) + (* if In None types *) + (* then None *) + (* else *) + (* ok (map from_opt types) *) + (* | ExpRecord entries *) + (* => TypBool tags *) + | ExpUnaryOp op arg + => let* type_arg := type_expression env tags arg in + match op with + | Not tags + => if is_bool type_arg + then ok type_arg + else error (Exn.Other "unary arg type not bool") + | BitNot tags + => if is_fixed_width_int type_arg + then ok type_arg + else error (Exn.Other "unary arg type not fixed width") + | UMinus tags + => if is_numeric env arg type_arg + then ok type_arg + else error (Exn.Other "unary arg type not numeric") + end + | ExpBinaryOp op arg1 arg2 + => let* type_arg1 := type_expression env tags arg1 in + let* type_arg2 := type_expression env tags arg2 in + binary_op_typing env op arg1 type_arg1 arg2 type_arg2 + (* | ExpCast typ expr *) + (* => TypBool tags *) + (* | ExpTypeMember typ mem *) + (* => TypBool tags *) + (* | ExpErrorMember mem *) + (* => TypBool tags *) + (* | ExpExpressionMember expr mem *) + (* => TypBool tags *) + (* | ExpTernary cond tru fls *) + (* => TypBool tags *) + (* | ExpFunctionCall func type_args args *) + (* => TypBool tags *) + (* | ExpAnonymousInstantiation typ args *) + (* => TypBool tags *) + (* | ExpBitMask expr mask *) + (* => TypBool tags *) + (* | ExpRange low high *) + (* => TypBool tags *) + | _ => error (Exn.Other "filling out the func") + end + end. + + Definition type_statement (tags: Info) (stmt: statement ) : typ := + match stmt with + | MkStatement tags type stmt + => match stmt with + | StmtMethodCall func type_args args + => TypBool tags + | StmtAssignment lhs rhs + => TypBool tags + | StmtDirectApplication typ args + => TypBool tags + | StmtConditional cond tru fls + => TypBool tags + | StmtBlock block + => TypBool tags + | StmtExit + => TypBool tags + | StmtEmpty + => TypBool tags + | StmtReturn expr + => TypBool tags + | StmtSwitch expr cases + => TypBool tags + | StmtDeclConstant typ name value + => TypBool tags + | StmtDeclVariable typ name init + => TypBool tags + | StmtDeclInstantiation typ args name init + => TypBool tags + end + end. + + Definition type_declaration (tags: Info) (decl: declaration) : typ := + match decl with + | MkDeclaration tags type decl + => match decl with + | DeclConstant typ name value + => TypBool tags + | DeclInstantiation typ args name init + => TypBool tags + | DeclParser name type_params params constructor_params locals states + => TypBool tags + | DeclControl name type_params params constructor_params locals apply + => TypBool tags + | DeclFunction ret_type name type_params params body + => TypBool tags + | DeclExternFunction ret_type name type_params params + => TypBool tags + | DeclVariable typ name init + => TypBool tags + | DeclValueSet typ name size + => TypBool tags + | DeclAction name data_params ctrl_params body + => TypBool tags + | DeclTable name props + => TypBool tags + | DeclHeaderTyp name fields + => TypBool tags + | DeclHeaderUnionTyp name fields + => TypBool tags + | DeclStructTyp name fields + => TypBool tags + | DeclError members + => TypBool tags + | DeclMatchKind members + => TypBool tags + | DeclEnumTyp name members + => TypBool tags + | DeclSerializableEnum typ name members + => TypBool tags + | DeclControlTyp name type_params params + => TypBool tags + | DeclParserTyp name type_params params + => TypBool tags + | DeclPackageTyp name type_params params + => TypBool tags + | DeclExternObject name type_params methods + => TypBool tags + | DeclTypeDef name typ_or_dcl + => TypBool tags + | DeclNewType name typ_or_dcl + => TypBool tags + end + end. + +End Checker. + diff --git a/coq/lib/Surface/Typing/CheckerEnv.v b/coq/lib/Surface/Typing/CheckerEnv.v new file mode 100644 index 000000000..5d852874d --- /dev/null +++ b/coq/lib/Surface/Typing/CheckerEnv.v @@ -0,0 +1,29 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. + +(* From Coq Require Import Numbers.BinNums Classes.EquivDec. *) +From Poulet4.Surface.Syntax Require Import Syntax. +From Poulet4.P4light.Syntax Require Import Info ConstValue. + +From Poulet4.P4light.Syntax Require P4String. + + +Section CheckerEnv. + + Notation P4String := (P4String.t Info). + Notation P4Value := (@Value Info). (*for now using p4light values*) + (* Notation P4Int := (P4Int.t Info). *) + + Definition env (a : Type) := P4String.AList Info a. + + Record checkerEnvs := + { typeEnv: env typ; + typeSynEnv: env P4String; + varEnv: env (typ * direction); + constEnv: env P4Value; (*for now using p4light values*) + externEnv: env P4String; + }. + + +End CheckerEnv. + From a647a5ffd87f129c63219ff7f609b1e8c4de84c0 Mon Sep 17 00:00:00 2001 From: pataei Date: Sat, 8 Apr 2023 18:50:55 -0400 Subject: [PATCH 14/25] working on expr typing --- coq/lib/Surface/Typing/Checker.v | 51 ++++++++++++++++++++++++++++---- 1 file changed, 46 insertions(+), 5 deletions(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 47860078e..5c030f92f 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -84,6 +84,18 @@ Section Checker. Definition binary_op_typing (env: checkerEnvs) (op: binOp) (arg1: expression) (type_arg1: typ) (arg2: expression) (type_arg2: typ) : result Exn.t typ := error (Exn.Other "fill out later."). + (*dummy function definition. fill in later. TODO.*) + Definition cast (env:checkerEnvs) (typ1 typ2: typ) : bool := + false. + + (*dummy function definition. fill in later. TODO.*) + Definition lookup_type (type: P4String) (env: checkerEnvs) : result Exn.t typ := + error (Exn.Other "fill out later."). + + (*dummy function definition. fill in later. TODO.*) + Definition type_eq (typ1 typ2: typ) : bool := + false. + Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := match expr with | MkExpression tags type expr => @@ -159,16 +171,45 @@ Section Checker. => let* type_arg1 := type_expression env tags arg1 in let* type_arg2 := type_expression env tags arg2 in binary_op_typing env op arg1 type_arg1 arg2 type_arg2 - (* | ExpCast typ expr *) - (* => TypBool tags *) + | ExpCast typ expr + => let* type_expr := type_expression env tags expr in + match type_expr with + | TypIdentifier tags name + => let* typ' := lookup_type name env in + let cast_ok := cast env typ typ' in + if cast_ok + then ok typ + else error (Exn.Other "cast incorrect") + | _ + => let cast_ok := cast env typ type_expr in + if cast_ok + then ok typ + else error (Exn.Other "cast incorrect") + end (* | ExpTypeMember typ mem *) - (* => TypBool tags *) + (* => TypBool tags *) (* | ExpErrorMember mem *) (* => TypBool tags *) (* | ExpExpressionMember expr mem *) (* => TypBool tags *) - (* | ExpTernary cond tru fls *) - (* => TypBool tags *) + | ExpTernary cond tru fls + => let* type_cond := type_expression env tags cond in + let* type_tru := type_expression env tags tru in + let* type_fls := type_expression env tags fls in + match type_cond with + | TypBool _ + => match type_tru with + | TypInteger _ + => if andb (is_integer type_fls) + (compile_time_known env cond) + then ok type_tru + else error (Exn.Other "ternary type incorrect") + | _ => if type_eq type_tru type_fls + then ok type_tru + else error (Exn.Other "mismatch type tru fls ternary") + end + | _ => error (Exn.Other "ternary condition type incorrect") + end (* | ExpFunctionCall func type_args args *) (* => TypBool tags *) (* | ExpAnonymousInstantiation typ args *) From 981b6fca5e961957b8d42665aac2da05a72c1a02 Mon Sep 17 00:00:00 2001 From: pataei Date: Sat, 8 Apr 2023 19:10:22 -0400 Subject: [PATCH 15/25] next up membership rules --- coq/lib/Surface/Typing/Checker.v | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 5c030f92f..bc23cfe53 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -96,6 +96,20 @@ Section Checker. Definition type_eq (typ1 typ2: typ) : bool := false. + Definition mask_type (type_expr type_mask: typ) : result Exn.t typ := + match type_expr, type_mask with + | TypBit _ w, TypBit _ w' + => if (w == w') + then ok type_mask + else error (Exn.Other "mask incorrect") + | TypBit w _, TypInteger _ + => ok type_mask + | TypInteger _, TypBit w _ + => ok type_mask + | _, _ + => error (Exn.Other "mask incorrect") + end. + Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := match expr with | MkExpression tags type expr => @@ -214,10 +228,16 @@ Section Checker. (* => TypBool tags *) (* | ExpAnonymousInstantiation typ args *) (* => TypBool tags *) - (* | ExpBitMask expr mask *) - (* => TypBool tags *) - (* | ExpRange low high *) - (* => TypBool tags *) + | ExpBitMask expr mask + => let* type_expr := type_expression env tags expr in + let* type_mask := type_expression env tags mask in + mask_type type_expr type_mask + | ExpRange low high + => let* type_low := type_expression env tags low in + let* type_high := type_expression env tags high in + if andb (type_eq type_low type_high) (is_fixed_width_int type_low) + then ok (TypSet tags type_low) + else error (Exn.Other "range types incorrect") | _ => error (Exn.Other "filling out the func") end end. From 4e625e3d86950258a72b16ecc58975ae64979db3 Mon Sep 17 00:00:00 2001 From: pataei Date: Sat, 8 Apr 2023 19:42:26 -0400 Subject: [PATCH 16/25] switching to spec --- coq/lib/Surface/Typing/Checker.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index bc23cfe53..9190503a4 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -203,7 +203,7 @@ Section Checker. (* | ExpTypeMember typ mem *) (* => TypBool tags *) (* | ExpErrorMember mem *) - (* => TypBool tags *) + (* => *) (* | ExpExpressionMember expr mem *) (* => TypBool tags *) | ExpTernary cond tru fls From ae21c14c7c5dc10cfa1a99f148c1ac60b949b1ca Mon Sep 17 00:00:00 2001 From: pataei Date: Sat, 8 Apr 2023 20:49:31 -0400 Subject: [PATCH 17/25] have to clean up exp mem in doc --- coq/lib/Surface/Typing/Checker.v | 39 +++++++++++++++++++++++++++----- 1 file changed, 33 insertions(+), 6 deletions(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 9190503a4..d59bfff02 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -73,6 +73,12 @@ Section Checker. | _ => false end. + Definition is_error (type: typ) : bool := + match type with + | TypError _ => true + | _ => false + end. + (*dummy function definition. fill in later. TODO.*) Definition to_nat (val: Val) : nat := 0. @@ -92,6 +98,18 @@ Section Checker. Definition lookup_type (type: P4String) (env: checkerEnvs) : result Exn.t typ := error (Exn.Other "fill out later."). + (*dummy function definition. fill in later. TODO.*) + Definition lookup_var (type: P4String) (env: checkerEnvs) : result Exn.t (typ * direction) := + error (Exn.Other "fill out later."). + + (*dummy function definition. fill in later. TODO.*) + Definition append_error (mem: P4String) : P4String := + mem. + + (*dummy function definition. fill in later. TODO.*) + Definition append_type (typ: P4String) (mem: P4String) : P4String := + mem. + (*dummy function definition. fill in later. TODO.*) Definition type_eq (typ1 typ2: typ) : bool := false. @@ -110,6 +128,10 @@ Section Checker. => error (Exn.Other "mask incorrect") end. + (*dummy function definition. fill in later. TODO.*) + Definition type_expression_member (env: checkerEnvs) (type_expr: typ) (mem: P4String) : result Exn.t typ := + error (Exn.Other "fill in later."). + Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := match expr with | MkExpression tags type expr => @@ -200,12 +222,17 @@ Section Checker. then ok typ else error (Exn.Other "cast incorrect") end - (* | ExpTypeMember typ mem *) - (* => TypBool tags *) - (* | ExpErrorMember mem *) - (* => *) - (* | ExpExpressionMember expr mem *) - (* => TypBool tags *) + | ExpTypeMember typ mem + => let* (t, d) := lookup_var (append_type typ mem) env in + ok t + | ExpErrorMember mem (*discuss with nate. error member is redundant. type member would take care of it.*) + => let* (t, d) := lookup_var (append_error mem) env in + if is_error t + then ok t + else error (Exn.Other "error member type incorrect") + | ExpExpressionMember expr mem + => let* type_expr := type_expression env tags expr in + type_expression_member env type_expr mem | ExpTernary cond tru fls => let* type_cond := type_expression env tags cond in let* type_tru := type_expression env tags tru in From b8efdb0cc2fde22294e46afcae4d949c29fc8b40 Mon Sep 17 00:00:00 2001 From: pataei Date: Sun, 9 Apr 2023 11:42:09 -0400 Subject: [PATCH 18/25] list almost done..only func call and instantiatio left --- coq/lib/Surface/Syntax/Syntax.v | 7 +++-- coq/lib/Surface/Typing/Checker.v | 49 ++++++++++++++++---------------- 2 files changed, 29 insertions(+), 27 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index d9086079c..65b096708 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -127,9 +127,10 @@ Section Syntax. (typ: typ) (*surface*) | TypExtern (tags: Info) (extern_name: P4String) - | TypRecord (tags: Info) - (type_params: list P4String) (*type variable*) - (fields: P4String.AList Info typ) (*surface*) + (*discuss: we don't need record type, and we can just agree on assigning struct type to a list of field assignments and since struct type doesn't have a name it should be fine. *) + (* | TypRecord (tags: Info) *) + (* (type_params: list P4String) (*type variable*) *) + (* (fields: P4String.AList Info typ) (*surface*) *) | TypNewTyp (tags: Info) (name: P4String) (typ: typ) (*surface*) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index d59bfff02..8e94543bb 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -132,6 +132,28 @@ Section Checker. Definition type_expression_member (env: checkerEnvs) (type_expr: typ) (mem: P4String) : result Exn.t typ := error (Exn.Other "fill in later."). + (*the tuple case has little mismatches of types. TODO. fix it.*) + Definition type_array_access (env: checkerEnvs) (array: expression) (type_array: typ) (index: expression) (type_index: typ) : result Exn.t typ := + match type_array with + | TypHeaderStack tags typ size + => if is_numeric env index type_index + then ok typ + else error (Exn.Other "array index not numeric") + (*the following block has a weird error. ask Ryan.*) + (* | TypTuple tags types *) + (* => if is_integer type_index *) + (* then let* i := from_opt (compile_time_eval env index) *) + (* (Exn.Other "failure in compile_time_eval")in *) + (* let* idx := from_opt (array_access_idx_to_z i) *) + (* (Exn.Other "failure in array_access_idx_to_z")in *) + (* if andb (Nat.leb 1 (N.to_nat idx)) *) + (* (Nat.leb (N.to_nat idx) (List.length types)) *) + (* then ok (Znth_default (TypVoid tags) (idx) types) *) + (* else error (Exn.Other "array access index out of bound") *) + (* else error (Exn.Other "array access index not integer") *) + | _ => error (Exn.Other "array access type incorrect") + end. + Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := match expr with | MkExpression tags type expr => @@ -151,25 +173,7 @@ Section Checker. | ExpArrayAccess array index => let* type_array := type_expression env tags array in let* type_index := type_expression env tags index in - match type_array with - | TypHeaderStack tags typ size - => if is_numeric env index type_index - then ok typ - else error (Exn.Other "array index not numeric") - (*the following block has a weird error. ask Ryan.*) - (* | TypTuple tags types *) - (* => if is_integer type_index *) - (* then let* i := from_opt (compile_time_eval env index) *) - (* (Exn.Other "failure in compile_time_eval")in *) - (* let* idx := from_opt (array_access_idx_to_z i) *) - (* (Exn.Other "failure in array_access_idx_to_z")in *) - (* if andb (Nat.leb 1 (N.to_nat idx)) *) - (* (Nat.leb (N.to_nat idx) (List.length types)) *) - (* then ok (Znth_default (TypVoid tags) (idx) types) *) - (* else error (Exn.Other "array access index out of bound") *) - (* else error (Exn.Other "array access index not integer") *) - | _ => error (Exn.Other "array access type incorrect") - end + type_array_access env array type_array index type_index | ExpBitStringAccess bits low high => let* type_bits := type_expression env tags bits in let* type_low := type_expression env tags low in @@ -180,11 +184,8 @@ Section Checker. | _ => error (Exn.Other "bit string access type incorrect") end (* | ExpList value *) - (* => let types := map (type_expression env tags) value in *) - (* if In None types *) - (* then None *) - (* else *) - (* ok (map from_opt types) *) + (* => let* types := rred (map (type_expression env tags) value) in *) + (* ok (TypTuple types) *) (* | ExpRecord entries *) (* => TypBool tags *) | ExpUnaryOp op arg From f3cf4c6ad52c8b5737e8207e1ec688d6f16987de Mon Sep 17 00:00:00 2001 From: pataei Date: Thu, 13 Apr 2023 12:38:46 -0400 Subject: [PATCH 19/25] changes in meeting --- coq/lib/Surface/Syntax/Syntax.v | 4 ++-- coq/lib/Surface/Typing/Checker.v | 22 +++++++++++----------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 65b096708..156b03fd5 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -85,8 +85,8 @@ Section Syntax. (width: N) | TypVarBit (tags: Info) (width: N) - | TypIdentifier (tags: Info) - (name: P4String) + | TypIdentifier (tags: Info) + (name: string) | TypSpecialization (tags: Info) (base: typ) (*surface*) (args: list typ) (*type arg*) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 8e94543bb..9604dec4c 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -140,17 +140,17 @@ Section Checker. then ok typ else error (Exn.Other "array index not numeric") (*the following block has a weird error. ask Ryan.*) - (* | TypTuple tags types *) - (* => if is_integer type_index *) - (* then let* i := from_opt (compile_time_eval env index) *) - (* (Exn.Other "failure in compile_time_eval")in *) - (* let* idx := from_opt (array_access_idx_to_z i) *) - (* (Exn.Other "failure in array_access_idx_to_z")in *) - (* if andb (Nat.leb 1 (N.to_nat idx)) *) - (* (Nat.leb (N.to_nat idx) (List.length types)) *) - (* then ok (Znth_default (TypVoid tags) (idx) types) *) - (* else error (Exn.Other "array access index out of bound") *) - (* else error (Exn.Other "array access index not integer") *) + | TypTuple tags types + => if is_integer type_index + then let* i := from_opt (compile_time_eval env index) + (Exn.Other "failure in compile_time_eval")in + let* idx := from_opt (array_access_idx_to_z i) + (Exn.Other "failure in array_access_idx_to_z")in + if andb (Nat.leb 1 (N.to_nat idx)) + (Nat.leb (N.to_nat idx) (List.length types)) + then ok (Znth_default (TypVoid tags) (idx) types) + else error (Exn.Other "array access index out of bound") + else error (Exn.Other "array access index not integer") | _ => error (Exn.Other "array access type incorrect") end. From 345aaf8a037dc0abd947e5270dc2b9b7f49f69a8 Mon Sep 17 00:00:00 2001 From: pataei Date: Fri, 14 Apr 2023 13:05:40 -0400 Subject: [PATCH 20/25] added some comments --- coq/lib/Surface/Syntax/Syntax.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 156b03fd5..f694c8131 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -87,6 +87,7 @@ Section Syntax. (width: N) | TypIdentifier (tags: Info) (name: string) + (*keep the syntax for specialization but wouldn't have the type. so this typscpecialization will never be generated and it's only used for writing programs. because once it happens inference substitutes it in the type.*) | TypSpecialization (tags: Info) (base: typ) (*surface*) (args: list typ) (*type arg*) @@ -108,6 +109,9 @@ Section Syntax. (name: P4String) (typ: option typ) (*surface*) (members: list P4String) + (*after inference the type_params list must be empty. so you can substitute + type variables when they're instantiated for the parameters and the type_params + would be empty.*) | TypParser (tags: Info) (type_params: list P4String) (*type variable*) (parameters: list parameter) From d564e2cf5576d6b1ac1cef79bc7bb314fa2fbebd Mon Sep 17 00:00:00 2001 From: pataei Date: Mon, 17 Apr 2023 16:23:02 -0400 Subject: [PATCH 21/25] added comment --- coq/lib/Surface/Syntax/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index f694c8131..1d0efb8e7 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -377,7 +377,7 @@ Section Syntax. (name: P4String) (members: P4String.AList Info expression) | DeclControlTyp (name: P4String) - (type_params: list P4String) + (type_params: list P4String) (*wrong: control decl can't be generic. look p4 spec, sec 14: control blocks*) (params: list parameter) | DeclParserTyp (name: P4String) (type_params: list P4String) From c18f08b29fd1b484c7404f532e0a11b8bc7038ef Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 2 May 2023 10:17:03 -0400 Subject: [PATCH 22/25] break checker and utils --- coq/lib/Surface/Syntax/Syntax.v | 17 ++-- coq/lib/Surface/Typing/Checker.v | 129 ++++++++----------------------- coq/lib/Surface/Typing/Utils.v | 99 ++++++++++++++++++++++++ 3 files changed, 136 insertions(+), 109 deletions(-) create mode 100644 coq/lib/Surface/Typing/Utils.v diff --git a/coq/lib/Surface/Syntax/Syntax.v b/coq/lib/Surface/Syntax/Syntax.v index 1d0efb8e7..d1cfe63c2 100644 --- a/coq/lib/Surface/Syntax/Syntax.v +++ b/coq/lib/Surface/Syntax/Syntax.v @@ -85,8 +85,8 @@ Section Syntax. (width: N) | TypVarBit (tags: Info) (width: N) - | TypIdentifier (tags: Info) - (name: string) + | TypName (tags: Info) + (name: P4String) (*keep the syntax for specialization but wouldn't have the type. so this typscpecialization will never be generated and it's only used for writing programs. because once it happens inference substitutes it in the type.*) | TypSpecialization (tags: Info) (base: typ) (*surface*) @@ -150,9 +150,6 @@ Section Syntax. (result_typ_name: P4String) | TypVoid (tags: Info) | TypDontCare (tags: Info) - (* with typVarTyp := (*type variable or their assignment*) *) - (* | TypVarTyp (type_var: P4String) *) - (* (type: option typ) *) with parameter := | Param (dir: direction) (typ: typ) (*surface*) @@ -198,17 +195,13 @@ Section Syntax. | MkExpression (tags: Info) (type: option typ) (expr: expressionPreT) - (* (dir: direction) *) + (* (dir: direction) *)(*might need this for bidirectional typing. but leave it out for now.*) with argument := | ExpArg (value: expression) | KeyValueArg (key: P4String) (value: expression) | MissingArg. - (* Variant fieldType := *) - (* | FieldType (typ: typ) (*surface*) *) - (* (field: P4String). *) - Variant stmtSwitchLabel := | StmtSwitchLabelDefault (tags: Info) | StmtSwitchLabelName (tags: Info) @@ -307,6 +300,7 @@ Section Syntax. | MkStatement (tags: Info) (type: option typ) (stmt: statementPreT) + (* (dir: direction) *) with block := | BlockEmpty (tags: Info) | BlockCons (statement: statement) @@ -377,7 +371,7 @@ Section Syntax. (name: P4String) (members: P4String.AList Info expression) | DeclControlTyp (name: P4String) - (type_params: list P4String) (*wrong: control decl can't be generic. look p4 spec, sec 14: control blocks*) + (type_params: list P4String) (params: list parameter) | DeclParserTyp (name: P4String) (type_params: list P4String) @@ -396,6 +390,7 @@ Section Syntax. | MkDeclaration (tags: Info) (type: option typ) (decl: declarationPreT). + (* (dir: direction) *) Variant program := | Program (decls: list declaration). diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 9604dec4c..4ba06e968 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -10,6 +10,7 @@ From Poulet4 Require Import Utils.AList (* Monads.Result *) Surface.Syntax.Syntax Surface.Typing.CheckerEnv + Surface.Typing.Utils P4light.Syntax.Info P4light.Syntax.P4Int P4light.Semantics.Semantics. @@ -33,88 +34,19 @@ Section Checker. | Some (width, false) => TypBit tags width end. - (*dummy function definition for now. TODO: fill in.*) - Definition compile_time_eval (env: checkerEnvs) (exp: expression) : option Val := - match exp with - | _ => Some ValBaseNull - end. - - Definition compile_time_known (env: checkerEnvs) (exp: expression) : bool := - match compile_time_eval env exp with - | Some _ => true - | _ => false - end. - - - Definition is_numeric (env: checkerEnvs) (exp: expression) (type: typ) : bool := - match type with - | TypInt _ _ => true - | TypBit _ _ => true - | TypInteger _ => compile_time_known env exp - | _ => false - end. - - Definition is_bool (type: typ) : bool := - match type with - | TypBool _ => true - | _ => false - end. - - Definition is_fixed_width_int (type: typ) : bool := - match type with - | TypInt _ _ => true - | TypBit _ _ => true - | _ => false - end. - - Definition is_integer (type: typ) : bool := - match type with - | TypInteger _ => true - | _ => false - end. - - Definition is_error (type: typ) : bool := - match type with - | TypError _ => true - | _ => false - end. - - (*dummy function definition. fill in later. TODO.*) - Definition to_nat (val: Val) : nat := 0. - (*dummy function definition. fill in later. TODO.*) Definition type_bit_string_access (env: checkerEnvs) (w: N) (low: expression) (type_low: typ) (high: expression) (type_high: typ) : result Exn.t typ := error (Exn.Other "fill out later."). (*dummy function definition. fill in later. TODO.*) - Definition binary_op_typing (env: checkerEnvs) (op: binOp) (arg1: expression) (type_arg1: typ) (arg2: expression) (type_arg2: typ) : result Exn.t typ := + Definition type_binary_op (env: checkerEnvs) (op: binOp) (arg1: expression) (type_arg1: typ) (arg2: expression) (type_arg2: typ) : result Exn.t typ := error (Exn.Other "fill out later."). - (*dummy function definition. fill in later. TODO.*) - Definition cast (env:checkerEnvs) (typ1 typ2: typ) : bool := - false. - - (*dummy function definition. fill in later. TODO.*) - Definition lookup_type (type: P4String) (env: checkerEnvs) : result Exn.t typ := - error (Exn.Other "fill out later."). - - (*dummy function definition. fill in later. TODO.*) - Definition lookup_var (type: P4String) (env: checkerEnvs) : result Exn.t (typ * direction) := - error (Exn.Other "fill out later."). - - (*dummy function definition. fill in later. TODO.*) - Definition append_error (mem: P4String) : P4String := - mem. - - (*dummy function definition. fill in later. TODO.*) - Definition append_type (typ: P4String) (mem: P4String) : P4String := - mem. - (*dummy function definition. fill in later. TODO.*) Definition type_eq (typ1 typ2: typ) : bool := false. - Definition mask_type (type_expr type_mask: typ) : result Exn.t typ := + Definition type_mask (type_expr type_mask: typ) : result Exn.t typ := match type_expr, type_mask with | TypBit _ w, TypBit _ w' => if (w == w') @@ -132,27 +64,28 @@ Section Checker. Definition type_expression_member (env: checkerEnvs) (type_expr: typ) (mem: P4String) : result Exn.t typ := error (Exn.Other "fill in later."). - (*the tuple case has little mismatches of types. TODO. fix it.*) + (*the tuple case has little mismatches of types. TODO. fix it. for now returns a dummy value.*) Definition type_array_access (env: checkerEnvs) (array: expression) (type_array: typ) (index: expression) (type_index: typ) : result Exn.t typ := - match type_array with - | TypHeaderStack tags typ size - => if is_numeric env index type_index - then ok typ - else error (Exn.Other "array index not numeric") - (*the following block has a weird error. ask Ryan.*) - | TypTuple tags types - => if is_integer type_index - then let* i := from_opt (compile_time_eval env index) - (Exn.Other "failure in compile_time_eval")in - let* idx := from_opt (array_access_idx_to_z i) - (Exn.Other "failure in array_access_idx_to_z")in - if andb (Nat.leb 1 (N.to_nat idx)) - (Nat.leb (N.to_nat idx) (List.length types)) - then ok (Znth_default (TypVoid tags) (idx) types) - else error (Exn.Other "array access index out of bound") - else error (Exn.Other "array access index not integer") - | _ => error (Exn.Other "array access type incorrect") - end. + error (Exn.Other "fill in later."). + (* match type_array with *) + (* | TypHeaderStack tags typ size *) + (* => if is_numeric env index type_index *) + (* then ok typ *) + (* else error (Exn.Other "array index not numeric") *) + (* (*the following block has a weird error. ask Ryan.*) *) + (* | TypTuple tags types *) + (* => if is_integer type_index *) + (* then let* i := from_opt (compile_time_eval env index) *) + (* (Exn.Other "failure in compile_time_eval")in *) + (* let* idx := from_opt (array_access_idx_to_z i) *) + (* (Exn.Other "failure in array_access_idx_to_z")in *) + (* if andb (Nat.leb 1 (N.to_nat idx)) *) + (* (Nat.leb (N.to_nat idx) (List.length types)) *) + (* then ok typ (*(Znth_default (TypVoid tags) (idx) types)*) (*TODO: dummy value returned*) *) + (* else error (Exn.Other "array access index out of bound") *) + (* else error (Exn.Other "array access index not integer") *) + (* | _ => error (Exn.Other "array access type incorrect") *) + (* end. *) Fixpoint type_expression (env: checkerEnvs) (tags: Info) (expr: expression) : result Exn.t typ := match expr with @@ -207,11 +140,11 @@ Section Checker. | ExpBinaryOp op arg1 arg2 => let* type_arg1 := type_expression env tags arg1 in let* type_arg2 := type_expression env tags arg2 in - binary_op_typing env op arg1 type_arg1 arg2 type_arg2 + type_binary_op env op arg1 type_arg1 arg2 type_arg2 | ExpCast typ expr => let* type_expr := type_expression env tags expr in match type_expr with - | TypIdentifier tags name + | TypName tags name => let* typ' := lookup_type name env in let cast_ok := cast env typ typ' in if cast_ok @@ -226,9 +159,9 @@ Section Checker. | ExpTypeMember typ mem => let* (t, d) := lookup_var (append_type typ mem) env in ok t - | ExpErrorMember mem (*discuss with nate. error member is redundant. type member would take care of it.*) + | ExpErrorMember mem => let* (t, d) := lookup_var (append_error mem) env in - if is_error t + if is_type_error t then ok t else error (Exn.Other "error member type incorrect") | ExpExpressionMember expr mem @@ -257,9 +190,9 @@ Section Checker. (* | ExpAnonymousInstantiation typ args *) (* => TypBool tags *) | ExpBitMask expr mask - => let* type_expr := type_expression env tags expr in - let* type_mask := type_expression env tags mask in - mask_type type_expr type_mask + => let* typed_expr := type_expression env tags expr in + let* typed_mask := type_expression env tags mask in + type_mask typed_expr typed_mask | ExpRange low high => let* type_low := type_expression env tags low in let* type_high := type_expression env tags high in diff --git a/coq/lib/Surface/Typing/Utils.v b/coq/lib/Surface/Typing/Utils.v new file mode 100644 index 000000000..469cbaceb --- /dev/null +++ b/coq/lib/Surface/Typing/Utils.v @@ -0,0 +1,99 @@ +From Coq Require Import Lists.List + NArith.NArith + Strings.String + ZArith.ZArith. + +(* From Coq Require Import Numbers.BinNums Classes.EquivDec. *) +From Poulet4 Require Import Utils.AList + Monads.Option + Utils.AListUtil + (* Monads.Result *) + Surface.Syntax.Syntax + Surface.Typing.CheckerEnv + P4light.Syntax.Info + P4light.Syntax.P4Int + P4light.Semantics.Semantics. + +From Poulet4.P4light.Syntax Require P4String. + +Import Result ResultNotations. +(*initially have none for types when you parse from p4 to surface ir. *) + +Section Utils. + + (* Context {tags_t: Type}. *) + Notation P4String := (P4String.t Info). + Notation P4Int := (P4Int.t Info). + Notation Val := (@ValueBase bool). + + (*dummy function definition for now. TODO: fill in.*) + Definition compile_time_eval (env: checkerEnvs) (exp: expression) : option Val := + match exp with + | _ => Some ValBaseNull + end. + + Definition compile_time_known (env: checkerEnvs) (exp: expression) : bool := + match compile_time_eval env exp with + | Some _ => true + | _ => false + end. + + + Definition is_numeric (env: checkerEnvs) (exp: expression) (type: typ) : bool := + match type with + | TypInt _ _ => true + | TypBit _ _ => true + | TypInteger _ => compile_time_known env exp + | _ => false + end. + + Definition is_bool (type: typ) : bool := + match type with + | TypBool _ => true + | _ => false + end. + + Definition is_fixed_width_int (type: typ) : bool := + match type with + | TypInt _ _ => true + | TypBit _ _ => true + | _ => false + end. + + Definition is_integer (type: typ) : bool := + match type with + | TypInteger _ => true + | _ => false + end. + + Definition is_type_error (type: typ) : bool := + match type with + | TypError _ => true + | _ => false + end. + + (*dummy function definition. fill in later. TODO.*) + Definition to_nat (val: Val) : nat := 0. + + (*dummy function definition. fill in later. TODO.*) + Definition cast (env:checkerEnvs) (typ1 typ2: typ) : bool := + false. + + (*dummy function definition. fill in later. TODO.*) + Definition lookup_type (type: P4String) (env: checkerEnvs) : result Exn.t typ := + error (Exn.Other "fill out later."). + + (*dummy function definition. fill in later. TODO.*) + Definition lookup_var (type: P4String) (env: checkerEnvs) : result Exn.t (typ * direction) := + error (Exn.Other "fill out later."). + + (*dummy function definition. fill in later. TODO.*) + Definition append_error (mem: P4String) : P4String := + mem. + + (*dummy function definition. fill in later. TODO.*) + Definition append_type (typ: P4String) (mem: P4String) : P4String := + mem. + +End Utils. + From 83561c1fdee5cbf527b9115d2b5ebdc4b70d1897 Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 2 May 2023 11:42:44 -0400 Subject: [PATCH 23/25] binop helper ready for Harim to be filled out --- coq/lib/Surface/Typing/Checker.v | 39 +++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index 4ba06e968..d3d0e32e8 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -39,10 +39,47 @@ Section Checker. error (Exn.Other "fill out later."). (*dummy function definition. fill in later. TODO.*) + (*hint: binary operation rules in formalized spec. disregard the insertion of cast. that is, assume that all casts have been inserted.*) + (*hint: lib/checker.ml --> type_binary_op.*) Definition type_binary_op (env: checkerEnvs) (op: binOp) (arg1: expression) (type_arg1: typ) (arg2: expression) (type_arg2: typ) : result Exn.t typ := - error (Exn.Other "fill out later."). + match op with + | And _ + | Or _ + => error (Exn.Other "@Harim fill out.") + | Plus _ + | Minus _ + | Mul _ + => error (Exn.Other "@Harim fill out.") + | Eq _ + | NotEq _ + => error (Exn.Other "@Harim fill out.") + | PlusSat _ + | MinusSat _ + => error (Exn.Other "@Harim fill out.") + | BitAnd _ + | BitXor _ + | BitOr _ + => error (Exn.Other "@Harim fill out.") + | PlusPlus _ + => error (Exn.Other "@Harim fill out.") + | Le _ + | Ge _ + | Lt _ + | Gt _ + => error (Exn.Other "@Harim fill out.") + | Mod _ + | Div _ + => error (Exn.Other "@Harim fill out.") + | Shl _ + | Shr _ + => error (Exn.Other "@Harim fill out.") + end. (*dummy function definition. fill in later. TODO.*) + (*checks equality of two types. If they are equal it returns true, otherwise, it returns false.*) + (*assume all generic types have been instantiated. *) + (*hint: type equality judgment in formalized spec.*) + (*hint: lib/checker.ml --> type_equality function which calls solve_types. solve_types does the inference.*) Definition type_eq (typ1 typ2: typ) : bool := false. From c1f69d8487b5e20c23e8e2c01a97f3d148f71e84 Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 2 May 2023 12:37:32 -0400 Subject: [PATCH 24/25] structure for type eq --- coq/lib/Surface/Typing/Checker.v | 55 ++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 2 deletions(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index d3d0e32e8..d8625ea42 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -81,7 +81,55 @@ Section Checker. (*hint: type equality judgment in formalized spec.*) (*hint: lib/checker.ml --> type_equality function which calls solve_types. solve_types does the inference.*) Definition type_eq (typ1 typ2: typ) : bool := - false. + match typ1, typ2 with + | TypBool _, TypBool _ + | TypError _, TypError _ + | TypMatchKind _, TypMatchKind _ + | TypInteger _, TypInteger _ + | TypString _, TypString _ + | TypVoid _, TypVoid _ + | TypDontCare _, TypDontCare _ + => true + | TypBit _ w1, TypBit _ w2 + | TypInt _ w1, TypInt _ w2 + | TypVarBit _ w1, TypVarBit _ w2 + => false (* error (Exn.Other "fill out" )*) + | TypName _ n1, TypName _ n2 + => false (* "fill out" *) + | TypSpecialization _ b1 arg1, TypSpecialization _ b2 arg2 + => false (* "fill out" *) + | TypHeaderStack _ tps1 fs1, TypHeaderStack _ tps2 fs2 + | TypHeader _ tps1 fs1, TypHeader _ tps2 fs2 + | TypHeaderUnion _ tps1 fs1, TypHeaderUnion _ tps2 fs2 + | TypStruct _ tps1 fs1, TypStruct _ tps2 fs2 + => false (* "fill out" *) + | TypTuple _ ts1, TypTuple _ ts2 + => false (* "fill out" *) + | TypEnum _ n1 t1 ms1, TypEnum _ n2 t2 ms2 + => false (* "fill out" *) + | TypParser _ tps1 ps1, TypParser _ tps2 ps2 + | TypControl _ tps1 ps1, TypControl _ tps2 ps2 + => false (* "fill out" *) + | TypPackage _ tps1 wps1 ps1, TypPackage _ tps2 wps2 ps2 + => false (* "fill out" *) + | TypFunction _ tps1 ps1 k1 rt1, TypFunction _ tps2 ps2 k2 rt2 + => false (* "fill out" *) + | TypSet _ t1, TypSet _ t2 + => false (* "fill out" *) + | TypExtern _ n1, TypExtern _ n2 + => false (* "fill out" *) + | TypNewTyp _ n1 t1, TypNewTyp _ n2 t2 + => false (* "fill out" *) + | TypAction _ dps1 cps1, TypAction _ dps2 cps2 + => false (* "fill out" *) + | TypConstructor _ tps1 wp1 ps1 rt1, TypConstructor _ tps2 wp2 ps2 rt2 + => false (* "fill out" *) + | TypTable _ n1, TypTable _ n2 + => false (* "fill out" *) + | _, _ + => false (* "fill out" *) + end. + Definition type_mask (type_expr type_mask: typ) : result Exn.t typ := match type_expr, type_mask with @@ -98,10 +146,13 @@ Section Checker. end. (*dummy function definition. fill in later. TODO.*) + (*type checking for expression member.*) + (*hint: membership rules in formalized spec. this is simpler than Ryan's implementation.*) + (*hint: lib/checker.ml --> type_expression_member.*) Definition type_expression_member (env: checkerEnvs) (type_expr: typ) (mem: P4String) : result Exn.t typ := error (Exn.Other "fill in later."). - (*the tuple case has little mismatches of types. TODO. fix it. for now returns a dummy value.*) + (*the tuple case has little mismatches of types. TODO. fix it. for now returns a dummy value.@parisa*) Definition type_array_access (env: checkerEnvs) (array: expression) (type_array: typ) (index: expression) (type_index: typ) : result Exn.t typ := error (Exn.Other "fill in later."). (* match type_array with *) From 0f45e727867a1f5ab9a9a381ebf3df0243a8a206 Mon Sep 17 00:00:00 2001 From: pataei Date: Tue, 2 May 2023 13:27:46 -0400 Subject: [PATCH 25/25] added sufficient comments for all helpers --- coq/lib/Surface/Typing/Checker.v | 9 ++++++--- coq/lib/Surface/Typing/Utils.v | 14 +++++++++++--- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/coq/lib/Surface/Typing/Checker.v b/coq/lib/Surface/Typing/Checker.v index d8625ea42..1a462ff47 100644 --- a/coq/lib/Surface/Typing/Checker.v +++ b/coq/lib/Surface/Typing/Checker.v @@ -35,8 +35,11 @@ Section Checker. end. (*dummy function definition. fill in later. TODO.*) + (*hint: bitstring access rule from the formalized spec. ignore inserting casts rule.*) + (*hint: lib/checker.ml --> type_bit_string_access. *) + (*hint: similar to type_array_access a little down this file.*) Definition type_bit_string_access (env: checkerEnvs) (w: N) (low: expression) (type_low: typ) (high: expression) (type_high: typ) : result Exn.t typ := - error (Exn.Other "fill out later."). + error (Exn.Other "fill out."). (*dummy function definition. fill in later. TODO.*) (*hint: binary operation rules in formalized spec. disregard the insertion of cast. that is, assume that all casts have been inserted.*) @@ -234,12 +237,12 @@ Section Checker. match type_expr with | TypName tags name => let* typ' := lookup_type name env in - let cast_ok := cast env typ typ' in + let cast_ok := explicit_cast env typ typ' in if cast_ok then ok typ else error (Exn.Other "cast incorrect") | _ - => let cast_ok := cast env typ type_expr in + => let cast_ok := explicit_cast env typ type_expr in if cast_ok then ok typ else error (Exn.Other "cast incorrect") diff --git a/coq/lib/Surface/Typing/Utils.v b/coq/lib/Surface/Typing/Utils.v index 469cbaceb..229e98945 100644 --- a/coq/lib/Surface/Typing/Utils.v +++ b/coq/lib/Surface/Typing/Utils.v @@ -73,25 +73,33 @@ Section Utils. end. (*dummy function definition. fill in later. TODO.*) - Definition to_nat (val: Val) : nat := 0. + (*the nitty gritty converting between types.*) + (* Definition to_nat (val: Val) : nat := 0. *) (*dummy function definition. fill in later. TODO.*) - Definition cast (env:checkerEnvs) (typ1 typ2: typ) : bool := + (*pairs of types that allow explicit cast return true. otherwise it returns false.*) + (*@parisa, finalize this for the p4 spec pr of casting.*) + Definition explicit_cast (env:checkerEnvs) (typ1 typ2: typ) : bool := false. (*dummy function definition. fill in later. TODO.*) + (*looks up type variable type in environment env and return its type if it finds it. + otherwise, it returns error.*) Definition lookup_type (type: P4String) (env: checkerEnvs) : result Exn.t typ := error (Exn.Other "fill out later."). (*dummy function definition. fill in later. TODO.*) - Definition lookup_var (type: P4String) (env: checkerEnvs) : result Exn.t (typ * direction) := + (*looks up variable var in environment env and if it finds it, it returns the pair (typ, dir), otherwise returns an error.*) + Definition lookup_var (var: P4String) (env: checkerEnvs) : result Exn.t (typ * direction) := error (Exn.Other "fill out later."). (*dummy function definition. fill in later. TODO.*) + (*returns: error.mem *) Definition append_error (mem: P4String) : P4String := mem. (*dummy function definition. fill in later. TODO.*) + (*returns: typ.mem *) Definition append_type (typ: P4String) (mem: P4String) : P4String := mem.