Skip to content

Commit dfe5c87

Browse files
petr-bauchpetr-bauch
authored
Merge pull request #91 from xbauch/feature/range_check
Range check via Cprover assert
2 parents 69460e6 + f442210 commit dfe5c87

File tree

9 files changed

+447
-77
lines changed

9 files changed

+447
-77
lines changed

‎gnat2goto/driver/goto_utils.adb

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ with Namet; use Namet;
22
with Nlists; use Nlists;
33
with Aspects; use Aspects;
44

5+
with Ada.Text_IO; use Ada.Text_IO;
6+
57
package body GOTO_Utils is
68

79
---------------------
@@ -92,6 +94,100 @@ package body GOTO_Utils is
9294
return Ret;
9395
end Symbol_Expr;
9496

97+
--------------------------------
98+
-- New_Parameter_Symbol_Entry --
99+
--------------------------------
100+
101+
procedure New_Parameter_Symbol_Entry (Name_Id : Symbol_Id;
102+
BaseName : String;
103+
Symbol_Type : Irep;
104+
A_Symbol_Table : in out Symbol_Table)
105+
is
106+
New_Symbol : Symbol;
107+
begin
108+
New_Symbol.SymType := Symbol_Type;
109+
New_Symbol.Name := Name_Id;
110+
New_Symbol.PrettyName := Intern (BaseName);
111+
New_Symbol.BaseName := Intern (BaseName);
112+
New_Symbol.Mode := Intern ("C");
113+
114+
-- Setting it as a parameter
115+
New_Symbol.IsParameter := True;
116+
New_Symbol.IsLValue := True;
117+
New_Symbol.IsFileLocal := True;
118+
New_Symbol.IsThreadLocal := True;
119+
120+
if A_Symbol_Table.Contains (Key => Name_Id) then
121+
Put_Line (Standard_Error,
122+
"----------At: New_Parameter_Symbol_Entry----------");
123+
Put_Line (Standard_Error,
124+
"----------Trying to create known symbol.----------");
125+
Put_Line (Standard_Error, "----------" & BaseName & "----------");
126+
else
127+
A_Symbol_Table.Insert (Name_Id, New_Symbol);
128+
end if;
129+
end New_Parameter_Symbol_Entry;
130+
131+
-------------------------------
132+
-- New_Function_Symbol_Entry --
133+
-------------------------------
134+
135+
function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
136+
Value : Irep;
137+
A_Symbol_Table : in out Symbol_Table)
138+
return Symbol is
139+
New_Symbol : Symbol;
140+
begin
141+
New_Symbol.SymType := Symbol_Type;
142+
New_Symbol.Name := Intern (Name);
143+
New_Symbol.PrettyName := New_Symbol.Name;
144+
New_Symbol.BaseName := New_Symbol.Name;
145+
New_Symbol.Mode := Intern ("C");
146+
New_Symbol.Value := Value;
147+
148+
if A_Symbol_Table.Contains (Key => Intern (Name)) then
149+
Put_Line (Standard_Error,
150+
"----------At: New_Function_Symbol_Entry----------");
151+
Put_Line (Standard_Error,
152+
"----------Trying to create known symbol.----------");
153+
Put_Line (Standard_Error, "----------" & Name & "----------");
154+
else
155+
A_Symbol_Table.Insert (Intern (Name), New_Symbol);
156+
end if;
157+
return New_Symbol;
158+
end New_Function_Symbol_Entry;
159+
160+
--------------------------
161+
-- Create_Fun_Parameter --
162+
--------------------------
163+
164+
-- To be called when one needs to build a function inside gnat2goto
165+
-- Modifies symbol table and Param_List as a side effect
166+
-- Returns irep of type I_Code_Parameter
167+
function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
168+
Param_Type : Irep; Param_List : Irep;
169+
A_Symbol_Table : in out Symbol_Table;
170+
Source_Location : Source_Ptr := No_Location)
171+
return Irep is
172+
Func_Param_Id : constant Symbol_Id := Intern (Fun_Name & Param_Name);
173+
-- Create an irep for the parameter
174+
Value_Arg : constant Irep :=
175+
Make_Code_Parameter (Source_Location => Source_Location,
176+
Default_Value => Ireps.Empty,
177+
I_Type => Param_Type,
178+
Base_Name => Param_Name,
179+
This => False,
180+
Identifier => Unintern (Func_Param_Id));
181+
begin
182+
-- Creates a symbol for the parameter
183+
New_Parameter_Symbol_Entry (Name_Id => Func_Param_Id,
184+
BaseName => Param_Name,
185+
Symbol_Type => Param_Type,
186+
A_Symbol_Table => A_Symbol_Table);
187+
Append_Parameter (Param_List, Value_Arg);
188+
return Value_Arg;
189+
end Create_Fun_Parameter;
190+
95191
---------------------
96192
-- Name_Has_Prefix --
97193
---------------------

‎gnat2goto/driver/goto_utils.ads

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,25 @@ package GOTO_Utils is
2929
function Symbol_Expr (Sym : Symbol) return Irep
3030
with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;
3131

32+
procedure New_Parameter_Symbol_Entry (Name_Id : Symbol_Id;
33+
BaseName : String;
34+
Symbol_Type : Irep;
35+
A_Symbol_Table : in out Symbol_Table);
36+
37+
function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
38+
Value : Irep;
39+
A_Symbol_Table : in out Symbol_Table)
40+
return Symbol;
41+
42+
function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;
43+
Param_Type : Irep; Param_List : Irep;
44+
A_Symbol_Table : in out Symbol_Table;
45+
Source_Location : Source_Ptr := No_Location)
46+
return Irep
47+
with Pre => (Kind (Param_Type) in Class_Type
48+
and then Kind (Param_List) = I_Parameter_List),
49+
Post => Kind (Create_Fun_Parameter'Result) = I_Code_Parameter;
50+
3251
function Name_Has_Prefix (N : Node_Id; Prefix : String) return Boolean;
3352

3453
function Has_GNAT2goto_Annotation

‎gnat2goto/driver/range_check.adb

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
with Binary_To_Hex; use Binary_To_Hex;
2+
3+
package body Range_Check is
4+
5+
-----------------
6+
-- Store_Bound --
7+
-----------------
8+
9+
function Store_Bound (Number : Bound_Type) return Integer
10+
is
11+
Length : constant Integer := Integer (Integer_Bounds_Table.Length);
12+
begin
13+
Integer_Bounds_Table.Append (Number);
14+
return Length;
15+
end Store_Bound;
16+
17+
-----------------------
18+
-- Load_Bound_In_Hex --
19+
-----------------------
20+
21+
function Load_Bound_In_Hex (Index : Integer; Bit_Width : Pos) return String
22+
is
23+
Bound : constant Uint := Uint (Integer_Bounds_Table.Element (Index));
24+
begin
25+
return Convert_Uint_To_Hex (
26+
Value => Bound,
27+
Bit_Width => Bit_Width);
28+
end Load_Bound_In_Hex;
29+
30+
end Range_Check;

‎gnat2goto/driver/range_check.ads

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
with Uintp; use Uintp;
2+
with Types; use Types;
3+
4+
with Ada.Containers.Vectors; use Ada.Containers;
5+
package Range_Check is
6+
7+
type Bound_Type is new Uint;
8+
9+
package Integer_Bounds_Vector is new
10+
Ada.Containers.Vectors (Index_Type => Natural,
11+
Element_Type => Bound_Type);
12+
13+
function Store_Bound (Number : Bound_Type) return Integer;
14+
15+
Integer_Bounds_Table : Integer_Bounds_Vector.Vector;
16+
17+
function Load_Bound_In_Hex (Index : Integer; Bit_Width : Pos) return String
18+
with Pre => Integer (Integer_Bounds_Table.Length) >= Index;
19+
20+
end Range_Check;

0 commit comments

Comments
 (0)