Skip to content

Commit

Permalink
Fix parser crash after invalid PSL directive. Fixes nickg#1088
Browse files Browse the repository at this point in the history
  • Loading branch information
nickg committed Dec 5, 2024
1 parent 0e0181a commit 3fa98e3
Show file tree
Hide file tree
Showing 10 changed files with 80 additions and 7 deletions.
2 changes: 2 additions & 0 deletions src/lexer.l
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,7 @@ NONDET ?i:nondet
NONDET_V ?i:nondet_vector
UNION ?i:union
INF ?i:inf
ENDPOINT ?i:endpoint

INTERCONNECT ?i:interconnect
DELAYFILE ?i:delayfile
Expand Down Expand Up @@ -610,6 +611,7 @@ BEFORE ?i:before
<PSL>"|->" { TOKEN(tSUFFIXOVR); }
<PSL>"|=>" { TOKEN(tSUFFIXNON); }
<PSL>{INF} { TOKEN(tINF); }
<PSL>{ENDPOINT} { TOKEN(tENDPOINT); }

<VLOG>"module" { return tMODULE; }
<VLOG>"endmodule" { return tENDMODULE; }
Expand Down
59 changes: 54 additions & 5 deletions src/parse.c
Original file line number Diff line number Diff line change
Expand Up @@ -9573,6 +9573,7 @@ static void p_block_declarative_item(tree_t parent)
case tDEFAULT:
case tSEQUENCE:
case tPROPERTY:
case tENDPOINT:
p_psl_declaration(parent);
break;

Expand Down Expand Up @@ -10997,7 +10998,7 @@ static void p_concurrent_statement_or_psl(tree_t parent)
consume(tCOLON);
tree_add_stmt(parent, p_psl_directive(label));
}
else if (scan(tDEFAULT, tSEQUENCE, tPROPERTY))
else if (scan(tDEFAULT, tSEQUENCE, tPROPERTY, tENDPOINT))
p_psl_declaration(parent);
else
tree_add_stmt(parent, p_psl_directive(NULL));
Expand Down Expand Up @@ -12852,7 +12853,8 @@ static psl_node_t p_psl_verification_directive(void)
case tCOVER:
return p_psl_cover_directive();
default:
one_of(tASSERT, tASSUME, tCOVER);
one_of(tASSERT, tASSUME, tASSUMEG, tRESTRICT, tRESTRICTG, tFAIRNESS,
tSTRONG, tCOVER);
return NULL;
}
}
Expand All @@ -12873,11 +12875,14 @@ static tree_t p_psl_directive(ident_t label)
insert_names_for_psl(nametab);

psl_node_t p = p_psl_verification_directive();
tree_set_psl(t, p);

scan_as_vhdl();

psl_check(p, nametab);
if (p != NULL) {
tree_set_psl(t, p);
psl_check(p, nametab);
}

pop_scope(nametab);

tree_set_loc(t, CURRENT_LOC);
Expand Down Expand Up @@ -12982,6 +12987,47 @@ static tree_t p_psl_sequence_declaration(void)
return t;
}

static tree_t p_psl_endpoint_declaration(void)
{
// sequence PSL_Identifier is Sequence ;

BEGIN("PSL endpoint declaration");

scan_as_psl();

psl_node_t decl = psl_new(P_ENDPOINT_DECL);

consume(tENDPOINT);

ident_t ident = p_identifier();
psl_set_ident(decl, ident);

tree_t t = tree_new(T_PSL);
tree_set_psl(t, decl);
tree_set_ident(t, ident);
insert_name(nametab, t, NULL);

push_scope(nametab);
insert_names_for_psl(nametab);

consume(tIS);

psl_node_t prop = p_psl_sequence();
psl_set_value(decl, prop);

consume(tSEMI);

psl_set_loc(decl, CURRENT_LOC);
psl_check(decl, nametab);

pop_scope(nametab);

scan_as_vhdl();

tree_set_loc(t, CURRENT_LOC);
return t;
}

static void p_psl_declaration(tree_t parent)
{
// Property_Declaration | Sequence_Declaration | Clock_Declaration
Expand All @@ -12998,8 +13044,11 @@ static void p_psl_declaration(tree_t parent)
case tDEFAULT:
tree_add_decl(parent, p_psl_clock_declaration());
break;
case tENDPOINT:
tree_add_decl(parent, p_psl_endpoint_declaration());
break;
default:
one_of(tPROPERTY, tSEQUENCE, tDEFAULT);
one_of(tPROPERTY, tSEQUENCE, tDEFAULT, tENDPOINT);
break;
}
}
Expand Down
5 changes: 4 additions & 1 deletion src/psl/psl-node.c
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,9 @@ static const imask_t has_map[P_LAST_PSL_KIND] = {

// P_CLOCKED
(I_FOREIGN | I_VALUE | I_REF),

// P_ENDPOINT_DECL
(I_IDENT | I_VALUE),
};

static const char *kind_text_map[P_LAST_PSL_KIND] = {
Expand All @@ -127,7 +130,7 @@ static const char *kind_text_map[P_LAST_PSL_KIND] = {
"P_SERE", "P_REPEAT", "P_PROPERTY_INST", "P_SEQUENCE_INST", "P_UNION",
"P_BUILTIN_FUNC", "P_VALUE_SET", "P_PARAM_DECL", "P_UNTIL", "P_ABORT",
"P_BEFORE", "P_SUFFIX_IMPL", "P_LOGICAL", "P_RANGE", "P_PROC_BLOCK",
"P_PARAM_SERE", "P_CLOCKED",
"P_PARAM_SERE", "P_CLOCKED", "P_ENDPOINT_DECL",
};

static const change_allowed_t change_allowed[] = {
Expand Down
1 change: 1 addition & 0 deletions src/psl/psl-node.h
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ typedef enum {
P_PROC_BLOCK,
P_PARAM_SERE,
P_CLOCKED,
P_ENDPOINT_DECL,

P_LAST_PSL_KIND
} psl_kind_t;
Expand Down
11 changes: 11 additions & 0 deletions src/psl/psl-sem.c
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,14 @@ static void psl_check_sequence_decl(psl_node_t p, nametab_t *tab)
psl_check(psl_value(p), tab);
}

static void psl_check_endpoint_decl(psl_node_t p, nametab_t *tab)
{
psl_check(psl_value(p), tab);

error_at(psl_loc(p), "PSL endpoint declarations are not supported as they "
"were not part of IEEE Std 1850-2010 or later standards");
}

static void psl_check_top_level(psl_node_t p, nametab_t *tab)
{
if (psl_kind(p) == P_CLOCKED)
Expand Down Expand Up @@ -439,6 +447,9 @@ void psl_check(psl_node_t p, nametab_t *tab)
case P_SEQUENCE_DECL:
psl_check_sequence_decl(p, tab);
break;
case P_ENDPOINT_DECL:
psl_check_endpoint_decl(p, tab);
break;
case P_HDL_EXPR:
psl_check_hdl_expr(p, tab);
break;
Expand Down
2 changes: 1 addition & 1 deletion src/scan.c
Original file line number Diff line number Diff line change
Expand Up @@ -248,7 +248,7 @@ const char *token_str(token_t tok)
"shortint", "longint", "int", "integer", "time", "typedef", "logic",
"enum", "tagged", "abort", "sync_abort", "async_abort", "before",
"before!", "before_", "before!_", "|->", "|=>", "next", "inf",
"repeat", "do",
"repeat", "do", "endpoint",
};

if (tok >= 200 && tok - 200 < ARRAY_LEN(token_strs))
Expand Down
1 change: 1 addition & 0 deletions src/scan.h
Original file line number Diff line number Diff line change
Expand Up @@ -406,5 +406,6 @@ bool is_scanned_as_psl(void);
#define tINF 506
#define tREPEAT 507
#define tDO 508
#define tENDPOINT 509

#endif // _SCAN_H
3 changes: 3 additions & 0 deletions test/psl/parse4.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -55,4 +55,7 @@ begin
-- Paramterized SERE
-- psl cover {for i in {1 to 3}: && {seq_b(i)}};

-- Garbage after PSL directive
-- psl asfasfa;

end architecture;
1 change: 1 addition & 0 deletions test/psl/sem1.vhd
Original file line number Diff line number Diff line change
Expand Up @@ -38,5 +38,6 @@ begin
-- psl assert {x[*]}[->1]; -- Error
-- psl assert {x[*1 to clk]}; -- Error
-- psl assert {z [[foo <= 1;]]}; -- Error
-- psl endpoint e1 is {x; y}; -- Not supported

end architecture;
2 changes: 2 additions & 0 deletions test/test_psl.c
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,7 @@ START_TEST(test_sem1)
{ 39, "expression must be a PSL Number but have type BIT" },
{ 40, "no visible declaration for FOO" },
{ 40, "no visible declaration for Z" },
{ 41, "PSL endpoint declarations are not supported" },
{ -1, NULL }
};
expect_errors(expect);
Expand Down Expand Up @@ -184,6 +185,7 @@ START_TEST(test_parse4)

const error_t expect[] = {
{ 53, "FOO is not a PSL sequence" },
{ 59, "unexpected ; while parsing architecture statement part" },
{ -1, NULL }
};
expect_errors(expect);
Expand Down

0 comments on commit 3fa98e3

Please sign in to comment.