@@ -211,7 +211,7 @@ private module HashCons {
211211
212212  private  newtype  HC_Params  = 
213213    HC_NoParams ( )  or 
214-     HC_ParamCons ( HashConsExpr   hc ,   int  i ,  HC_Params  list )  {  mk_ParamCons ( hc ,  i ,  list ,  _)  } 
214+     HC_ParamCons ( Type   t ,   string   name ,   int  i ,  HC_Params  list )  {  mk_ParamCons ( t ,   name ,  i ,  list ,  _)  } 
215215
216216  /** 
217217   * HashConsExpr is the hash-cons of an expression. The relationship between `Expr` 
@@ -624,11 +624,21 @@ private module HashCons {
624624    strictcount ( access .getTarget ( ) )  =  1 
625625  } 
626626
627+   /** 
628+    * Gets the name of a variable. 
629+    * 
630+    * Extracted for performance reasons, to avoid magic, which was causing performance issues in getParameter(int i). 
631+    */ 
632+   pragma [ nomagic] 
633+   private  string  getVariableName ( Variable  v )  {  result  =  v .getName ( )  } 
634+ 
627635  /* Note: This changed from the original HashCons module to be able to find structural equivalent expression. */ 
628636  private  predicate  mk_Variable ( Type  t ,  string  name ,  VariableAccess  access )  { 
629637    analyzableVariable ( access )  and 
630638    exists ( Variable  v  | 
631-       v  =  access .getTarget ( )  and  t  =  v .getUnspecifiedType ( )  and  name  =  v .getName ( ) 
639+       v  =  access .getTarget ( )  and 
640+       t  =  v .getUnspecifiedType ( )  and 
641+       name  =  getVariableName ( v ) 
632642    ) 
633643  } 
634644
@@ -1104,7 +1114,14 @@ private module HashCons {
11041114    nee .getExpr ( ) .getFullyConverted ( )  =  child .getAnExpr ( ) 
11051115  } 
11061116
1107-   private  predicate  mk_StmtCons ( HashConsStmt  hc ,  int  i ,  HC_Stmts  list ,  BlockStmt  block )  { 
1117+   private  class  LambdaBlockStmt  extends  BlockStmt  { 
1118+     LambdaBlockStmt ( )  { 
1119+       // Restricting to statements inside a lambda expressions. 
1120+       this .getParentScope * ( )  =  any ( LambdaExpression  le ) .getLambdaFunction ( ) 
1121+     } 
1122+   } 
1123+ 
1124+   private  predicate  mk_StmtCons ( HashConsStmt  hc ,  int  i ,  HC_Stmts  list ,  LambdaBlockStmt  block )  { 
11081125    hc  =  hashConsStmt ( block .getStmt ( i ) )  and 
11091126    ( 
11101127      exists ( HashConsStmt  head ,  HC_Stmts  tail  | 
@@ -1118,13 +1135,13 @@ private module HashCons {
11181135  } 
11191136
11201137  private  predicate  mk_StmtConsInner ( 
1121-     HashConsStmt  head ,  HC_Stmts  tail ,  int  i ,  HC_Stmts  list ,  BlockStmt  block 
1138+     HashConsStmt  head ,  HC_Stmts  tail ,  int  i ,  HC_Stmts  list ,  LambdaBlockStmt  block 
11221139  )  { 
11231140    list  =  HC_StmtCons ( head ,  i ,  tail )  and 
11241141    mk_StmtCons ( head ,  i ,  tail ,  block ) 
11251142  } 
11261143
1127-   private  predicate  mk_BlockStmtCons ( HC_Stmts  hc ,  BlockStmt  s )  { 
1144+   private  predicate  mk_BlockStmtCons ( HC_Stmts  hc ,  LambdaBlockStmt  s )  { 
11281145    if  s .getNumStmt ( )  >  0 
11291146    then 
11301147      exists ( HashConsStmt  head ,  HC_Stmts  tail  | 
@@ -1275,24 +1292,25 @@ private module HashCons {
12751292    mk_DeclConsInner ( _,  _,  s .getNumDeclarations ( )  -  1 ,  hc ,  s ) 
12761293  } 
12771294
1278-   private  predicate  mk_ParamCons ( HashConsExpr  hc ,  int  i ,  HC_Params  list ,  Function  f )  { 
1279-     hc  =  hashConsExpr ( f .getParameter ( i ) .getAnAccess ( ) )  and 
1280-     ( 
1281-       exists ( HashConsExpr  head ,  HC_Params  tail  | 
1282-         mk_ParamConsInner ( head ,  tail ,  i  -  1 ,  list ,  f )  and 
1283-         i  >  0 
1284-       ) 
1295+   private  predicate  mk_ParamCons ( Type  t ,  string  name ,  int  i ,  HC_Params  list ,  Function  f )  { 
1296+     exists ( Parameter  p  | 
1297+       p  =  f .getParameter ( i )  and 
1298+       t  =  p .getType ( )  and 
1299+       name  =  p .getName ( ) 
1300+     | 
1301+       mk_ParamConsInner ( _,  _,  _,  i  -  1 ,  list ,  f )  and 
1302+       i  >  0 
12851303      or 
12861304      i  =  0  and 
12871305      list  =  HC_NoParams ( ) 
12881306    ) 
12891307  } 
12901308
12911309  private  predicate  mk_ParamConsInner ( 
1292-     HashConsExpr   head ,  HC_Params  tail ,  int  i ,  HC_Params  list ,  Function  f 
1310+     Type   t ,   string   name ,  HC_Params  tail ,  int  i ,  HC_Params  list ,  Function  f 
12931311  )  { 
1294-     list  =  HC_ParamCons ( head ,  i ,  tail )  and 
1295-     mk_ParamCons ( head ,  i ,  tail ,  f ) 
1312+     list  =  HC_ParamCons ( t ,   name ,  i ,  tail )  and 
1313+     mk_ParamCons ( t ,   name ,  i ,  tail ,  f ) 
12961314  } 
12971315
12981316  private  predicate  mk_FunctionCons ( 
@@ -1302,7 +1320,7 @@ private module HashCons {
13021320    name  =  f .getName ( )  and 
13031321    body  =  hashConsStmt ( f .getBlock ( ) )  and 
13041322    if  f .getNumberOfParameters ( )  >  0 
1305-     then  mk_ParamConsInner ( _,  _,  f .getNumberOfParameters ( )  -  1 ,  params ,  f ) 
1323+     then  mk_ParamConsInner ( _,  _,  _ ,   f .getNumberOfParameters ( )  -  1 ,  params ,  f ) 
13061324    else  params  =  HC_NoParams ( ) 
13071325  } 
13081326
@@ -1486,8 +1504,6 @@ private module HashCons {
14861504
14871505  cached 
14881506  HashConsStmt  hashConsStmt ( Stmt  s )  { 
1489-     // Restricting to statements inside a lambda expressions. 
1490-     s .getParentScope * ( )  =  any ( LambdaExpression  le ) .getLambdaFunction ( )  and 
14911507    exists ( HC_Stmts  list  | 
14921508      mk_BlockStmtCons ( list ,  s )  and 
14931509      result  =  HC_BlockStmt ( list ) 
0 commit comments