#---------------------------------------------------------------------------*
#
#  @file semantic_verification.galgas
#
#  @section desc File description
#
#  Semantics verification of OIL abtract syntax.
#
#  @section copyright Copyright
#
#  Goil OIL compiler, part of Trampoline RTOS
#
#  Trampoline is copyright (c) CNRS, University of Nantes,
#  Ecole Centrale de Nantes
#  Trampoline is protected by the French intellectual property law.
#
#  This software is distributed under the GNU Public Licence V2.
#  Check the LICENSE file in the root directory of Trampoline
#
#  $Date$
#  $Rev$
#  $Author$
#  $URL$
#
#---------------------------------------------------------------------------*



#---------------------------------------------------------------------------*
# Check all objects attributes are defines
#
method @implementation verifyApplication
  ?let @applicationDefinition appDef {
  for () imp_ in  imp do
    if [[appDef objects] hasKey ![imp_lkey string]] then
      let @objectKind obj
      [[appDef objects] get !imp_lkey ?obj]
      [imp_obj verifyApplication !obj]
    end
  end
}

#---------------------------------------------------------------------------*
method @implementationObject verifyApplication
  ?let @objectKind objectsOfKind {
  for () obj_ in  [objectsOfKind objects] do
    for () in  attributes do
      [type verifyApplication !obj_attributes]
    end
  end
}

#---------------------------------------------------------------------------*
method @impType verifyApplication
  ?let @objectAttributes attrs {
  for () in  [attrs objectParams] do
    if [lkey string] == [name string] then
      [self verifyMultipleType !value]
    end
  end
}

#---------------------------------------------------------------------------*
method @impType verifyType
  ?let @object_t attr {
  error [attr location]: "Internal error, a generic type should not be instantiated"
}

#---------------------------------------------------------------------------*
method @impType verifyMultipleType
  ?let @object_t attr {
  cast attr
  case == @multipleAttribute ma :
    for () in  [ma items] do
      [self verifyType !item]
    end
  else
    [self verifyType !attr]
  end
}

#---------------------------------------------------------------------------*
override method @impStructType verifyType
  ?let @object_t attr {
  cast attr
  case == @structAttribute sa :
    for () in  structAttributes do
      if [[[sa subAttributes] objectParams] hasKey ![lkey string]] then
        let @object_t subAttr
        [[[sa subAttributes] objectParams] get !lkey ?subAttr]
        [type verifyMultipleType !subAttr]
      end
    end
  else
    error [attr location] : "STRUCT expected"
  end
}

#---------------------------------------------------------------------------*
override method @refType verifyType
  ?let @object_t attr {
  cast attr
  case == @objectRefAttribute :
  else 
    error [attr location] : "object reference expected"
  end
}

#---------------------------------------------------------------------------*
override method @impBoolType verifyType
  ?let @object_t attr {
  cast attr
  case == @boolAttribute b :
    if [b value] then
      for () in  trueSubAttributes do
        if [[[b subAttributes] objectParams] hasKey ![lkey string]] then
          let @object_t subAttrs
          [[[b subAttributes] objectParams] get !lkey ?subAttrs]
          [type verifyMultipleType !subAttrs]
        end
      end
    else
      for () in  falseSubAttributes do
        if [[[b subAttributes] objectParams] hasKey ![lkey string]] then
          let @object_t subAttrs
          [[[b subAttributes] objectParams] get !lkey ?subAttrs]
          [type verifyMultipleType !subAttrs]
        end
      end
    end
  else 
    error [attr location] : "BOOLEAN expected"
  end
}

#---------------------------------------------------------------------------*
override method @impEnumType verifyType
  ?let @object_t attr {
  cast attr
  case == @enumAttribute e :
    if [valuesMap hasKey ![e value]] then
      let @implementationObjectMap validVal
      [valuesMap get !lstringWith(![e value]) ?validVal]
      for () in  validVal do
        if [[[e subAttributes] objectParams] hasKey ![lkey string]] then
          let @object_t subAttrs
          [[[e subAttributes] objectParams] get !lkey ?subAttrs]
          [type verifyMultipleType !subAttrs]
        end
      end
    else
      error [e location] : [e value]+" is not a valid enum value"
    end
  case == @auto :
  else 
    message "**** @impEnumType ****\n"
    error [attr location] : "ENUM expected"
  end
}

#---------------------------------------------------------------------------*
# may be a _TYPE or a STRING 
override method @impAutoDefaultType verifyType
  ?let @object_t attr {
  cast attr
  case == @stringAttribute :
    if type != @dataType. string & type != @dataType. identifier then
      error [attr location] : "string of identifier expected"
    end 
  case == @string_class :
    if type != @dataType. identifier then
      error [attr location] : [type oilType]+" expected"
    end
  case == @auto :
  else 
    message "*** @impAutoDefaultType ***\n"
    log attr
    error [attr location] : [type oilType]+" expected"
  end
}

#---------------------------------------------------------------------------*
# may be a UINT32, INT32, UINT64, INT64 or FLOAT 
override method @impRangedType verifyType
  ?let @object_t attr {
  cast attr
  case == @uint32_class :
    if type != @dataType. uint32Number then
      error [attr location] : [type oilType]+" expected"
    end
  case == @sint32_class :
    if type != @dataType. sint32Number then
      error [attr location] : [type oilType]+" expected"
    end
  case == @uint64_class :
    if type != @dataType. uint64Number then
      error [attr location] : [type oilType]+" expected"
    end
  case == @sint64_class :
    if type != @dataType. sint64Number then
      error [attr location] : [type oilType]+" expected"
    end
  case == @float_class :
    if type != @dataType. floatNumber then
      error [attr location] : [type oilType]+" expected"
    end
  case == @auto :
    if withAuto == false then
      error [attr location] : "AUTO is not allowed for "+name+" attribute"
    end
  else
#    message "*** @impRangedType ***\n";
    error [attr location] : [type oilType]+" expected"
  end
}

#---------------------------------------------------------------------------*

func attributeAllowsAuto
  ?let @impType  type
  ->@bool     allowsAuto {
  allowsAuto = true
  cast type
  case >= @impAutoDefaultType autoType :
    if not [autoType withAuto] then
      # It does not allow AUTO
      allowsAuto = false
    end
  else
    # It does not allow AUTO
    allowsAuto = false
  end
}

#
# Verify all attributes are defined
#
proc verifyAllAttributes
  ?let @implementation imp
  ?let @objectsMap objects {
  for () in  objects do
    let @implementationObject impObj = [imp impObject ![lkey string]]
#    message "*** implementation object = ".lkey."\n";
    for () obj_ in  [objectsOfKind objects] do
      for () imp_ in  [impObj attributes] do
        if [[obj_attributes objectParams] hasKey ![imp_lkey string]] then
          # the parameter is defined in the object
          # get it to see if it is set to AUTO
          let @object_t value
          [[obj_attributes objectParams] get !imp_lkey ?value]
          cast value
          case == @auto :
            # check the implementation definition param allows AUTO
            if not attributeAllowsAuto(!imp_type) then
              error [value location]:"AUTO value is not allowed for the "+[lkey string]+" attribute"
            end
          else end
        else
          # the parameter is not defined in the object
          if not attributeAllowsAuto(!imp_type) & not [imp_type multiple] then
            error obj_lkey:"In "+lkey+" "+obj_lkey+", attribute "+[imp_lkey string]+" is not defined and is not AUTO"
          end
        end
        cast imp_type
        case == @impAutoDefaultType :
        else end
      end
    end
  end
}
#
# Per object static verification
#

###
## @fn counters_well_formed
##
## counters_well_formed checks each counter has all the required
## attributes.
## Required attributes are:
## - MAXALLOWEDVALUE
## - TICKSPERBASE
## - MINCYCLE
##
## @param counters    the map of counters.
##
#routine counters_well_formed
#  ??@counter_map counters
#:
#  foreach counters (@lstring counter_name @counter_obj counter) do
#
#    cast [counter max_allowed_value]:
#      when == @void do 
#        error [counter_name location]: "MAXALLOWEDVALUE attribute not defined for COUNTER ".[counter_name string];
#      else
#    end cast;
#
#    cast [counter ticks_per_base]:
#      when == @void do 
#        error [counter_name location]: "TICKSPERBASE attribute not defined for COUNTER ".[counter_name string];
#      else
#    end cast;
#
#    cast [counter min_cycle]:
#      when == @void do 
#        error [counter_name location]: "MINCYCLE attribute not defined for COUNTER ".[counter_name string];
#      else
#    end cast;
#
#  end foreach;
#end routine;
#
###
## @fn alarms_well_formed
##
## alarms_well_formed checks each alarm has all the required
## attributes.
## Required attributes are:
## - COUNTER
## - ACTION
## - AUTOSTART
##
## @param alarms    the map of alarms.
##
#routine alarms_well_formed
#  ??@alarm_map alarms
#:
#  foreach alarms (@lstring alarm_name @alarm_obj alarm) do
#
#    if [[alarm counter_name] string] == "" then
#        error alarm_name: "COUNTER attribute undefined for ALARM ".[alarm_name string];
#    end if;
#
#    cast [alarm action_params]:
#      when == @void_action do
#        error alarm_name: "ACTION attribute undefined for ALARM ".[alarm_name string];
#      else
#    end cast;
#
#    cast [alarm autostart_params]:
#    when == @autostart_void do
#        error alarm_name: "AUTOSTART attribute undefined for ALARM ".[alarm_name string];
#    else end cast;
#
#  end foreach;
#end routine;
#
###
## @fn events_well_formed
##
## events_well_formed checks each event has the required
## attribute.
## Required attribute is:
## - MASK
##
## @param events    the map of events.
##
#routine events_well_formed
#  ??@event_map events
#:
#  foreach events (@lstring event_name @event_obj event) do
#
#    cast [event mask]:
#      when == @event_mask_void_obj mask do
#          error event_name: "MASK attribute undefined for EVENT ".[event_name string];
#          error [mask location]: "was previously defined here";
#      else
#    end cast;
#
#  end foreach;
#end routine;
#
#routine all_events_and_resources_and_messages_defined_and_used 
#    ??@root_obj cpu
#:
#  @task_map tasks := [cpu tasks];
#  @isr_map isrs := [cpu isrs];
#  @event_map events := [cpu events];
#  @resource_map resources := [cpu resources];
#  @message_map messages := [cpu messages];
#  @stringset used_events [emptySet];
#  @stringset used_resources [emptySet];
#  @stringset used_messages [emptySet];
#
#  #Events and resources and messages referenced in a task are defined
#  foreach tasks (@lstring task_name @task_obj task) do
#
#    #all referenced events must be defined
#    @lstringlist task_events;
#    task_events:= [task events];
#    foreach task_events (@lstring event_name) do
#      used_events += ![event_name string];
#      if (not [events hasKey ![event_name string]])
#      then error event_name: "EVENT ".[event_name string]." is not defined";
#      end if;
#    end foreach;
#
#    #all referenced resources must be defined
#    @lstringlist task_resources;
#    task_resources:= [task resources];
#    foreach task_resources (@lstring res_name) do
#      used_resources += ![res_name string];
#      if (not [resources hasKey ![res_name string]])
#      then error res_name: "RESOURCE ".[res_name string]." is not defined";
#      end if;
#    end foreach;
#
#    #all referenced messages must be defined
#    @lstringlist task_messages;
#    task_messages:= [task messages];
#    foreach task_messages (@lstring mess_name) do
#      used_messages += ![mess_name string];
#      if (not [messages hasKey ![mess_name string]]) then
#        error mess_name: "MESSAGE ".[mess_name string]." is not defined";
#      end if;
#    end foreach;
#  end foreach;
#
#  # Resources and messages referenced in an ISR are defined
#  foreach isrs (@lstring isr_name @isr_obj isr) do
#
#    #all referenced resources must be defined
#    @lstringlist isr_resources:= [isr resources];
#    foreach isr_resources (@lstring res_name) do
#      used_resources += ![res_name string];
#      if (not [resources hasKey ![res_name string]]) then
#        error isr_name: "RESOURCE ".res_name." is not defined";
#      end if;
#    end foreach;
#
#    #all referenced messages must be defined
#    @lstringlist isr_messages;
#    isr_messages:= [isr messages];
#    foreach isr_messages (@lstring mess_name) do
#      used_messages += ![mess_name string];
#      if (not [messages hasKey ![mess_name string]]) then
#        error isr_name: "MESSAGE ".mess_name." is not defined";
#      end if;
#    end foreach;
#
#  end foreach;
#
#  #all defined events should be referenced in a task
#  foreach events (@lstring event_key *) do
#    if (not [used_events hasKey ![event_key string]]) then
#      warning event_key: "EVENT ".[event_key string]." is defined but never used";
#    end if;
#  end foreach;
#
#  #all defined resources should be referenced in a task or an ISR
#  foreach resources (@lstring res_key *) do
#    if (not [used_resources hasKey ![res_key string]]) then
#      warning res_key: "RESOURCE ".[res_key string]." is defined but never used";
#    end if;
#  end foreach;
#
#  #all defined messages should be referenced in a task or an ISR
#  foreach messages (@lstring mess_key *) do
#    if (not [used_messages hasKey ![mess_key string]]) then
#      warning mess_key: "MESSAGE ".[mess_key string]." is defined but never used";
#    end if;
#  end foreach;
#    
#end routine;
#
#routine all_event_masks_different
#    ?@event_map events 
#:
#  @stringset defined_masks [emptySet];
#  foreach events (@lstring event_name @event_obj event) do
#    @event_mask_obj mask;
#    mask:= [event mask];
#    cast mask:
#      when == @event_mask_user_obj m do 
#        @string mask_in_string:= [[[m mask] uint64] string];
#        if [defined_masks hasKey !mask_in_string] then
#          warning event_name: "Mask ".mask_in_string." already used";
#        else
#          defined_masks += !mask_in_string;
#        end if;
#      else
#    end cast;
#  end foreach;
#end routine;
#
#routine all_alarm_actions_correct
#  ?@alarm_map   alarms
#  ?@task_map    tasks
#  ?@counter_map counters
#:    
#  @stringset defined_task_names;
#
#  defined_task_names:= [tasks allKeys];
#  foreach alarms (@lstring alarm_name @alarm_obj alarm_data) do
#    @action_obj alarm_action;
#    alarm_action:= [alarm_data action_params];
#    cast alarm_action:
#      when == @setevent_action act do
#        if not [defined_task_names hasKey ![[act task_name] string]] then
#          error [act task_name]: "TASK ".[[act task_name] string]." is never defined";
#        else 
#          @task_obj task_data;
#          @lstringlist known_events;
#          [tasks get ![act task_name] ?task_data];
#          known_events:= [task_data events];
#          if ([known_events length] == 0) then
#             error [act event_name]: "An alarm can't set an Event to a basic task (Task ".[[act task_name] string]." is a basic task).";         
#          end if;
#          #@bool known;
#          #is_in_lstringlist !known_events ![act event_name] ?* ?known;
#          #if not known then
#          #  error [act event_name]: "EVENT ".[[act event_name] string]." is not defined for TASK ".[[act task_name] string];
#          #end if;
#        end if;
#      when == @activatetask_action act do
#        if not [defined_task_names hasKey ![[act task_name] string]] then
#          error [act task_name]: "TASK ".[[act task_name] string]." is not defined";
#        end if;
#      when == @incrementcounter_action act do
#        if [counters hasKey ![[act counter_name] string]] then
#          @counter_obj cnt;
#          [counters getCounter ![act counter_name] ?cnt];
#          cast [cnt type]:
#            when == @software_counter do
#            else
#              error [act counter_name]: "OS285 - It is impossible to increment a hardware counter (".[[act counter_name] string]." is not a software counter).";
#          end cast;
#        else
#          error [act counter_name]: "COUNTER ".[[act counter_name] string]." is never defined";
#        end if;
#      else            
#    end cast;
#  end foreach;
#end routine;

#routine tasks_well_formed
#  ??@objectKindMap tasks
#:
#  foreach tasks do
#    
#    cast [task priority]:
#      when == @void do
#        error task_name: "PRIORITY attribute not defined for TASK ".[task_name string];
#      else
#    end cast;
#
#    cast [task activation]:
#      when == @void do
#        error task_name: "ACTIVATION attribute not defined for TASK ".[task_name string];
#      when == @uint32_class ui do
#        @lstringlist defined_events:= [task events];
#        if ( [defined_events length] > 0 & [ui value] > 1) then
#          error task_name: "ACTIVATION attribute for extended task ".[task_name string]." should be set to 1";
#          error [ui location]: "ACTIVATION attribute set to ".[[ui value] string]." here";
#        end if;
#      else
#        error here: "Internal error, wrong datatype for ACTIVATION in task ".[task_name string];
#    end cast;
#
#    if [[task schedule] string] == "" then
#      error task_name: "SCHEDULE attribute not defined for TASK ".[task_name string];
#    end if;
#
#    cast [task autostart]:
#      when == @task_autostart_void do
#        error task_name: "AUTOSTART attribute not defined for TASK ".[task_name string];
#      else
#    end cast;
#
#  end foreach;
#end routine;

##
# verifyCrossReferences verifies each object referenced by another object exists
#
method @objectsMap verifyCrossReferences
  ?let @implementation imp
{
  for () in self do
    [[imp imp] get !lkey ?let @implementationObject obj];
    [objectsOfKind verifyCrossReferences !self !obj]
  end
}

method @objectKind verifyCrossReferences
  ?let @objectsMap     allObjects
  ?let @implementationObject obj
{
  for () in objects do
   [attributes verifyCrossReferences !allObjects ![obj attributes]]
  end
}

method @objectAttributes verifyCrossReferences
  ?let @objectsMap allObjects
  ?let @implementationObjectMap attributes
{
  for () in objectParams do
    if [attributes hasKey ![lkey string]] then
      [attributes get !lkey ?let @impType type];
      [value verifyCrossReferences !allObjects !type]
    end
  end
}

method @object_t verifyCrossReferences
  ?let @objectsMap unused allObjects
  ?let @impType unused type
{
}

override method @multipleAttribute verifyCrossReferences
  ?let @objectsMap  allObjects
  ?let @impType  type
{
  for () in items do
    [item verifyCrossReferences !allObjects !type]
  end
}

override method @boolAttribute verifyCrossReferences
  ?let @objectsMap  allObjects
  ?let @impType  type
{
  let @impBoolType boolType = type as @impBoolType
  if value then
    [subAttributes verifyCrossReferences !allObjects ![boolType trueSubAttributes]]
  else
    [subAttributes verifyCrossReferences !allObjects ![boolType falseSubAttributes]]
  end
}

override method @enumAttribute verifyCrossReferences
  ?let @objectsMap  allObjects
  ?let @impType  type
{
  let @impEnumType enumType = type as @impEnumType
  let @lstring key = @lstring.new {!value !.here}
  [[enumType valuesMap] get !key ?let @implementationObjectMap expectedAttributes]
  [subAttributes verifyCrossReferences !allObjects !expectedAttributes]
}

override method @structAttribute verifyCrossReferences
  ?let @objectsMap  allObjects
  ?let @impType  type
{
  let @impStructType structType = type as @impStructType
  [subAttributes verifyCrossReferences !allObjects ![structType structAttributes]]
}

override method @objectRefAttribute verifyCrossReferences
  ?let @objectsMap  allObjects
  ?let @impType  type
{
  let @refType refType = type as @refType
  # look for the object map of kind [refType ref]
  [allObjects get ![refType ref] ?let @objectKind kindMap]
  if not [[kindMap objects] hasKey ![value string]] then
    error value: "Referenced "+[refType ref]+": "+value+" does not exist"
  end
}


method @applicationDefinition verifyCrossReferences
  ?let @implementation imp
{
  [objects verifyCrossReferences !imp]
}

##
# @fn verify_all
#
# routine verify_all does the verification of all the system.
# 
# @param cpu the root object got from the parsing
# 
proc verifyAll
  ?let @implementation imp
  ?let @applicationDefinition application
{
  verifyAllAttributes ( !imp ![application objects])
  [imp verifyApplication !application]

  # Verify objects references from an object exist
  [application verifyCrossReferences !imp];
}