source: repy_checkapi/CheckAPI/check_api_oracle_setter_getter.repy

Last change on this file was 33, checked in by jerome, 5 years ago

Initial commit of repy CheckAPI

  • Property svn:executable set to *
File size: 8.2 KB
Line 
1'''
2<Program Name>
3  check_api_oracle_setter_getter.repy
4
5<Started>
6  This version was started on Apr 11, 2011, however it has been an ongoing
7  project since Autumn 2010.
8
9<Author>
10  jeffra45@.cs.washington.edu
11  Jeff Rasley
12
13<Purpose>
14  The CheckAPI Oracle is used to set/get and verify observed behavior or the
15  Repy V2 implementation, this is used with systolic verification.
16'''
17
18# Used to designate a non-value, since None is a proper return value.
19class Null(object):
20  pass
21
22
23# Stores a return value and an error.
24mycontext['setter_getter_value'] = (Null, Null)
25
26
27
28
29def convert_error(err):
30  """
31  <Purpose>
32    Convert an exception object into a string representation of its type.
33  <Argument>
34    err
35      An exception instance itself.
36  <Return>
37    A String representation of an exception.
38  """
39  if err != None:
40    return str(type(err)).split('.')[1][:-2]
41
42
43 
44
45def regex_cond_range(min, max, wrap=True):
46  # "<RANGE 0, 10>, matches numerical ranges [0, 10] inclusive."
47  return _wrap_regex("<RANGE " + str(min) + ", " + str(max) + ">", wrap)
48
49
50
51
52def regex_cond_ip(wrap=True):
53  return _wrap_regex("<IP>", wrap)
54
55
56
57
58def regex_cond_obj(wrap=True):
59  return _wrap_regex("<OBJ>", wrap)
60
61
62
63
64def _wrap_regex(substring, wrap=True):
65  if wrap:
66    return "^" + substring + "$"
67  else:
68    return substring
69
70
71
72
73def regex_cond_triple(one, two, three, wrap=True):
74  # "^<TUPLE (one:two:three)>$", where one/two/tree are regexes all separated
75  # by a ':' character and each one could be a 'special' regex. This triple
76  # function could easily be converted to handle N-tuples but for Repy it
77  # is not needed.
78  return _wrap_regex("<TUPLE (" + one + ":" + two + ":" + three + ")>", wrap)
79
80
81
82
83def assert_value_okay(cond_regex, value):
84  # Attempt to find upper and lower bounds for 'special' regex that is wrapped
85  # inside of < >.
86  lower, upper = cond_regex.find("<"), cond_regex.rfind(">")
87  if lower != -1 and upper != -1:
88    special_regex = cond_regex[lower+1:upper]
89    leftover_regex = cond_regex[:lower] + cond_regex[upper+1:]
90  else:
91    # No 'special' regex found.
92    special_regex = ""
93    leftover_regex = cond_regex
94 
95  # Begin to try and determine what 'special' regex was used.
96  if special_regex.startswith("RANGE"):
97    range_min, range_max = special_regex.strip("RANGE").split(",")
98    if value < int(range_min) or value > int(range_max):
99      error_str = "Value: " + str(value) + ", does not match regex: " + cond_regex
100      raise ModelConformanceFailure(error_str)
101 
102  elif special_regex.startswith("IP"):
103    if not validate_ip(value):
104      error_str = "IP address: " + str(value) + ", is not a valid address."
105      raise ModelConformanceFailure(error_str)
106   
107  elif special_regex.startswith("OBJ"):
108    # Not sure what to do with an object here...
109    if not isinstance(value, str): #is_model_object(value):
110      error_str = "The object returned by the implementation was not an object. " + str(type(value))
111      raise ModelConformanceFailure(error_str)
112     
113  elif special_regex.startswith("TUPLE"):
114    # Unpack each element in the tuple and validate each part individually.
115    plower, pupper = special_regex.find("(")+1, special_regex.rfind(")")
116    inner_regexes = special_regex[plower:pupper].split(":")
117   
118    assert(isinstance(value, tuple))
119    assert(len(value) == len(inner_regexes))
120   
121    # Verify all of the inner values using this same function.
122    i = 0
123    for cond in inner_regexes:
124      assert_value_okay(cond, value[i])
125      i += 1
126     
127     
128  elif special_regex == "":
129    if leftover_regex == "None":
130      if value != None:
131        raise ModelConformanceFailure("Thread did not return proper value of None.")
132    else:
133      # This is the case where there was no special regex and we would use the
134      # Repy regex module if it existed to match our value. For now we will only
135      # support the {min,max} length matcher since that is all we need.
136      leftb, rightb = leftover_regex.find("{"), leftover_regex.rfind("}")
137      minlen, maxlen = leftover_regex[leftb+1:rightb].split(",")
138      if len(value) > int(maxlen) or len(value) < int(minlen):
139        error_str = "The length of the value returned by the implementation is "
140        error_str += "not between " + str(minlen) + "-" + str(maxlen) + ", it is "
141        error_str += str(len(value)) + "."
142        raise ModelConformanceFailure(error_str)
143         
144         
145  else:
146    # No idea what kind of regex this is, raise an error!
147    error_str = "The condition regex value in setter/getter did not match"
148    error_str += " anything it knows about, there is a problem."
149    raise InternalCheckAPIError(error_str)
150   
151
152
153
154def oracle_getter(cond_regex, error_list):
155  """
156  <Purpose>
157    Verifies and returns the current value in the setter/getter.
158   
159  <Arguments>
160    cond_regex
161      A regex-line string that expresses a condition for the implementations
162      return value.
163    error_list
164      A list of non-deterministic errors that could have occurred for this call.
165 
166  <Exceptions>
167    ModelConformanceFailure
168      If the value in the setter/getter does not match the regex condition and
169      is not in the error list.
170       
171  <Returns>
172    The current tuple value/error from the setter/getter.
173  """
174 
175  value, error = mycontext['setter_getter_value']
176  mycontext['setter_getter_value'] = (Null, Null)
177 
178  # Error raised by the implementation, and no return value.
179  if error != None and value == None:
180    # Check to see if error is in the ND errors if okay, raise it, if not raise conformance error.
181    if type(error) not in map(type, error_list):
182      error_str = "Impl raised the error: " + convert_error(error)
183      error_str += ", this does not match any of the known acceptable errors."
184      raise ModelConformanceFailure(error_str)
185    else:
186      # The error is acceptable to raise, return it.
187      return (None, error)
188 
189  # Error raised by implementation and a return value, shouldn't happen.
190  elif error != None and value != None:
191    error_str = "Oracle getter should not return both a value and error."
192    raise InternalCheckAPIError(error_str)
193
194  # No error seen, but has a return value.
195  elif error == None and value != None:
196    if cond_regex is not None:
197      assert_value_okay(cond_regex, value)
198     
199    # If we don't have a regex, we can ignore it.
200    return (value, None)
201   
202  # If there was no error and no return value, ignore.
203  elif error == None and value == None:
204    return (value, error)
205 
206  # If the setter was set to anything but the above conditions, such as Null,
207  # we didn't properly set values. Raise an internal error.
208  else:
209    error_str = "Oracle getter should not return (Null, Null), it was."
210    raise InternalCheckAPIError(error_str)
211
212
213
214
215def oracle_setter(value, error=None):
216  """
217  <Purpose>
218    Stores a value in the setter/getter for later use.
219 
220  <Argument>
221    value
222      The given value that is going to be stored in the setter/getter.
223  """
224  mycontext['setter_getter_value'] = (value, error)
225 
226 
227 
228 
229def validate_ip(ipaddr):
230  """
231  <Purpose>
232    Determines if ipaddr is a valid IP address.
233    0.X and 224-255.X addresses are not allowed.
234
235  <Arguments>
236    ipaddr: String to check for validity. (It will check that this is a string).
237
238  <Returns>
239    True if a valid IP, False otherwise.
240  """
241  # Argument must be of the string type
242  if not type(ipaddr) == str:
243    return False
244
245  # A valid IP should have 4 segments, explode on the period
246  octets = ipaddr.split(".")
247
248  # Check that we have 4 parts
249  if len(octets) != 4:
250    return False
251
252  # Check that each segment is a number between 0 and 255 inclusively.
253  for octet in octets:
254    # Attempt to convert to an integer
255    try:
256      ipnumber = int(octet)
257    except ValueError:
258      # There was an error converting to an integer, not an IP
259      return False
260
261    # IP addresses octets must be between 0 and 255
262    if not (ipnumber >= 0 and ipnumber <= 255):
263      return False
264
265  # should not have a ValueError (I already checked)
266  firstipnumber = int(octets[0])
267
268  # IP addresses with the first octet 0 refer to all local IPs.   These are
269  # not allowed
270  if firstipnumber == 0:
271    return False
272
273  # IP addresses with the first octet >=224 are either Multicast or reserved.
274  # These are not allowed
275  if firstipnumber >= 224:
276    return False
277
278  # At this point, assume the IP is valid
279  return True
Note: See TracBrowser for help on using the repository browser.