aslt: fix some missing quotes and fix conflict.

cram: add test_cntlm.t
UQ-PAC · Mar 13, 2024 · 0dd10e5 · 0dd10e5
1 parent 3d5a06f
commit 0dd10e5
Show file tree

Hide file tree

Showing 9 changed files with 147,663 additions and 10 deletions.
diff --git a/libASL/Semantics.g4 b/libASL/Semantics.g4
@@ -0,0 +1,102 @@
+grammar Semantics;
+
+// borrowed from https://github.com/UQ-PAC/bil-to-boogie-translator/blob/main/src/main/antlr4/Semantics.g4
+
+// See aslp/libASL/asl.ott for reference grammar Bap-ali-plugin/asli_lifer.ml may also be useful for
+// visitors
+
+stmt: assignment_stmt | call_stmt | conditional_stmt;
+stmts: OPEN_BRACKET (stmt (SCOLON stmt)*)? CLOSE_BRACKET;
+
+stmt_lines: stmt* EOF;  // a convenient entry point for space-separated stmts, unused within this gramamr
+
+assignment_stmt:
+	'Stmt_Assign' OPEN_PAREN lexpr COMMA expr CLOSE_PAREN					# Assign
+	| 'Stmt_ConstDecl' OPEN_PAREN type COMMA ident COMMA expr CLOSE_PAREN	# ConstDecl
+	| 'Stmt_VarDecl' OPEN_PAREN type COMMA ident COMMA expr CLOSE_PAREN    # VarDecl
+	| 'Stmt_VarDeclsNoInit' OPEN_PAREN type COMMA OPEN_BRACKET OPEN_PAREN (ident (COMMA ident)*)? CLOSE_PAREN CLOSE_BRACKET CLOSE_PAREN  # VarDeclsNoInit
+	| 'Stmt_Assert' OPEN_PAREN expr CLOSE_PAREN # Assert
+	| 'Stmt_Throw' OPEN_PAREN message=ident+ CLOSE_PAREN # Throw;
+
+call_stmt:
+	'Stmt_TCall' OPEN_PAREN
+		ident COMMA
+
+		OPEN_BRACKET (targs (SCOLON targs)*)? CLOSE_BRACKET COMMA
+
+		OPEN_BRACKET (expr (SCOLON expr)*)? CLOSE_BRACKET
+
+		CLOSE_PAREN;
+
+conditional_stmt:
+	'Stmt_If' OPEN_PAREN expr COMMA
+	  tcase=stmts COMMA
+		OPEN_BRACKET CLOSE_BRACKET COMMA  // elseif chains are transformed away by aslp
+		fcase=stmts CLOSE_PAREN
+	# ConditionalStmt
+;
+
+type_register_slices:
+	(COMMA OPEN_PAREN OPEN_BRACKET 'Slice_HiLo' OPEN_PAREN expr COMMA expr CLOSE_PAREN CLOSE_BRACKET COMMA ident CLOSE_PAREN)*;
+
+type:
+	'Type_Bits' OPEN_PAREN expr CLOSE_PAREN  # TypeBits
+	| 'Type_Constructor(boolean)'            # TypeBoolean
+	| 'Type_Constructor(' name=ident ')'       # TypeConstructor
+	| 'Type_Register' OPEN_PAREN QUOTE width=integer QUOTE type_register_slices CLOSE_PAREN # TypeRegister;
+
+lexpr:
+	'LExpr_Var' OPEN_PAREN ident CLOSE_PAREN			# LExprVar
+	| 'LExpr_Field' OPEN_PAREN lexpr COMMA ident CLOSE_PAREN		# LExprField
+	| 'LExpr_Array' OPEN_PAREN (lexpr (COMMA expr)*)? CLOSE_PAREN	# LExprArray;
+
+expr:
+	'Expr_Var' OPEN_PAREN ident CLOSE_PAREN                                     # ExprVar
+	| 'Expr_TApply' OPEN_PAREN ident COMMA
+	    OPEN_BRACKET (targs (SCOLON targs)*)? CLOSE_BRACKET COMMA
+	    OPEN_BRACKET (expr (SCOLON expr)*)? CLOSE_BRACKET
+	    CLOSE_PAREN                                                             # ExprTApply
+	| 'Expr_Slices' OPEN_PAREN expr COMMA
+			OPEN_BRACKET slice_expr CLOSE_BRACKET
+			CLOSE_PAREN										                                          # ExprSlices
+	| 'Expr_Field' OPEN_PAREN expr COMMA ident CLOSE_PAREN                      # ExprField
+	| 'Expr_Array' OPEN_PAREN base=expr (COMMA indices+=expr)* CLOSE_PAREN			# ExprArray
+	| integer                                                                 	# ExprLitInt
+	| bits                                                                      # ExprLitBits
+	| OPEN_PAREN expr CLOSE_PAREN                                               # ExprParen
+	// | 'Expr_LitHex' OPEN_PAREN QUOTE HEXDIGIT+ QUOTE CLOSE_PAREN		# ExprLitHex
+	// | 'Expr_LitMask' OPEN_PAREN QUOTE BINARY QUOTE CLOSE_PAREN		# ExprLitMask
+	// | 'Expr_LitString' OPEN_PAREN QUOTE ident QUOTE CLOSE_PAREN		# ExprLitString
+;
+
+ident: QUOTE ID QUOTE;
+
+integer: DECIMAL;
+bits: BINARY;
+
+targs: expr;
+
+slice_expr: 'Slice_LoWd' OPEN_PAREN expr COMMA expr CLOSE_PAREN;
+
+BINARY: SQUOTE [0-1]+ SQUOTE;
+DECIMAL: [0-9]+;
+ID: [a-zA-Z_][a-zA-Z0-9_.]*;
+
+// Delimiters
+OPEN_PAREN: '(';
+CLOSE_PAREN: ')';
+COMMA: ',';
+OPEN_BRACKET: '[';
+CLOSE_BRACKET: ']';
+OPEN_CURLY: '{';
+CLOSE_CURLY: '}';
+SQUOTE: '\'';
+QUOTE: '"';
+EQUALS: '=';
+COLON: ':';
+SCOLON: ';';
+
+// Ignored
+NEWLINE: ('\r\n' | '\n') -> skip;
+WHITESPACE: ' '+ -> skip;
+COMMENT: '//' ~[\r\n]* -> skip;
diff --git a/libASL/asl.ott b/libASL/asl.ott
@@ -182,14 +182,14 @@ typeident :: '' ::=    {{ phantom }}
                        {{ ocaml ident }}
                        {{ com Type Identifier }}
                        {{ pp     l = PPrint.string (pprint_ident l) }}
-                       {{ pp-raw l = PPrint.string (pprint_ident l) }}
+                       {{ pp-raw l = PPrint.string ("\"" ^ pprint_ident l ^ "\"") }}
   | typeid             :: :: TypeIdent {{ ocaml Ident [[typeid]] }}
 
 anyident :: '' ::=     {{ phantom }}
                        {{ ocaml ident }}
                        {{ com Identifier (in a separate namespace from type identifiers) }}
                        {{ pp     l = PPrint.string (pprint_ident l) }}
-                       {{ pp-raw l = PPrint.string (pprint_ident l) }}
+                       {{ pp-raw l = PPrint.string ("\"" ^ pprint_ident l ^ "\"") }}
   | id                 :: :: AnyIdent {{ ocaml Ident [[id]] }}
   | typeid             :: :: AnyTypeIdent {{ ocaml Ident [[typeid]] }}
 
@@ -472,7 +472,7 @@ regfield :: 'RegField_' ::=
     {{ phantom }} {{ ocaml slice list * ident }}
     {{ pp-raw rf = string "([ "^^ separate (string ";\n") (List.map pp_raw_slice (fst rf)) ^^ string " ], " ^^ pp_raw_ident (snd rf) ^^ string ")" }}
     {{ pp rf = separate (string "\n") (List.map pp_slice (fst rf)) ^^ string " " ^^ pp_ident (snd rf) }}
-    | slice_list anyident  :: :: Field {{ ocaml ([[slice_list]], [[anyident]]) }}
+    | slice1 , ... , slicen anyident  :: :: Field {{ ocaml ([[slice1...slicen]], [[anyident]]) }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Statements

diff --git a/libASL/dune b/libASL/dune
@@ -1,7 +1,8 @@
 (ocamllex lexer)
 
 (menhir
- (modules asl_parser))
+ (modules asl_parser)
+ (flags (--explain)))
 
 (rule
  (targets asl_parser_pp.ml asl_parser.mly asl_lexer.mll asl_ast.ml)